Port ConCert core to MetaCoq 1.3.1

4ever2 · Jan 16, 2025 · 9d19164 · 9d19164
1 parent fe36d62
commit 9d19164
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 10 deletions.
diff --git a/embedding/theories/pcuic/PCUICCorrectnessAux.v b/embedding/theories/pcuic/PCUICCorrectnessAux.v
@@ -240,17 +240,17 @@ Lemma type_value_term_value Σ ty :
   PcbvCurr.value Σ (type_to_term ty).
 Proof.
   intros Hc Hty. induction Hty.
-  + simpl. constructor. apply tInd_atom.
-  + simpl. now constructor.
+  + simpl. constructor. constructor. apply tInd_atom.
   + simpl. now constructor.
+  + simpl. constructor. now constructor.
   + simpl in *. propify. destruct_hyps.
     erewrite decompose_inductive_mkApps by eauto.
     rewrite <- mkApps_unfold.
     eapply PcbvCurr.value_app.
     * apply tInd_value_head.
     * apply All_app_inv; eauto.
       eapply decompose_inductive_value with (t1 := ty1); eauto.
-  + constructor; eauto.
+  + do 2 constructor; eauto.
 Qed.
 
 #[export] Hint Constructors ty_val : hints.
@@ -369,9 +369,9 @@ Proof.
     inversion Hok; subst.
     eapply Wcbv_value_vars_to_apps; eauto.
     eapply All_impl_inner; eauto.
-  + destruct cm. constructor; auto.
-    simpl. now constructor.
-  + simpl in *. constructor; auto.
+  + destruct cm. do 2 constructor; auto.
+    simpl. now do 2 constructor.
+  + simpl in *. do 2 constructor; auto.
   + simpl in *.
     inversion Hok; subst. now eapply type_value_term_value.
 Qed.

diff --git a/embedding/theories/pcuic/PCUICTranslate.v b/embedding/theories/pcuic/PCUICTranslate.v
@@ -35,7 +35,7 @@ Reserved Notation "T⟦ ty ⟧ " (at level 5).
 Fixpoint type_to_term (ty : type) : term :=
   match ty with
   | tyInd i => tInd (mkInd (kername_of_string i) 0) []
-  | tyForall nm ty => tProd (aRelevant (nNamed (TCString.of_string nm))) (tSort Universe.type0) T⟦ty⟧
+  | tyForall nm ty => tProd (aRelevant (nNamed (TCString.of_string nm))) (tSort Sort.type0) T⟦ty⟧
   | tyVar nm => tVar (TCString.of_string nm)
   | tyApp ty1 ty2 => tApp T⟦ty1⟧ T⟦ty2⟧
   | tyArr ty1 ty2 =>
@@ -84,7 +84,7 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   | eRel i => tRel i
   | eVar nm => tVar (TCString.of_string nm)
   | eLambda nm ty b => tLambda (aRelevant (nNamed (TCString.of_string nm))) T⟦ty⟧ t⟦b⟧Σ
-  | eTyLam nm b => tLambda (aRelevant (nNamed (TCString.of_string nm))) (tSort Universe.type0) t⟦b⟧Σ
+  | eTyLam nm b => tLambda (aRelevant (nNamed (TCString.of_string nm))) (tSort Sort.type0) t⟦b⟧Σ
   | eLetIn nm e1 ty e2 => tLetIn (aRelevant (nNamed (TCString.of_string nm))) t⟦e1⟧Σ T⟦ty⟧ t⟦e2⟧Σ
   | eApp e1 e2 => tApp t⟦e1⟧Σ t⟦e2⟧Σ
   | eConstr i t =>
@@ -175,7 +175,7 @@ Definition trans_one_constr (ind_name : ename) (nparam : nat) (c : constr) : ter
 Fixpoint gen_params n := match n with
                          | O => []
                          | S n' => let nm := ("A" ++ string_of_nat n)%bs in
-                                  let decl := (tSort Universe.type0) in
+                                  let decl := (tSort Sort.type0) in
                                   gen_params n' ++ [mkdecl (aRelevant (nNamed nm)) None (decl)]
                          end.
 
@@ -185,7 +185,7 @@ Definition trans_global_dec (gd : global_dec) : mutual_inductive_entry :=
     let (mp,unqualified_nm) := kername_of_string nm in
     let oie := {|
           mind_entry_typename := unqualified_nm;
-          mind_entry_arity := tSort Universe.type0;
+          mind_entry_arity := tSort Sort.type0;
           mind_entry_template := false;
           mind_entry_consnames :=
             map (fun c => let (mp,unqualified_nm) := kername_of_string c.1 in

diff --git a/extraction/theories/CameLIGOPretty.v b/extraction/theories/CameLIGOPretty.v
@@ -722,6 +722,8 @@ Section PPTerm.
     | tFix _ _ => fun _ => "NotSupportedMutualFix"
     | tCoFix l n => fun _ => "NotSupportedCoFix"
     | tPrim _ => fun _ => "NotSupportedCoqPrimitive"
+    | tLazy _ => fun _ => "NotSupportedLazy"
+    | tForce _ => fun _ => "NotSupportedForce"
   end.
 
 End PPTerm.

diff --git a/extraction/theories/LiquidityPretty.v b/extraction/theories/LiquidityPretty.v
@@ -697,6 +697,8 @@ Definition get_record_projs (oib : ExAst.one_inductive_body) : list string :=
     end
   | tCoFix l n => "NotSupportedCoFix"
   | tPrim _ => "NotSupportedCoqPrimitive"
+  | tLazy _ => "NotSupportedLazy"
+  | tForce _ => "NotSupportedForce"
   end.
 
 End print_term.