Fix translations, and a bit of quotation

.vscode/metacoq.code-workspace

@@ -12,6 +12,7 @@
 
 
 
+
 			"-R", "safechecker-plugin/theories","MetaCoq.SafeCheckerPlugin",
 
 			"-R", "utils/theories","MetaCoq.Utils",
@@ -32,7 +33,9 @@
 		"-R", "erasure-plugin/theories","MetaCoq.ErasurePlugin",
 		"-R", "translations","MetaCoq.Translations",
 		"-R", "test-suite/plugin-demo/theories","MetaCoq.ExtractedPluginDemo",
-		"-R", "test-suite","MetaCoq.TestSuite"
+		"-R", "test-suite","MetaCoq.TestSuite",
+		"-R", "quotation/theories", "MetaCoq.Quotation",
+
 	    ],
 
 	 // When enabled, will trim trailing whitespace when saving a file.

quotation/theories/ToPCUIC/Common/Environment.v

@@ -111,7 +111,7 @@ Module QuoteEnvironment (T : Term) (Import E : EnvironmentSig T) (Import QEH : Q
   #[export] Instance quote_extends_strictly_on_decls {Σ Σ'} : ground_quotable (@extends_strictly_on_decls Σ Σ') := ltac:(cbv [extends_strictly_on_decls]; exact _).
   #[export] Instance quote_strictly_extends_decls {Σ Σ'} : ground_quotable (@strictly_extends_decls Σ Σ') := ltac:(cbv [strictly_extends_decls]; exact _).
 
-  #[export] Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl) := ltac:(cbv [primitive_invariants]; exact _).
+  #[export] Instance quote_primitive_invariants {prim_ty cdecl} : ground_quotable (primitive_invariants prim_ty cdecl) := ltac:(cbv [primitive_invariants]; exact _).
 
   #[export] Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t') := ltac:(induction 1; exact _).
   #[export] Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t') := ltac:(induction 1; exact _).

quotation/theories/ToPCUIC/PCUIC/PCUICAst.v

@@ -11,7 +11,8 @@ From MetaCoq.Quotation.ToPCUIC.QuotationOf.PCUIC Require Import PCUICAst.Instanc
 #[export] Instance quote_branch {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (branch term) := ltac:(destruct 1; exact _).
 #[local] Hint Extern 1 => assumption : typeclass_instances.
 
-#[export] Instance quote_term : ground_quotable term := ltac:(induction 1 using term_forall_list_ind; exact _).
+#[export] Instance quote_term : ground_quotable term.
+ induction 1 using term_forall_list_ind; try exact _.
 
 Module QuotePCUICTerm <: QuoteTerm PCUICTerm.
   #[export] Instance quote_term : ground_quotable PCUICTerm.term := ltac:(cbv [PCUICTerm.term]; exact _).

quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v

@@ -5,8 +5,8 @@ From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) Universes Primitive
 
 #[export] Instance quote_array_model {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (array_model term) := ltac:(destruct 1; exact _).
 
-#[export] Instance quote_prim_model {term tag} {qterm : quotation_of term} : ground_quotable (prim_model term tag) := ltac:(destruct 1; exact _).
+#[export] Instance quote_prim_model {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model term tag) := ltac:(destruct 1; eauto).
 
-#[export] Instance quote_prim_model_of {term tag} : ground_quotable (prim_model_of term tag) := ltac:(cbv [prim_model_of]; exact _).
+#[export] Instance quote_prim_model_of {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model_of term tag) := ltac:(cbv [prim_model_of]; destruct tag; exact _).
 
-#[export] Instance quote_prim_val {term} {qterm : quotation_of term} : ground_quotable (prim_val term) := ltac:(cbv [prim_val]; exact _).
+#[export] Instance quote_prim_val {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_val term) := ltac:(cbv [prim_val]; exact _).

quotation/theories/ToTemplate/Common/Environment.v

@@ -111,7 +111,7 @@ Module QuoteEnvironment (T : Term) (Import E : EnvironmentSig T) (Import QEH : Q
   #[export] Instance quote_extends_strictly_on_decls {Σ Σ'} : ground_quotable (@extends_strictly_on_decls Σ Σ') := ltac:(cbv [extends_strictly_on_decls]; exact _).
   #[export] Instance quote_strictly_extends_decls {Σ Σ'} : ground_quotable (@strictly_extends_decls Σ Σ') := ltac:(cbv [strictly_extends_decls]; exact _).
 
-  #[export] Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl) := ltac:(cbv [primitive_invariants]; exact _).
+  #[export] Instance quote_primitive_invariants {prim_ty cdecl} :0 ground_quotable (primitive_invariants prim_ty cdecl) := ltac:(cbv [primitive_invariants]; exact _).
 
   #[export] Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t') := ltac:(induction 1; exact _).
   #[export] Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t') := ltac:(induction 1; exact _).

translations/param_binary.v

@@ -145,7 +145,7 @@ Fixpoint tsl_rec1_app (app : list term) (E : tsl_table) (t : term) : term :=
   | tFix _ _ | tCoFix _ _ => todo "tsl"
   | tVar _ | tEvar _ _ => todo "tsl"
   | tLambda _ _ _ => tVar "impossible"
-  | tInt _ | tFloat _ => todo "tsl"
+  | tInt _ | tFloat _ | tArray _ _ _ _ => todo "tsl"
   end
   in apply app t1
   end.

translations/param_original.v

@@ -106,7 +106,7 @@ Fixpoint tsl_rec1_app (app : option term) (E : tsl_table) (t : term) : term :=
   | tFix _ _ | tCoFix _ _ => todo "tsl"
   | tVar _ | tEvar _ _ => todo "tsl"
   | tLambda _ _ _ => tVar "impossible"
-  | tInt _ | tFloat _ => todo "tsl"
+  | tInt _ | tFloat _ | tArray _ _ _ _ => todo "tsl"
   end in
   match app with Some t' => mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
                | None => t1 end