fix L framework for 9.0

Author: mrhaandi

theories/L/Computability/Synthetic.v

@@ -209,7 +209,7 @@ Qed.
 Definition F1 {X} (T : nat -> list X) :=  (fun n => let (n, m) := Cantor.of_nat n in nth_error (T n) m).
 
 #[global]
-Instance term_F1 {X} {H : encodable X} :  @computable ((nat -> list X) -> nat -> option X) ((! nat ~> ! list X) ~> ! nat ~> ! option X) (@F1 X).
+Instance term_F1 {X} {H : encodable X} :  @computable ((nat -> list X) -> nat -> option X) ((! nat ~> ! (list X)) ~> ! nat ~> ! (option X)) (@F1 X).
 Proof.
   extract.
 Qed.

theories/L/Datatypes/LBool.v

@@ -6,7 +6,7 @@ From Undecidability.L.Tactics Require Import LTactics GenEncode.
 (*   Eval simpl in *)
 (*     if b then .\"t", "f"; "t" else .\"t", "f"; "f". *)
 
-MetaCoq Run (tmGenEncodeInj "bool_enc" bool).
+MetaRocq Run (tmGenEncodeInj "bool_enc" bool).
 (* For each encoding, Lrewrite must contain an lemma that solves goals like "encode b s t >* match ...end". The database Lrewrite also calls Lproc to discharge the other assumptions *)
 #[export] Hint Resolve bool_enc_correct : Lrewrite.
 

theories/L/Datatypes/LNat.v

@@ -7,7 +7,7 @@ From Undecidability.L Require Import Datatypes.LBool Functions.EqBool Datatypes.
 Import GenEncode. Import Nat.
 (* ** Encoding of natural numbers *)
 
-MetaCoq Run (tmGenEncodeInj "nat_enc" nat).
+MetaRocq Run (tmGenEncodeInj "nat_enc" nat).
 #[export] Hint Resolve nat_enc_correct : Lrewrite.
 
 #[global]
@@ -114,7 +114,7 @@ Proof.
 Qed.
 
 Lemma unenc_correct2 t n : nat_unenc t = Some n -> nat_enc n = t.
-Proof with try solve [Coq.Init.Tactics.easy].
+Proof.
   revert n. eapply (size_induction (f := size) (p := (fun t => forall n, nat_unenc t = Some n -> nat_enc n = t))). clear t. intros t IHt n H.
   destruct t as [ | | t]. easy. easy.
   destruct t as [ | | t]. easy. easy.

theories/L/Datatypes/LOptions.v

@@ -8,7 +8,7 @@ Section Fix_X.
   Context {intX : encodable X}.
 
 
-  MetaCoq Run (tmGenEncode "option_enc" (option X)).
+  MetaRocq Run (tmGenEncode "option_enc" (option X)).
   Hint Resolve option_enc_correct : Lrewrite.
 
   Global Instance encInj_option_enc {H : encInj intX} : encInj (encodable_option_enc).

theories/L/Datatypes/LProd.v

@@ -15,7 +15,7 @@ Section Fix_XY.
   Context {intX : encodable X}.
   Context {intY : encodable Y}.
 
-  MetaCoq Run (tmGenEncode "prod_enc" (X * Y)).
+  MetaRocq Run (tmGenEncode "prod_enc" (X * Y)).
   Hint Resolve prod_enc_correct : Lrewrite.
 
   Global Instance encInj_prod_enc {H : encInj intX} {H' : encInj intY} : encInj (encodable_prod_enc).

theories/L/Datatypes/LSum.v

@@ -9,7 +9,7 @@ Section Fix_XY.
   Variable intX : encodable X.
   Variable intY : encodable Y.
 
-  MetaCoq Run (tmGenEncode "sum_enc" (X + Y)).
+  MetaRocq Run (tmGenEncode "sum_enc" (X + Y)).
   Hint Resolve sum_enc_correct : Lrewrite.
 
   Global Instance encInj_sum_enc {H : encInj intX} {H' : encInj intY} : encInj (encodable_sum_enc).

theories/L/Datatypes/LTerm.v

@@ -3,7 +3,7 @@ From Undecidability.L Require Export Util.L_facts.
 From Undecidability.L.Tactics Require Import LTactics GenEncode.
 
 (* ** Encoding for L-terms *)
-MetaCoq Run (tmGenEncodeInj "term_enc" term).
+MetaRocq Run (tmGenEncodeInj "term_enc" term).
 #[export] Hint Resolve term_enc_correct : Lrewrite.
 
 (* register the non-constant constructors *)

theories/L/Datatypes/LUnit.v

@@ -3,5 +3,5 @@ From Undecidability.L.Tactics Require Import LTactics GenEncode.
 (* * Encodings and extracted basic functions *)
 (* ** Encoding of unit *)
 
-MetaCoq Run (tmGenEncodeInj "unit_enc" unit).
+MetaRocq Run (tmGenEncodeInj "unit_enc" unit).
 #[export] Hint Resolve unit_enc_correct : Lrewrite.

theories/L/Datatypes/List/List_enc.v

@@ -6,7 +6,7 @@ Section Fix_X.
   Variable (X:Type).
   Context {intX : encodable X}.
 
-  MetaCoq Run (tmGenEncode "list_enc" (list X)).
+  MetaRocq Run (tmGenEncode "list_enc" (list X)).
 
   Global Instance encInj_list_enc {H : encInj intX} : encInj (encodable_list_enc).
   Proof. register_inj. Qed. 

theories/L/Reductions/H10_to_L.v

@@ -27,7 +27,7 @@ Inductive poly : Set :=
   | poly_add : poly -> poly -> poly
   | poly_mul : poly -> poly -> poly.
 
-MetaCoq Run (tmGenEncode "enc_poly" poly).
+MetaRocq Run (tmGenEncode "enc_poly" poly).
 #[export] Hint Resolve enc_poly_correct : Lrewrite.
 
 #[export]