diff --git a/Makefile b/Makefile
index 30eb78ba6..a9889ce64 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
 
-all: printconf template-coq pcuic safechecker erasure erasure-plugin safechecker-plugin # quotation
+all: printconf template-coq pcuic safechecker erasure erasure-plugin safechecker-plugin quotation
 
 -include Makefile.conf
 
@@ -12,7 +12,7 @@ ifeq '$(METACOQ_CONFIG)' 'local'
   export OCAMLPATH
 endif
 
-.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations # quotation
+.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations quotation
 
 printconf:
 ifeq '$(METACOQ_CONFIG)' 'local'
@@ -26,14 +26,14 @@ else
 endif
 endif
 
-install: all
+install: all 
 	$(MAKE) -C utils install
 	$(MAKE) -C common install
 	$(MAKE) -C template-coq install
 	$(MAKE) -C pcuic install
 	$(MAKE) -C safechecker install
 	$(MAKE) -C template-pcuic install
-# $(MAKE) -C quotation install
+	$(MAKE) -C quotation install
 	$(MAKE) -C safechecker-plugin install
 	$(MAKE) -C erasure install
 	$(MAKE) -C erasure-plugin install
@@ -45,7 +45,7 @@ uninstall:
 	$(MAKE) -C pcuic uninstall
 	$(MAKE) -C safechecker uninstall
 	$(MAKE) -C template-pcuic uninstall
-#	$(MAKE) -C quotation uninstall
+	$(MAKE) -C quotation uninstall
 	$(MAKE) -C safechecker-plugin uninstall
 	$(MAKE) -C erasure uninstall
 	$(MAKE) -C erasure-plugin uninstall
@@ -74,7 +74,7 @@ clean:
 	$(MAKE) -C pcuic clean
 	$(MAKE) -C safechecker clean
 	$(MAKE) -C template-pcuic clean
-#	$(MAKE) -C quotation clean
+	$(MAKE) -C quotation clean
 	$(MAKE) -C erasure clean
 	$(MAKE) -C erasure-plugin clean
 	$(MAKE) -C examples clean
@@ -88,7 +88,7 @@ vos:
 	$(MAKE) -C pcuic vos
 	$(MAKE) -C safechecker vos
 	$(MAKE) -C template-pcuic vos
-#	$(MAKE) -C quotation vos
+	$(MAKE) -C quotation vos
 	$(MAKE) -C erasure vos
 	$(MAKE) -C erasure-plugin vos
 	$(MAKE) -C translations vos
@@ -100,7 +100,7 @@ quick:
 	$(MAKE) -C pcuic quick
 	$(MAKE) -C safechecker quick
 	$(MAKE) -C template-pcuic quick
-#	$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent
+	$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent
 	$(MAKE) -C erasure quick
 	$(MAKE) -C erasure-plugin quick
 	$(MAKE) -C translations quick
@@ -112,7 +112,7 @@ mrproper:
 	$(MAKE) -C pcuic mrproper
 	$(MAKE) -C safechecker mrproper
 	$(MAKE) -C template-pcuic mrproper
-#	$(MAKE) -C quotation mrproper
+	$(MAKE) -C quotation mrproper
 	$(MAKE) -C erasure mrproper
 	$(MAKE) -C erasure-plugin mrproper
 	$(MAKE) -C examples mrproper
@@ -126,7 +126,7 @@ mrproper:
 	$(MAKE) -C pcuic .merlin
 	$(MAKE) -C safechecker .merlin
 	$(MAKE) -C template-pcuic .merlin
-#	$(MAKE) -C quotation .merlin
+	$(MAKE) -C quotation .merlin
 	$(MAKE) -C erasure .merlin
 	$(MAKE) -C erasure-plugin .merin
 
@@ -148,8 +148,8 @@ safechecker: pcuic
 template-pcuic: template-coq pcuic
 	$(MAKE) -C template-pcuic
 
-#quotation: template-coq pcuic template-pcuic
-#	$(MAKE) -C quotation
+quotation: template-coq pcuic template-pcuic
+	$(MAKE) -C quotation
 
 safechecker-plugin: safechecker template-pcuic
 	$(MAKE) -C safechecker-plugin
diff --git a/coq-metacoq-quotation.opam.disabled b/coq-metacoq-quotation.opam
similarity index 100%
rename from coq-metacoq-quotation.opam.disabled
rename to coq-metacoq-quotation.opam
diff --git a/coq-metacoq.opam b/coq-metacoq.opam
index b497f3e21..0d05677db 100644
--- a/coq-metacoq.opam
+++ b/coq-metacoq.opam
@@ -24,7 +24,7 @@ depends: [
   "coq-metacoq-safechecker-plugin" {= version}
   "coq-metacoq-erasure-plugin" {= version}
   "coq-metacoq-translations" {= version}
-#  "coq-metacoq-quotation" {= version}
+  "coq-metacoq-quotation" {= version}
 ]
 build: [
   ["bash" "./configure.sh" ] {with-test}
diff --git a/quotation/theories/ToPCUIC/Coq/Init.v b/quotation/theories/ToPCUIC/Coq/Init.v
index 2c22b1c51..02d39f555 100644
--- a/quotation/theories/ToPCUIC/Coq/Init.v
+++ b/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.
diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v b/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v
index a983580f0..cacfba567 100644
--- a/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v
+++ b/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 _).
diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v b/quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v
index 3c9b88ab2..904baa88f 100644
--- a/quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v
+++ b/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 _).
diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v b/quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v
index 1683fa234..428815bdf 100644
--- a/quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v
+++ b/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.
diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v b/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v
index 8472e92ab..6e8d3e747 100644
--- a/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v
+++ b/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v
@@ -20,6 +20,9 @@ From MetaCoq.Quotation.ToPCUIC.QuotationOf.PCUIC Require Import PCUICAst.Instanc
 #[export] Instance quote_case_branch_typing {cf wf_local_fun typing Σ Γ ci p ps mdecl idecl ptm brs} {qwf_local_fun : quotation_of wf_local_fun} {qtyping : quotation_of typing} {quote_wf_local_fun : forall Γ, ground_quotable (@wf_local_fun Σ Γ)} {quote_typing : forall Γ i t, ground_quotable (typing Σ Γ i t)} : ground_quotable (@case_branch_typing cf wf_local_fun typing Σ Γ ci p ps mdecl idecl ptm brs)
   := ltac:(destruct 1; exact _).
 
+#[export] Instance quote_primitive_typing_hyps {cf typing Σ Γ p} {qtyping : quotation_of typing} {quote_typing : forall x y, ground_quotable (typing Σ Γ x y)} : ground_quotable (@primitive_typing_hyps cf typing Σ Γ p)
+  := ltac:(destruct 1; exact _).
+
 (* So long as pcuic does axiomatic guard checking, we can't do better than axiomatizing it here *)
 #[export] Instance quote_guard_checking {k Σ Γ t} : ground_quotable (@guard guard_checking k Σ Γ t).
 Proof.
diff --git a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
index c74b76fe4..eb1225ab6 100644
--- a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
+++ b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
@@ -1,12 +1,87 @@
+From MetaCoq.Utils.MCTactics Require Import DestructHead UniquePose.
 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 _).
+
+Definition 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 _).
+
+Definition 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.
+
+Definition quote_onPrims_via_dep
+  {term eq_term leq_term u u' p} {eq_term_dep leq_term_dep}
+  {qp : @onPrims_dep term eq_term leq_term eq_term_dep leq_term_dep u u' p}
+  {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 e, eq_term_dep x y e -> quotation_of e}
+  {quote_leq_term : forall x y e, leq_term_dep x y e -> quotation_of e}
+  : quotation_of p.
+Proof.
+  destruct qp.
+  all: lazymatch goal with
+       | [ H : All_Forall.All2_dep ?T ?x |- _ ]
+         => lazymatch T with
+            | (fun _ _ r => quotation_of r) => idtac
+            | _
+              => assert (All_Forall.All2_dep (fun _ _ r => quotation_of r) x);
+                 [ eapply All_Forall.All2_dep_impl; try exact H; [];
+                   cbv beta; intros;
+                   repeat match goal with
+                     | [ H : _ * _ |- _ ] => destruct H
+                     end;
+                   cbn [fst snd] in *
+                 | clear H ]
+            end
+       | _ => idtac
+       end.
+  all: repeat (let H := multimatch goal with H : _ |- _ => H end in
+               first [ unique pose proof (quote_leq_term _ _ _ H)
+                     | unique pose proof (quote_eq_term _ _ _ H) ]).
+  all: exact _.
+Defined.
+
+#[export] Hint Extern 0 (@quotation_of (@onPrims ?term ?eq_term ?leq_term ?u ?u') ?x)
+=> lazymatch goal with
+   | [ H : @onPrims_dep _ _ _ ?eq_term_dep ?leq_term_dep _ _ x |- _ ]
+     => simple apply (@quote_onPrims_via_dep term eq_term leq_term u u' x eq_term_dep leq_term_dep H)
+   | _ => simple apply @quote_ground;
+          tryif (lazymatch type of leq_term with
+                 | _ -> _ -> Prop => idtac
+                 | Relation_Definitions.relation _ => idtac
+                 end)
+          then simple apply (@quote_onPrims_Type_Prop term eq_term leq_term u u')
+          else simple apply (@quote_onPrims term eq_term leq_term u u')
+   end
+  : typeclass_instances.
+#[export] Hint Cut [
+    ( _ * )
+      quote_ground
+      quote_onPrims
+  ] : typeclass_instances.
diff --git a/quotation/theories/ToTemplate/Coq/Init.v b/quotation/theories/ToTemplate/Coq/Init.v
index 933e5aa79..826a29845 100644
--- a/quotation/theories/ToTemplate/Coq/Init.v
+++ b/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.