WIP

quotation/theories/ToPCUIC/Coq/Init.v

@@ -36,6 +36,10 @@ Defined.
 #[export] Polymorphic Instance quote_prod {A B} {qA : quotation_of A} {qB : quotation_of B} {quoteA : ground_quotable A} {quoteB : ground_quotable B} : ground_quotable (prod A B) := (ltac:(induction 1; exact _)).
 #[export] Polymorphic Instance quote_list {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (list A) := (ltac:(induction 1; exact _)).
 #[export] Polymorphic Instance quotation_of_list {A ls} {qA : quotation_of A} {qls : @All A quotation_of ls} : quotation_of ls := ltac:(induction qls; exact _).
+#[export] Hint Extern 0 (@All ?A quotation_of ?ls)
+=> lazymatch goal with
+   | [ H : @All _ quotation_of _ |- _ ] => assumption
+   end : typeclass_instances.
 #[export] Instance quote_comparison : ground_quotable comparison := ltac:(destruct 1; exact _).
 #[export] Instance quote_CompareSpec {Peq Plt Pgt : Prop} {qPeq : quotation_of Peq} {qPlt : quotation_of Plt} {qPgt : quotation_of Pgt} {quote_Peq : ground_quotable Peq} {quote_Plt : ground_quotable Plt} {quote_Pgt : ground_quotable Pgt} {c} : ground_quotable (CompareSpec Peq Plt Pgt c).
 Proof.

quotation/theories/ToPCUIC/PCUIC/PCUICAst.v

@@ -11,11 +11,7 @@ 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.
- induction 1 using term_forall_list_ind; try exact _.
- destruct p as [? []]; cbn in X. exact _. exact _. destruct X as [? []].
- exact _.
-Defined.
+#[export] Instance quote_term : ground_quotable term := ltac:(induction 1 using term_forall_list_ind; exact _).
 
 Module QuotePCUICTerm <: QuoteTerm PCUICTerm.
   #[export] Instance quote_term : ground_quotable PCUICTerm.term := ltac:(cbv [PCUICTerm.term]; exact _).

quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v

@@ -29,11 +29,6 @@ End with_R.
 #[export] Instance quote_compare_decls {eq_term leq_term u u'} {qeq_term : quotation_of eq_term} {qleq_term : quotation_of leq_term} {quote_eq_term : forall x y, ground_quotable (eq_term x y)} {quote_leq_term : forall x y, ground_quotable (leq_term x y)} : ground_quotable (@compare_decls eq_term leq_term u u')
   := ltac:(destruct 1; exact _).
 
-#[export] Instance quote_onPrims {eq_term leq_term u u'} {qeq_term : quotation_of eq_term} {qleq_term : quotation_of leq_term}
-  {quote_eq_term : forall x y, ground_quotable (eq_term x y)}
-  {quote_leq_term : forall x y, ground_quotable (leq_term x y)} : ground_quotable (@onPrims term eq_term leq_term u u') :=
-  ltac:(destruct 1; exact _).
-
 #[export] Hint Unfold
   eq_predicate
   : quotation.
@@ -54,7 +49,7 @@ Proof.
   | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3) (x4 : ?X4) (x5 : ?X5) (x6 : ?X6) (x7 : ?X7) (x8 : ?X8) (x9 : ?X9) (x10 : ?X10) (t : ?X11), quotation_of t
     => change (forall (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4) (x5 : X5) (x6 : X6) (x7 : X7) (x8 : X8) (x9 : X9) (x10 : X10), ground_quotable X11) in quote_eq_term_upto_univ_napp
   end.
-  destruct t; try replace_quotation_of_goal ().
+  destruct t; replace_quotation_of_goal ().
 Defined.
 
 #[export] Instance quote_compare_term {cf pb Σ ϕ x y} : ground_quotable (@compare_term cf pb Σ ϕ x y) := ltac:(cbv [compare_term]; exact _).

quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v

@@ -4,7 +4,7 @@ From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init.
 From MetaCoq.Quotation.ToPCUIC Require Import (hints) Equations.Type.
 From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall.
 From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) BasicAst Universes Kernames.
-From MetaCoq.Quotation.ToPCUIC.PCUIC Require Import (hints) PCUICAst.
+From MetaCoq.Quotation.ToPCUIC.PCUIC Require Import (hints) PCUICAst PCUICPrimitive.
 
 #[export] Instance quote_red1 {Σ Γ t u} : ground_quotable (@red1 Σ Γ t u).
 Proof.

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

@@ -1,12 +1,36 @@
+From MetaCoq.Utils Require Import MCTactics.DestructHead.
 From MetaCoq.PCUIC Require Import utils.PCUICPrimitive.
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
 From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Numbers Coq.Floats.
 From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) Universes Primitive.
+From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall.
 
 #[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 quotation_of_array_model {term a} {qterm : quotation_of term} {qa : @tPrimProp term quotation_of (existT _ Primitive.primArray (primArrayModel a))} : quotation_of a
+  := ltac:(cbv -[quotation_of] in qa; destruct a; destruct_head'_prod; exact _).
+
+#[export] Hint Extern 0 (@tPrimProp ?term quotation_of ?a)
+=> lazymatch goal with
+   | [ H : @tPrimProp _ quotation_of _ |- _ ] => assumption
+   end : typeclass_instances.
+
 #[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} {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} {quote_term : ground_quotable term} : ground_quotable (prim_val term) := ltac:(cbv [prim_val]; exact _).
+
+#[export] Instance quotation_of_prim_val {term} {p : prim_val term} {qterm : quotation_of term} {qp : @tPrimProp term quotation_of p} : quotation_of p := ltac:(destruct p as [? p]; destruct p; exact _).
+
+#[export] Instance quote_onPrims {term eq_term leq_term u u'} {qterm : quotation_of term} {qeq_term : quotation_of eq_term} {qleq_term : quotation_of leq_term}
+  {quote_term : ground_quotable term}
+  {quote_eq_term : forall x y, ground_quotable (eq_term x y)}
+  {quote_leq_term : forall x y, ground_quotable (leq_term x y)} : ground_quotable (@onPrims term eq_term leq_term u u')
+  := ltac:(destruct 1; exact _).
+
+#[export] Instance quote_onPrims_Type_Prop {term eq_term} {leq_term : _ -> _ -> Prop} {u u'} {qterm : quotation_of term} {qeq_term : quotation_of eq_term} {qleq_term : quotation_of leq_term}
+  {quote_term : ground_quotable term}
+  {quote_eq_term : forall x y, ground_quotable (eq_term x y)}
+  {quote_leq_term : forall x y, ground_quotable (leq_term x y)} : ground_quotable (@onPrims term eq_term leq_term u u')
+  := @quote_onPrims term eq_term leq_term u u' qterm qeq_term qleq_term quote_term quote_eq_term quote_leq_term.

quotation/theories/ToTemplate/Coq/Init.v

@@ -36,6 +36,10 @@ Defined.
 #[export] Polymorphic Instance quote_prod {A B} {qA : quotation_of A} {qB : quotation_of B} {quoteA : ground_quotable A} {quoteB : ground_quotable B} : ground_quotable (prod A B) := (ltac:(induction 1; exact _)).
 #[export] Polymorphic Instance quote_list {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (list A) := (ltac:(induction 1; exact _)).
 #[export] Polymorphic Instance quotation_of_list {A ls} {qA : quotation_of A} {qls : @All A quotation_of ls} : quotation_of ls := ltac:(induction qls; exact _).
+#[export] Hint Extern 0 (@All ?A quotation_of ?ls)
+=> lazymatch goal with
+   | [ H : @All _ quotation_of _ |- _ ] => assumption
+   end : typeclass_instances.
 #[export] Instance quote_comparison : ground_quotable comparison := ltac:(destruct 1; exact _).
 #[export] Instance quote_CompareSpec {Peq Plt Pgt : Prop} {qPeq : quotation_of Peq} {qPlt : quotation_of Plt} {qPgt : quotation_of Pgt} {quote_Peq : ground_quotable Peq} {quote_Plt : ground_quotable Plt} {quote_Pgt : ground_quotable Pgt} {c} : ground_quotable (CompareSpec Peq Plt Pgt c).
 Proof.