diff --git a/Makefile b/Makefile
index 6780d1a14..2ced02b9b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,8 @@
-all: template-coq checker pcuic extraction
+all: template-coq plugin-demo checker pcuic extraction
 
 .PHONY: all template-coq checker install html clean mrproper .merlin test-suite translations
 
-install: 
+install:
 	$(MAKE) -C template-coq install
 	$(MAKE) -C checker install
 	$(MAKE) -C pcuic install
@@ -42,6 +42,9 @@ template-coq:
 pcuic: template-coq
 	$(MAKE) -C pcuic
 
+plugin-demo: template-coq
+	$(MAKE) -C plugin-demo
+
 extraction: checker template-coq pcuic
 	$(MAKE) -C extraction
 
diff --git a/checker/Makefile b/checker/Makefile
index 5ae45fd51..712dbfdf0 100644
--- a/checker/Makefile
+++ b/checker/Makefile
@@ -1,22 +1,22 @@
-all: Makefile.coq
-	$(MAKE) -f Makefile.coq
+TEMPLATE_LIB=../template-coq
 
-.PHONY: all install html clean mrproper
+coq: sources Makefile.coq
+	$(MAKE) -f Makefile.coq
 
-install: Makefile.coq
-	$(MAKE) -f Makefile.coq install
+Makefile.coq: _CoqProject gen-src get-mc
+	coq_makefile -f _CoqProject -o Makefile.coq
 
-html: all
-	$(MAKE) -f Makefile.coq html
+gen-src:
+	$(MAKE) -C gen-src
 
-clean: Makefile.coq
-	$(MAKE) -f Makefile.coq clean
+get-mc: gen-src
+	cp -r $(TEMPLATE_LIB)/gen-src/to-lower.sh src
+	(cd src; ./to-lower.sh)
+	cp -r $(TEMPLATE_LIB)/gen-src/*.ml $(TEMPLATE_LIB)/gen-src/*.mli src
 
-mrproper: clean
-	rm -f Makefile.coq
+.PHONY: get-mc gen-src
 
-Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
+clean:
+	$(MAKE) -f Makefile.coq clean
 
-.merlin: Makefile.coq
-	$(MAKE) -f Makefile.coq .merlin
+sources: gen-src
diff --git a/checker/_CoqProject b/checker/_CoqProject
index 298c9f671..4441f306a 100644
--- a/checker/_CoqProject
+++ b/checker/_CoqProject
@@ -1,90 +1,107 @@
--R ../template-coq/theories Template
--R theories TemplateChecker
--I  ../template-coq/src
+-Q ../template-coq/theories Template
+-I  ../template-coq/build
 -I src
--Q src TemplateChecker
+-Q theories TemplateChecker
 
-src/decimal.mli
-src/decimal.ml
-src/peanoNat.mli
-src/peanoNat.ml
-src/datatypes.mli
-src/datatypes.ml
-src/bool.mli
-src/bool.ml
-src/checker0.mli
 src/checker0.ml
-src/utils.mli
-src/utils.ml
-src/config0.mli
-src/config0.ml
-src/univSubst0.mli
-src/univSubst0.ml
-src/univ0.mli
-src/univ0.ml
-src/nat0.mli
-src/nat0.ml
-src/mSetWeakList.mli
-src/mSetWeakList.ml
-src/list0.mli
-src/list0.ml
-src/specif.mli
-src/specif.ml
-src/equalities.mli
-src/equalities.ml
-src/basics.mli
-src/basics.ml
-src/fSetWeakList.mli
-src/fSetWeakList.ml
-src/decidableType.mli
-src/decidableType.ml
-src/fMapWeakList.mli
-src/fMapWeakList.ml
-src/ascii.mli
-src/ascii.ml
-src/binNums.mli
-src/binNums.ml
-src/binNat.mli
-src/binNat.ml
-src/binPos.mli
-src/binPos.ml
-src/binPosDef.mli
-src/binPosDef.ml
-
-src/orders.mli
-src/orders.ml
-src/ordersTac.mli
-src/ordersTac.ml
-src/orderedType0.mli
-src/orderedType0.ml
-
-src/basicAst.mli
-src/basicAst.ml
-src/ast0.mli
-src/ast0.ml
-src/astUtils.mli
-src/astUtils.ml
-src/uGraph0.mli
-src/uGraph0.ml
-src/binInt.mli
-src/binInt.ml
-src/monad_utils.mli
-src/monad_utils.ml
-src/templateMonad.mli
-src/templateMonad.ml
-src/typing0.mli
-src/typing0.ml
-src/string0.mli
-src/string0.ml
-src/liftSubst.mli
+src/checker0.mli
 src/liftSubst.ml
-src/retyping0.mli
+src/liftSubst.mli
+src/monad_utils.ml
+src/monad_utils.mli
 src/retyping0.ml
+src/retyping0.mli
+src/typing0.ml
+src/typing0.mli
 src/typingWf.ml
 src/typingWf.mli
+src/univSubst0.ml
+src/univSubst0.mli
+src/wf.ml
+src/wf.mli
 
 src/term_quoter.ml
 src/g_template_checker.ml4
 src/template_coq_checker_plugin.mlpack
 
 theories/Loader.v
+
+# from MetaCoq (include verbatim)
+src/ascii.ml
+src/ascii.mli
+src/ast0.ml
+src/ast0.mli
+src/astUtils.ml
+src/astUtils.mli
+src/basicAst.ml
+src/basicAst.mli
+src/basics.ml
+src/basics.mli
+src/binInt.ml
+src/binInt.mli
+src/binNat.ml
+src/binNat.mli
+src/binNums.ml
+src/binNums.mli
+src/binPosDef.ml
+src/binPosDef.mli
+src/binPos.ml
+src/binPos.mli
+src/bool.ml
+src/bool.mli
+src/common0.ml
+src/common0.mli
+src/config0.ml
+src/config0.mli
+src/datatypes.ml
+src/datatypes.mli
+src/decidableType.ml
+src/decidableType.mli
+src/decimal.ml
+src/decimal.mli
+src/equalities.ml
+src/equalities.mli
+src/extractable.ml
+src/extractable.mli
+src/fMapWeakList.ml
+src/fMapWeakList.mli
+src/list0.ml
+src/list0.mli
+src/logic0.ml
+src/logic0.mli
+src/mSetWeakList.ml
+src/mSetWeakList.mli
+src/nat0.ml
+src/nat0.mli
+src/orderedType0.ml
+src/orderedType0.mli
+src/orders.ml
+src/orders.mli
+src/ordersTac.ml
+src/ordersTac.mli
+src/peanoNat.ml
+src/peanoNat.mli
+src/specif.ml
+src/specif.mli
+src/string0.ml
+src/string0.mli
+src/uGraph0.ml
+src/uGraph0.mli
+src/univ0.ml
+src/univ0.mli
+src/utils.ml
+src/utils.mli
+
+# From MetaCoq
+src/run_extractable.mli
+src/run_extractable.ml
+src/tm_util.ml
+src/quoter.ml
+src/quoted.ml
+src/denote.ml
+src/denote.mli
+src/denoter.ml
+src/plugin_core.mli
+src/plugin_core.ml
+src/ast_quoter.ml
+src/ast_denoter.ml
diff --git a/checker/gen-src/Extract.v b/checker/gen-src/Extract.v
new file mode 100644
index 000000000..0f53bed41
--- /dev/null
+++ b/checker/gen-src/Extract.v
@@ -0,0 +1,9 @@
+From Template Require Import All Extraction.
+
+Cd "../src".
+
+Recursive Extraction Library TypingWf.
+Recursive Extraction Library Checker.
+Recursive Extraction Library Retyping.
+
+Cd "../gen-src".
\ No newline at end of file
diff --git a/checker/gen-src/Makefile b/checker/gen-src/Makefile
new file mode 100644
index 000000000..7f6123f7f
--- /dev/null
+++ b/checker/gen-src/Makefile
@@ -0,0 +1,8 @@
+coq: Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+Makefile.coq: _CoqProject
+	coq_makefile -f _CoqProject -o Makefile.coq
+
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq clean
diff --git a/checker/gen-src/_CoqProject b/checker/gen-src/_CoqProject
new file mode 100644
index 000000000..17b07667b
--- /dev/null
+++ b/checker/gen-src/_CoqProject
@@ -0,0 +1,5 @@
+-R ../../template-coq/theories Template
+-I ../../template-coq/src
+-Q . Checker
+
+Extract.v
\ No newline at end of file
diff --git a/checker/src/.gitignore b/checker/src/.gitignore
new file mode 100644
index 000000000..bd41c435d
--- /dev/null
+++ b/checker/src/.gitignore
@@ -0,0 +1,3 @@
+*.mli
+*.ml
+to-lower.sh
\ No newline at end of file
diff --git a/checker/src/g_template_checker.ml4 b/checker/src/g_template_checker.ml4
index 65b80e6c9..59af545bf 100644
--- a/checker/src/g_template_checker.ml4
+++ b/checker/src/g_template_checker.ml4
@@ -12,7 +12,7 @@ let pr_char_list = prlist_with_sep mt pr_char
 
 let check env evm c =
   (* Feedback.msg_debug (str"Quoting"); *)
-  let term = Term_quoter.quote_term_rec env (EConstr.to_constr evm c) in
+  let term = Ast_quoter.quote_term_rec env (EConstr.to_constr evm c) in
   (* Feedback.msg_debug (str"Finished quoting.. checking."); *)
   let fuel = pow two (pow two (pow two two)) in
   let checker_flags = true in
diff --git a/checker/src/template_coq_checker_plugin.mlpack b/checker/src/template_coq_checker_plugin.mlpack
index 441688c60..746897925 100644
--- a/checker/src/template_coq_checker_plugin.mlpack
+++ b/checker/src/template_coq_checker_plugin.mlpack
@@ -1,26 +1,50 @@
-Decimal
 Datatypes
 Bool
-PeanoNat
+Decimal
+Nat0
 List0
-Equalities
-DecidableType
+PeanoNat
+Utils
 Basics
-MSetWeakList
-FSetWeakList
-FMapWeakList
-Nat0
-BinNums
 BinPosDef
 BinPos
 BinNat
 BinInt
 Ascii
 String0
-Specif
+DecidableType
 Orders
 OrdersTac
 OrderedType0
+MSetWeakList
+FMapWeakList
+BinNums
+Univ0
+Ast0
+AstUtils
+BasicAst
+Common
+Config0
+
+Denote
+Denoter
+Equalities
+Extractable
+Logic
+Specif
+UGraph0
+
+Tm_util
+Quoted
+Quoter
+Ast_quoter
+Ast_denoter
+Plugin_core
+Run_extractable
+
+
+
+FSetWeakList
 
 Utils
 Config0
diff --git a/extraction/Makefile.plugin.local b/extraction/Makefile.plugin.local
index bfa366be4..2c5fb9068 100644
--- a/extraction/Makefile.plugin.local
+++ b/extraction/Makefile.plugin.local
@@ -1,2 +1,2 @@
-CAMLFLAGS+=-open Template_coq_checker_plugin -open Template_coq_checker_plugin.Typing0 -open Template_coq_pcuic_plugin
+# CAMLFLAGS+=-open Template_coq_checker_plugin -open Template_coq_checker_plugin.Typing0 -open Template_coq_pcuic_plugin
 CAMLFLAGS+=-w -33 # Unused opens
diff --git a/pcuic/Makefile.plugin.local b/pcuic/Makefile.plugin.local
index 97774d3d0..8337be017 100644
--- a/pcuic/Makefile.plugin.local
+++ b/pcuic/Makefile.plugin.local
@@ -1,2 +1,2 @@
-CAMLFLAGS+=-open Template_coq_checker_plugin
+# CAMLFLAGS+=-open Template_coq_checker_plugin
 CAMLFLAGS+=-w -33 # Unused opens
\ No newline at end of file
diff --git a/plugin-demo/Makefile b/plugin-demo/Makefile
new file mode 100644
index 000000000..058d53b00
--- /dev/null
+++ b/plugin-demo/Makefile
@@ -0,0 +1,23 @@
+TEMPLATE_LIB=../template-coq
+
+coq: sources Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+Makefile.coq: _CoqProject gen-src get-mc
+	coq_makefile -f _CoqProject -o Makefile.coq
+
+gen-src:
+	$(MAKE) -C gen-src
+
+get-mc:
+	cp -r $(TEMPLATE_LIB)/gen-src/to-lower.sh src
+	(cd src; ./to-lower.sh)
+	cp -r $(TEMPLATE_LIB)/gen-src/*.ml $(TEMPLATE_LIB)/gen-src/*.mli src
+
+.PHONY: get-mc gen-src
+
+clean:
+	$(MAKE) -f Makefile.coq clean
+
+sources:
+	$(MAKE) -C gen-src
diff --git a/plugin-demo/README.md b/plugin-demo/README.md
new file mode 100644
index 000000000..430d42ea4
--- /dev/null
+++ b/plugin-demo/README.md
@@ -0,0 +1,26 @@
+# Writing a Plugin with the Extractable Monad
+
+You can use `Template.TemplateMonad.Extractable` to write plugins in Gallina.
+You can use this project as a template for doing this.
+
+
+**Beware**: Things are a little bit convoluted/brittle due to the extraction processes.
+Pull requests are welcome.
+
+## How to use it
+
+1. Write your plugin inside the `gen-src` directory (using the `_CoqProject` in that directory). The plugin should use the `Template.TemplateMonad.Extractable` monad to interact with Coq.
+2. Modify the `gen-src/Extract.v` file to extract the module that you want to call from your plugin.
+3. Run `make sources` which will build the Coq sources to your plugin and extract them to OCaml.
+4. In the `src` directory, write the entry point to your plugin. See `src/g_plugin_demo.ml4` for some examples. *Make sure that you do not use any names that conflict with names of `ml` files inside of `template-coq`.*
+5. In the `src` directory, create an `mlpack` file which includes all the files that you need. This file *must* start with the template located in `template-coq/gen-src/meta_coq_plugin_template.mlpack` to ensure that it uses the appropriate dependencies.
+6. Include any Coq files that your plugin requires in the top-level `theories` directory.
+7. Build the plugin from the root directory and you should be good to go.
+
+
+## How it works
+
+As mentioned above, things are a bit brittle.
+Essentially, what the `Makefile` does is first build the contents of `gen-src` to build the OCaml for the plugin.
+The recursive extraction command will generate all of the files into the `src` directory, including the files that `template-coq` provides.
+The top-level `Makefile` then copies the contents of the `template-coq/gen-src` directory over the `src` directory before building it to ensure that everything is consistent.
diff --git a/plugin-demo/_CoqProject b/plugin-demo/_CoqProject
new file mode 100644
index 000000000..ee148f665
--- /dev/null
+++ b/plugin-demo/_CoqProject
@@ -0,0 +1,94 @@
+-I src
+-Q theories Lens
+
+
+src/demo.ml
+src/demo.mli
+
+
+src/g_demo_plugin.ml4
+src/demo_plugin.mlpack
+
+theories/Lens.v
+theories/Demo.v
+
+
+# from MetaCoq (include verbatim)
+src/ascii.ml
+src/ascii.mli
+src/ast0.ml
+src/ast0.mli
+src/astUtils.ml
+src/astUtils.mli
+src/basicAst.ml
+src/basicAst.mli
+src/basics.ml
+src/basics.mli
+src/binInt.ml
+src/binInt.mli
+src/binNat.ml
+src/binNat.mli
+src/binNums.ml
+src/binNums.mli
+src/binPosDef.ml
+src/binPosDef.mli
+src/binPos.ml
+src/binPos.mli
+src/bool.ml
+src/bool.mli
+src/common0.ml
+src/common0.mli
+src/config0.ml
+src/config0.mli
+src/datatypes.ml
+src/datatypes.mli
+src/decidableType.ml
+src/decidableType.mli
+src/decimal.ml
+src/decimal.mli
+src/equalities.ml
+src/equalities.mli
+src/extractable.ml
+src/extractable.mli
+src/fMapWeakList.ml
+src/fMapWeakList.mli
+src/list0.ml
+src/list0.mli
+src/logic0.ml
+src/logic0.mli
+src/mSetWeakList.ml
+src/mSetWeakList.mli
+src/nat0.ml
+src/nat0.mli
+src/orderedType0.ml
+src/orderedType0.mli
+src/orders.ml
+src/orders.mli
+src/ordersTac.ml
+src/ordersTac.mli
+src/peanoNat.ml
+src/peanoNat.mli
+src/specif.ml
+src/specif.mli
+src/string0.ml
+src/string0.mli
+src/uGraph0.ml
+src/uGraph0.mli
+src/univ0.ml
+src/univ0.mli
+src/utils.ml
+src/utils.mli
+
+# From MetaCoq
+src/run_extractable.mli
+src/run_extractable.ml
+src/tm_util.ml
+src/quoter.ml
+src/quoted.ml
+src/denote.ml
+src/denote.mli
+src/denoter.ml
+src/plugin_core.mli
+src/plugin_core.ml
+src/ast_quoter.ml
+src/ast_denoter.ml
diff --git a/plugin-demo/gen-src/Extract.v b/plugin-demo/gen-src/Extract.v
new file mode 100644
index 000000000..cb88c951a
--- /dev/null
+++ b/plugin-demo/gen-src/Extract.v
@@ -0,0 +1,8 @@
+Require Import Template.Extraction.
+Require Import Demo.demo.
+
+Cd "../src".
+
+Recursive Extraction Library demo.
+
+Cd "../gen-src".
\ No newline at end of file
diff --git a/plugin-demo/gen-src/Makefile b/plugin-demo/gen-src/Makefile
new file mode 100644
index 000000000..7f6123f7f
--- /dev/null
+++ b/plugin-demo/gen-src/Makefile
@@ -0,0 +1,8 @@
+coq: Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+Makefile.coq: _CoqProject
+	coq_makefile -f _CoqProject -o Makefile.coq
+
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq clean
diff --git a/plugin-demo/gen-src/_CoqProject b/plugin-demo/gen-src/_CoqProject
new file mode 100644
index 000000000..d6cf9e427
--- /dev/null
+++ b/plugin-demo/gen-src/_CoqProject
@@ -0,0 +1,8 @@
+-R ../../template-coq/theories Template
+-I ../../template-coq/src
+-Q ../theories Lens
+-Q . Demo
+
+../theories/Lens.v
+demo.v
+Extract.v
\ No newline at end of file
diff --git a/plugin-demo/gen-src/demo.v b/plugin-demo/gen-src/demo.v
new file mode 100644
index 000000000..815e7af1e
--- /dev/null
+++ b/plugin-demo/gen-src/demo.v
@@ -0,0 +1,222 @@
+Require Import Coq.Lists.List.
+From Template Require Import
+     Ast
+     Loader
+     TemplateMonad.Extractable.
+Import TemplateMonad.Extractable.
+Require Import Template.BasicAst Template.AstUtils Ast.
+
+
+Let TemplateMonad := TM.
+Fixpoint mconcat (ls : list (TemplateMonad unit)) : TemplateMonad unit :=
+  match ls with
+  | nil => tmReturn tt
+  | m :: ms => tmBind m (fun _ => mconcat ms)
+  end.
+
+Fixpoint print_all_kns (t : Ast.term) : TM unit :=
+  match t with
+  | tEvar _ ls =>
+    mconcat (List.map print_all_kns ls)
+  | tCast a _ b
+  | tProd _ a b
+  | tLambda _ a b =>
+    tmBind (print_all_kns a) (fun _ => print_all_kns b)
+  | tApp a b =>
+    tmBind (print_all_kns a) (fun _ => mconcat (List.map print_all_kns b))
+  | tLetIn _ a b c =>
+    tmBind (print_all_kns a) (fun _ => tmBind (print_all_kns b) (fun _ => print_all_kns c))
+  | tConst c _ => tmMsg c
+  | tInd i _ => tmMsg i.(inductive_mind)
+  | tConstruct i _ _ => tmMsg i.(inductive_mind)
+  | tProj (i,_,_) b =>
+    tmBind (tmMsg i.(inductive_mind)) (fun _ => print_all_kns b)
+  | _ => tmReturn tt
+  end.
+
+Notation "<% x %>" := (ltac:(let p y := exact y in quote_term x p))
+  (only parsing).
+
+
+Definition gr_to_kername (gr : global_reference) : kername :=
+  match gr with
+  | ConstRef kn => kn
+  | IndRef ind => ind.(inductive_mind)
+  | ConstructRef ind _ => ind.(inductive_mind)
+  end.
+
+Definition tmResolve (nm : String.string) : TM (option kername) :=
+  tmBind (tmAbout nm)
+         (fun gr =>
+            match gr with
+            | None => tmReturn None
+            | Some (ConstRef kn) => tmReturn (Some kn)
+            | Some (IndRef ind) => tmReturn (Some ind.(inductive_mind))
+            | Some (ConstructRef ind _) => tmReturn (Some ind.(inductive_mind))
+            end).
+
+
+(* ^^ Everything above here is generic *)
+
+Require Import Lens.Lens.
+
+
+Set Primitive Projections.
+Set Universe Polymorphism.
+
+Record Info : Set :=
+{ type : ident
+; ctor : ident
+; fields : list (ident * term)
+}.
+
+Fixpoint countTo (n : nat) : list nat :=
+  match n with
+  | 0 => nil
+  | S m => countTo m ++ (m :: nil)
+  end.
+
+Require Import String.
+Open Scope string_scope.
+Definition prepend (ls : string) (i : ident) : ident :=
+  ls ++ i.
+
+Definition cBuild_Lens := <% Build_Lens %>.
+
+Require Import Coq.Lists.List.
+Require Import Coq.Bool.Bool.
+
+
+(* check to see if Var 0 is referenced in any of the terms *)
+Definition mentions (v : nat) (ls : list (ident * term)) : bool :=
+  false.
+
+
+
+Definition mkLens (At : term) (fields : list (ident * term)) (i : nat)
+: option (ident * term) :=
+  match At with
+  | tInd ind args =>
+    let ctor := tConstruct ind 0 args in
+    match nth_error fields i with
+    | None => None
+    | Some (name, Bt) =>
+      if mentions 1 (skipn (S i) fields)
+      then None
+      else
+        let p (x : nat) : projection := (ind, 0, x) in
+        let get_body := tProj (p i) (tRel 0) in
+        let f x :=
+            let this := tProj (p x) (tRel 0) in
+            if PeanoNat.Nat.eqb x i
+            then tApp (tRel 1) (this :: nil)
+            else this
+        in
+        let update_body :=
+            tApp ctor (map f (countTo (List.length fields)))
+        in
+        Some ( prepend "_" name
+             , tApp cBuild_Lens
+                    (At :: At :: Bt :: Bt ::
+                        tLambda nAnon At get_body ::
+                        tLambda nAnon (tProd nAnon Bt Bt) (tLambda nAnon At update_body) ::
+                        nil))
+    end
+  | _ => None
+  end.
+
+Definition getFields (mi : mutual_inductive_body)
+: option Info :=
+  match mi.(ind_bodies) with
+  | oib :: nil =>
+    match oib.(ind_ctors) with
+    | ctor :: nil =>
+      Some {| type := oib.(ind_name)
+            ; ctor := let '(x,_,_) := ctor in x
+            ; fields := oib.(ind_projs)
+           |}
+    | _ => None
+    end
+  | _ => None
+  end.
+
+(* baseName should not contain any paths. For example, if the full name
+is A.B.C#D#E#F, baseName should be F. Also, by import ordering,
+ensure that F resolves to  A.B.C#D#E#F. Use Locate to check this.
+
+If the definition of F refers to any other inductive, they should not
+be in the current section(s).
+ *)
+
+Definition opBind {A B} (a: option A) (f: A -> option B) : option B :=
+  match a with
+  | Some a => f a
+  | None  => None
+  end.
+
+Definition genLensN (baseName : String.string) : TM unit :=
+  tmBind (tmAbout baseName) (fun gr =>
+    match gr with
+    | Some (IndRef kn) =>
+      let name := kn.(inductive_mind) in
+      let ty := Ast.tInd
+        {| BasicAst.inductive_mind := name
+         ; BasicAst.inductive_ind := 0 (* TODO: fix for mutual records *) |} List.nil in
+      tmBind (tmQuoteInductive name) (fun ind =>
+          match getFields ind with
+          | Some info =>
+            let gen i :=
+                match mkLens ty info.(fields) i return TemplateMonad unit with
+                | None => tmFail "failed to build lens"
+                | Some x =>
+                  tmBind (tmEval Common.cbv (snd x)) (fun d =>
+                  tmBind (tmDefinition (fst x) None d) (fun _ =>
+                  tmReturn tt))
+                end
+            in
+            mconcat (map gen (countTo (List.length info.(fields))))
+          | None => tmFail ("failed to get inductive info but quote succeeded")
+          end)
+    | _ => tmFail "not an inductive"
+    end).
+
+
+Definition tmQuoteConstantR (nm : String.string) (bypass : bool) : TM _ :=
+  tmBind (tmAbout nm)
+         (fun gr =>
+            match gr with
+            | Some (ConstRef kn) =>
+              tmBind (tmQuoteConstant kn bypass)
+                     (fun x => tmReturn (Some x))
+            | _ => tmReturn None
+            end).
+
+Definition lookupPrint (baseName : String.string) : TM unit :=
+  tmBind (tmQuoteConstantR baseName true)
+         (fun b =>
+            match b with
+            | None => tmFail "not a constant"
+            | Some b =>
+              match b with
+              | ParameterEntry _ => tmReturn tt
+              | DefinitionEntry d =>
+                tmPrint (definition_entry_body d)
+              end
+            end).
+
+Definition x := <% 0 %>.
+
+Definition lookup (baseName : String.string) : TM unit :=
+  tmBind (tmQuoteConstant baseName true)
+         (fun b => tmReturn tt).
+
+Definition genLensNInst  : TM unit := genLensN "Point".
+
+
+Definition showoffOld : TM unit :=
+  tmBind (tmMsg "showing off tmDefn" )
+         (fun _ =>
+            tmBind (tmDefinition "zeroE" None x)
+                   (fun _ => tmReturn tt)).
+
+Definition showoff : TM unit := genLensNInst.
diff --git a/plugin-demo/src/.gitignore b/plugin-demo/src/.gitignore
new file mode 100644
index 000000000..573f734a5
--- /dev/null
+++ b/plugin-demo/src/.gitignore
@@ -0,0 +1,6 @@
+*.ml
+*.mli
+*.cm*
+*.o
+*.a
+to-lower.sh
\ No newline at end of file
diff --git a/plugin-demo/src/demo_plugin.mlpack b/plugin-demo/src/demo_plugin.mlpack
new file mode 100644
index 000000000..fb2aa38d1
--- /dev/null
+++ b/plugin-demo/src/demo_plugin.mlpack
@@ -0,0 +1,50 @@
+Datatypes
+Bool
+Decimal
+Nat0
+List0
+PeanoNat
+Utils
+Basics
+BinPosDef
+BinPos
+BinNat
+BinInt
+Ascii
+String0
+DecidableType
+Orders
+OrdersTac
+OrderedType0
+MSetWeakList
+FMapWeakList
+BinNums
+Univ0
+Ast0
+AstUtils
+BasicAst
+Common
+Config0
+
+Tm_util
+Denote
+Denoter
+Equalities
+Extractable
+Logic
+Specif
+UGraph0
+
+Quoted
+Quoter
+Ast_quoter
+Ast_denoter
+Plugin_core
+Run_extractable
+
+Demo
+G_demo_plugin
+
+Datatypes
+Datatypes
+Datatypes
\ No newline at end of file
diff --git a/plugin-demo/src/g_demo_plugin.ml4 b/plugin-demo/src/g_demo_plugin.ml4
new file mode 100644
index 000000000..b7b7124ab
--- /dev/null
+++ b/plugin-demo/src/g_demo_plugin.ml4
@@ -0,0 +1,40 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmp" i*)
+
+open Entries
+open Run_extractable
+open Ltac_plugin
+open Entries
+open Names
+open Tacexpr
+open Tacinterp
+open Misctypes
+open Stdarg
+open Tacarg
+open Ast_quoter
+
+DECLARE PLUGIN "demo_plugin"
+
+VERNAC COMMAND EXTEND Make_vernac CLASSIFIED AS QUERY
+   | [ "Showoff" ] ->
+     [ Run_extractable.run_vernac Demo.showoff ]
+END;;
+
+let quote_string s =
+  let rec aux acc i =
+    if i < 0 then acc
+    else aux (s.[i] :: acc) (i - 1)
+  in aux [] (String.length s - 1)
+
+VERNAC COMMAND EXTEND Make_lens_vernac CLASSIFIED AS SIDEFF
+| [ "Make" "Lens" ident(name) ] ->
+     [ Run_extractable.run_vernac (Demo.genLensN (quote_string (Names.Id.to_string name))) ]
+
+END;;
+
+VERNAC COMMAND EXTEND Unquote_vernac CLASSIFIED AS SIDEFF
+| [ "LookupPrint" ident(name) ] ->
+     [ let nstr = Names.Id.to_string name in
+       Run_extractable.run_vernac (Demo.lookupPrint (quote_string nstr)) ]
+
+END;;
diff --git a/plugin-demo/test/test.v b/plugin-demo/test/test.v
new file mode 100644
index 000000000..6991415ab
--- /dev/null
+++ b/plugin-demo/test/test.v
@@ -0,0 +1,4 @@
+Require Import Demo.Demo.
+
+
+Showoff.
\ No newline at end of file
diff --git a/plugin-demo/theories/Demo.v b/plugin-demo/theories/Demo.v
new file mode 100644
index 000000000..ff2670ec4
--- /dev/null
+++ b/plugin-demo/theories/Demo.v
@@ -0,0 +1,26 @@
+Require Import Coq.Strings.String.
+Declare ML Module "demo_plugin".
+Require Import Lens.Lens.
+
+Set Primitive Projections.
+
+Record Point : Set :=
+  { x: nat;
+    y:nat
+  }.
+
+Definition two:=1+2.
+About plus.
+
+LookupPrint two.
+
+
+Fail Print zeroE.
+
+Make Lens Point.
+
+SearchAbout Point.
+
+(*
+(* process coq segmentation fault *)
+    *)
\ No newline at end of file
diff --git a/plugin-demo/theories/Lens.v b/plugin-demo/theories/Lens.v
new file mode 100644
index 000000000..8b226ad9e
--- /dev/null
+++ b/plugin-demo/theories/Lens.v
@@ -0,0 +1,24 @@
+Set Primitive Projections.
+
+Record Lens (a b c d : Type) : Type :=
+{ view : a -> c
+; over : (c -> d) -> a -> b
+}.
+
+Arguments over {_ _ _ _} _ _ _.
+Arguments view {_ _ _ _} _ _.
+
+Definition lens_compose {a b c d e f : Type}
+           (l1 : Lens a b c d) (l2 : Lens c d e f)
+: Lens a b e f :=
+{| view := fun x : a => view l2 (view l1 x)
+ ; over := fun f0 : e -> f => over l1 (over l2 f0) |}.
+
+Infix "∙" := lens_compose (at level 90, left associativity).
+
+Section ops.
+  Context {a b c d : Type} (l : Lens a b c d).
+
+  Definition set (new : d) : a -> b :=
+    l.(over) (fun _ => new).
+End ops.
diff --git a/template-coq/.gitignore b/template-coq/.gitignore
new file mode 100644
index 000000000..f08c6eae6
--- /dev/null
+++ b/template-coq/.gitignore
@@ -0,0 +1,2 @@
+Makefile.plugin
+Makefile.plugin.conf
\ No newline at end of file
diff --git a/template-coq/Makefile b/template-coq/Makefile
index 5ae45fd51..9b749cc64 100644
--- a/template-coq/Makefile
+++ b/template-coq/Makefile
@@ -1,7 +1,25 @@
-all: Makefile.coq
+all: coq plugin
+
+coq: Makefile.coq
 	$(MAKE) -f Makefile.coq
+	mkdir -p build
+	cp src/template_coq.cmx src/template_coq.cmxa src/template_coq.cmxs build
+
+
+plugin: coq Makefile.plugin gen-src/.generate
+	@ echo "Copying from src to gen-src"
+	@ for x in $(TOCOPY); do rm -f gen-src/$$x; cp src/$$x gen-src/$$x; done
+	(cd gen-src; ./to-lower.sh)
+	$(MAKE) -f Makefile.plugin
+
+theories/Extraction.vo: coq
 
-.PHONY: all install html clean mrproper
+gen-src/.generate: theories/Extraction.vo
+	coqc -Q theories Template theories/Extraction.v
+	@ touch gen-src/.generate
+
+
+.PHONY: all install html clean mrproper plugin coq
 
 install: Makefile.coq
 	$(MAKE) -f Makefile.coq install
@@ -18,5 +36,10 @@ mrproper: clean
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
 
+Makefile.plugin: _PluginProject
+	coq_makefile -f _PluginProject -o Makefile.plugin
+
 .merlin: Makefile.coq
 	$(MAKE) -f Makefile.coq .merlin
+
+TOCOPY=ast_denoter.ml ast_quoter.ml denote.ml denoter.ml plugin_core.ml plugin_core.mli quoted.ml quoter.ml run_extractable.ml run_extractable.mli tm_util.ml
diff --git a/template-coq/_CoqProject b/template-coq/_CoqProject
index c2bdc0a9f..914cd0ca4 100644
--- a/template-coq/_CoqProject
+++ b/template-coq/_CoqProject
@@ -1,22 +1,26 @@
 -I src
 -R theories Template
 
+# the MetaCoq plugin
 src/tm_util.ml
-# src/quoter.mli
+
+src/quoted.ml
 src/quoter.ml
-# src/constr_quoter.mli
+src/constr_quoted.ml
 src/constr_quoter.ml
-src/denote.mli
+
+src/denoter.ml
 src/denote.ml
-# src/g_template_coq.mli
+src/constr_denoter.ml
+
 src/g_template_coq.ml4
 src/template_coq.mlpack
 src/template_monad.mli
 src/template_monad.ml
 src/run_template_monad.mli
 src/run_template_monad.ml
-src/pluginCore.mli
-src/pluginCore.ml
+src/plugin_core.mli
+src/plugin_core.ml
 
 theories/LibHypsNaming.v
 theories/utils.v theories/config.v theories/kernel/univ.v
@@ -27,7 +31,7 @@ theories/LiftSubst.v theories/UnivSubst.v theories/Typing.v
 theories/TypingWf.v theories/Generation.v theories/WeakeningEnv.v
 theories/Closed.v theories/Weakening.v theories/Substitution.v
 theories/MetaTheory.v theories/Checker.v theories/WcbvEval.v
-theories/Retyping.v theories/All.v theories/Extraction.v
+theories/Retyping.v theories/All.v
 
 # the Template monad
 theories/TemplateMonad.v
@@ -35,4 +39,7 @@ theories/TemplateMonad/Common.v
 theories/TemplateMonad/Core.v
 theories/TemplateMonad/Extractable.v
 theories/TemplateMonad/Monad.v
-theories/monad_utils.v
\ No newline at end of file
+theories/monad_utils.v
+
+# Extraction
+theories/Extraction.v
diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject
new file mode 100644
index 000000000..8adc44e4d
--- /dev/null
+++ b/template-coq/_PluginProject
@@ -0,0 +1,84 @@
+-I gen-src
+-R test-plugin Test
+
+# Generated Code
+gen-src/ascii.ml
+gen-src/ascii.mli
+gen-src/ast0.ml
+gen-src/ast0.mli
+gen-src/astUtils.ml
+gen-src/astUtils.mli
+gen-src/basicAst.ml
+gen-src/basicAst.mli
+gen-src/basics.ml
+gen-src/basics.mli
+gen-src/binInt.ml
+gen-src/binInt.mli
+gen-src/binNat.ml
+gen-src/binNat.mli
+gen-src/binNums.ml
+gen-src/binNums.mli
+gen-src/binPosDef.ml
+gen-src/binPosDef.mli
+gen-src/binPos.ml
+gen-src/binPos.mli
+gen-src/bool.ml
+gen-src/bool.mli
+gen-src/common0.ml
+gen-src/common0.mli
+gen-src/config0.ml
+gen-src/config0.mli
+gen-src/datatypes.ml
+gen-src/datatypes.mli
+gen-src/decidableType.ml
+gen-src/decidableType.mli
+gen-src/decimal.ml
+gen-src/decimal.mli
+gen-src/equalities.ml
+gen-src/equalities.mli
+gen-src/extractable.ml
+gen-src/extractable.mli
+gen-src/fMapWeakList.ml
+gen-src/fMapWeakList.mli
+gen-src/list0.ml
+gen-src/list0.mli
+gen-src/logic0.ml
+gen-src/logic0.mli
+gen-src/mSetWeakList.ml
+gen-src/mSetWeakList.mli
+gen-src/nat0.ml
+gen-src/nat0.mli
+gen-src/orderedType0.ml
+gen-src/orderedType0.mli
+gen-src/orders.ml
+gen-src/orders.mli
+gen-src/ordersTac.ml
+gen-src/ordersTac.mli
+gen-src/peanoNat.ml
+gen-src/peanoNat.mli
+gen-src/specif.ml
+gen-src/specif.mli
+gen-src/string0.ml
+gen-src/string0.mli
+gen-src/uGraph0.ml
+gen-src/uGraph0.mli
+gen-src/univ0.ml
+gen-src/univ0.mli
+gen-src/utils.ml
+gen-src/utils.mli
+
+
+gen-src/tm_util.ml
+gen-src/quoted.ml
+gen-src/quoter.ml
+gen-src/denoter.ml
+gen-src/denote.ml
+gen-src/plugin_core.ml
+gen-src/plugin_core.mli
+gen-src/ast_quoter.ml
+gen-src/ast_denoter.ml
+
+gen-src/run_extractable.ml
+gen-src/run_extractable.mli
+
+gen-src/meta_coq_plugin_template.mlpack
diff --git a/template-coq/gen-src/.gitignore b/template-coq/gen-src/.gitignore
new file mode 100644
index 000000000..a8e0efef5
--- /dev/null
+++ b/template-coq/gen-src/.gitignore
@@ -0,0 +1,3 @@
+*.mli
+*.ml
+.generate
\ No newline at end of file
diff --git a/template-coq/gen-src/meta_coq_plugin_template.mlpack b/template-coq/gen-src/meta_coq_plugin_template.mlpack
new file mode 100644
index 000000000..74679db84
--- /dev/null
+++ b/template-coq/gen-src/meta_coq_plugin_template.mlpack
@@ -0,0 +1,43 @@
+Datatypes
+Bool
+Decimal
+Nat0
+List0
+PeanoNat
+Utils
+Basics
+BinPosDef
+BinPos
+BinNat
+BinInt
+Ascii
+String0
+DecidableType
+Orders
+OrdersTac
+OrderedType0
+MSetWeakList
+FMapWeakList
+BinNums
+Univ0
+Ast0
+AstUtils
+BasicAst
+Common
+Config0
+
+Denote
+Denoter
+Equalities
+Extractable
+Logic
+Specif
+UGraph0
+
+Tm_util
+Quoted
+Quoter
+Ast_quoter
+Ast_denoter
+Plugin_core
+Run_extractable
diff --git a/template-coq/gen-src/to-lower.sh b/template-coq/gen-src/to-lower.sh
new file mode 100755
index 000000000..93bb3e362
--- /dev/null
+++ b/template-coq/gen-src/to-lower.sh
@@ -0,0 +1,9 @@
+for i in *.ml*
+do
+    newi=`echo $i | cut -b 1 | tr '[:upper:]' '[:lower:]'``echo $i | cut -b 2-`;
+    if [ $i != $newi ]
+    then
+        echo "Moving " $i "to" $newi;
+        mv $i $newi;
+    fi
+done
diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml
new file mode 100644
index 000000000..838c5138b
--- /dev/null
+++ b/template-coq/src/ast_denoter.ml
@@ -0,0 +1,140 @@
+open Names
+open Constr
+open BasicAst
+open Ast0
+open Quoted
+open Quoter
+open Ast_quoter
+
+module ExtractionDenoter =
+struct
+  type t = Ast0.term
+  type quoted_ident = char list
+  type quoted_int = Datatypes.nat
+  type quoted_bool = bool
+  type quoted_name = name
+  type quoted_sort = Univ0.universe
+  type quoted_cast_kind = cast_kind
+  type quoted_kernel_name = char list
+  type quoted_inductive = inductive
+  type quoted_proj = projection
+  type quoted_global_reference = global_reference
+
+  type quoted_sort_family = sort_family
+  type quoted_constraint_type = Univ0.constraint_type
+  type quoted_univ_constraint = Univ0.univ_constraint
+  type quoted_univ_instance = Univ0.Instance.t
+  type quoted_univ_constraints = Univ0.constraints
+  type quoted_univ_context = Univ0.universe_context
+  type quoted_inductive_universes = quoted_univ_context
+
+  type quoted_mind_params = (ident * local_entry) list
+  type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list
+  type quoted_definition_entry = t * t option * quoted_univ_context
+  type quoted_mind_entry = mutual_inductive_entry
+  type quoted_mind_finiteness = recursivity_kind
+  type quoted_entry = (constant_entry, quoted_mind_entry) sum option
+
+  type quoted_context_decl = context_decl
+  type quoted_context = context
+  type quoted_one_inductive_body = one_inductive_body
+  type quoted_mutual_inductive_body = mutual_inductive_body
+  type quoted_constant_body = constant_body
+  type quoted_global_decl = global_decl
+  type quoted_global_declarations = global_declarations
+  type quoted_program = program
+
+  let mkAnon = mkAnon
+  let mkName = mkName
+  let quote_kn = quote_kn
+  let mkRel = mkRel
+  let mkVar = mkVar
+  let mkEvar = mkEvar
+  let mkSort = mkSort
+  let mkCast = mkCast
+  let mkConst = mkConst
+  let mkProd = mkProd
+
+  let mkLambda = mkLambda
+  let mkApp = mkApp
+  let mkLetIn = mkLetIn
+  let mkFix = mkFix
+  let mkConstruct = mkConstruct
+  let mkCoFix = mkCoFix
+  let mkInd = mkInd
+  let mkCase = mkCase
+  let quote_proj = quote_proj
+  let mkProj = mkProj
+  let print_term (u: t) : Pp.t = Pp.str "printing not implemented"
+
+  let unquote_def (x: 't BasicAst.def) : ('t, name, quoted_int) Quoted.adef =
+    {
+      adname=dname x;
+      adtype=dtype x;
+      adbody=dbody x;
+      rarg=rarg x
+    }
+
+  let inspect_term (tt: t):(t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term=
+    match tt with
+    | Coq_tRel n -> ACoq_tRel n
+    | Coq_tVar v -> ACoq_tVar v
+    | Coq_tEvar (x,l) -> ACoq_tEvar (x,l)
+    | Coq_tSort u -> ACoq_tSort u
+    | Coq_tCast (t,k,tt) -> ACoq_tCast (t,k,tt)
+    | Coq_tProd (a,b,c) -> ACoq_tProd (a,b,c)
+    | Coq_tLambda (a,b,c) -> ACoq_tLambda (a,b,c)
+    | Coq_tLetIn (a,b,c,d) -> ACoq_tLetIn (a,b,c,d)
+    | Coq_tApp (a,b) -> ACoq_tApp (a,b)
+    | Coq_tConst (a,b) -> ACoq_tConst (a,b)
+    | Coq_tInd (a,b) -> ACoq_tInd (a,b)
+    | Coq_tConstruct (a,b,c) -> ACoq_tConstruct (a,b,c)
+    | Coq_tCase (a,b,c,d) -> ACoq_tCase (a,b,c,d)
+    | Coq_tProj (a,b) -> ACoq_tProj (a,b)
+    | Coq_tFix (a,b) -> ACoq_tFix (List.map unquote_def a,b)
+    | Coq_tCoFix (a,b) -> ACoq_tCoFix (List.map unquote_def a,b)
+    (*
+    | Coq_tApp of term * term list
+    | Coq_tConst of kername * universe_instance
+    | Coq_tInd of inductive * universe_instance
+    | Coq_tConstruct of inductive * nat * universe_instance
+    | Coq_tCase of (inductive * nat) * term * term * (nat * term) list
+    | Coq_tProj of projection * term
+    | Coq_tFix of term mfixpoint * nat
+    | Coq_tCoFix of term mfixpoint * nat
+    *)
+
+  let unquote_ident (qi: quoted_ident) : Id.t
+  = Ast_quoter.unquote_ident qi
+
+  let unquote_name (qn: quoted_name) : Name.t
+  = Ast_quoter.unquote_name qn
+
+  let unquote_int (q:  quoted_int) : int
+  = Ast_quoter.unquote_int q
+
+  let unquote_bool (q: quoted_bool) : bool
+  = Ast_quoter.unquote_bool q
+
+  let unquote_cast_kind (q: quoted_cast_kind ) : Constr.cast_kind
+  = Ast_quoter.unquote_cast_kind q
+
+  let unquote_kn (q:  quoted_kernel_name ) : Libnames.qualid
+  = Ast_quoter.unquote_kn q
+
+  let unquote_inductive (q:  quoted_inductive ) : Names.inductive
+  = Ast_quoter.unquote_inductive q
+
+  let unquote_proj (q: quoted_proj ) : (quoted_inductive * quoted_int * quoted_int)
+  = Ast_quoter.unquote_proj q
+
+  let unquote_universe (q: Evd.evar_map) (qs: quoted_sort): Evd.evar_map * Univ.Universe.t
+  = Ast_quoter.unquote_universe q qs
+
+  let unquote_universe_instance(evm: Evd.evar_map) (l: quoted_univ_instance): Evd.evar_map * Univ.Instance.t
+  = (evm,  Univ.Instance.of_array (Array.of_list (List0.map unquote_level l)))
+
+
+end
+
+module  ExtractionDenote = Denote.Denote(ExtractionDenoter)
diff --git a/checker/src/term_quoter.ml b/template-coq/src/ast_quoter.ml
similarity index 87%
rename from checker/src/term_quoter.ml
rename to template-coq/src/ast_quoter.ml
index b2902f7b0..00e11ab2a 100644
--- a/checker/src/term_quoter.ml
+++ b/template-coq/src/ast_quoter.ml
@@ -4,28 +4,12 @@
 open Constr
 open BasicAst
 open Ast0
-open Template_coq
+open Quoted
 open Quoter
 
-let quote_string s =
-  let rec aux acc i =
-    if i < 0 then acc
-    else aux (s.[i] :: acc) (i - 1)
-  in aux [] (String.length s - 1)
-
-let unquote_string l =
-  let buf = Bytes.create (List.length l) in
-  let rec aux i = function
-    | [] -> ()
-    | c :: cs ->
-      Bytes.set buf i c; aux (succ i) cs
-  in
-  aux 0 l;
-  Bytes.to_string buf
-
 module TemplateASTQuoter =
 struct
-  type t = term
+  type t = Ast0.term
   type quoted_ident = char list
   type quoted_int = Datatypes.nat
   type quoted_bool = bool
@@ -64,7 +48,7 @@ struct
   open Names
 
   let quote_ident id =
-    quote_string (Id.to_string id)
+    string_to_list (Id.to_string id)
 
   let quote_name = function
     | Anonymous -> Coq_nAnon
@@ -83,7 +67,7 @@ struct
     else if Univ.Level.is_set l then Univ0.Level.set
     else match Univ.Level.var_index l with
          | Some x -> Univ0.Level.Var (quote_int x)
-         | None -> Univ0.Level.Level (quote_string (Univ.Level.to_string l))
+         | None -> Univ0.Level.Level (string_to_list (Univ.Level.to_string l))
 
   let quote_universe s : Univ0.universe =
     (* hack because we can't recover the list of level*int *)
@@ -110,7 +94,7 @@ struct
     | NATIVEcast -> NativeCast
     | VMcast -> VmCast
 
-  let quote_kn kn = quote_string (KerName.to_string kn)
+  let quote_kn kn = string_to_list (KerName.to_string kn)
   let quote_inductive (kn, i) = { inductive_mind = kn ; inductive_ind = i }
   let quote_proj ind p a = ((ind,p),a)
 
@@ -273,17 +257,19 @@ struct
       mind_entry_universes = univs;
       mind_entry_private = None }
 
+  let quote_constant_entry (ty, body, ctx) : constant_entry =
+    match body with
+    | None -> ParameterEntry { parameter_entry_type = ty;
+                               parameter_entry_universes = ctx }
+    | Some b -> DefinitionEntry { definition_entry_type = ty;
+                                  definition_entry_body = b;
+                                  definition_entry_universes = ctx;
+                                  definition_entry_opaque = false }
+
   let quote_entry e =
     match e with
     | Some (Left (ty, body, ctx)) ->
-       let entry = match body with
-         | None -> ParameterEntry { parameter_entry_type = ty;
-                                    parameter_entry_universes = ctx }
-        | Some b -> DefinitionEntry { definition_entry_type = ty;
-                                      definition_entry_body = b;
-                                      definition_entry_universes = ctx;
-                                      definition_entry_opaque = false }
-       in Some (Left entry)
+      Some (Left (quote_constant_entry (ty, body, ctx)))
     | Some (Right mind_entry) ->
        Some (Right mind_entry)
     | None -> None
@@ -298,7 +284,7 @@ struct
 
 
   let unquote_ident (qi: quoted_ident) : Id.t =
-    let s = unquote_string qi in
+    let s = list_to_string qi in
     Id.of_string s
 
   let unquote_name (q: quoted_name) : Name.t =
@@ -323,15 +309,15 @@ struct
     | RevertCast -> REVERTcast
 
   let unquote_kn (q: quoted_kernel_name) : Libnames.qualid =
-    let s = unquote_string q in
+    let s = list_to_string q in
     Libnames.qualid_of_string s
 
   let unquote_inductive (q: quoted_inductive) : Names.inductive =
     let { inductive_mind = na; inductive_ind = i } = q in
-    let comps = CString.split '.' (unquote_string na) in
+    let comps = CString.split '.' (list_to_string na) in
     let comps = List.map Id.of_string comps in
     let id, dp = CList.sep_last comps in
-    let dp = DirPath.make dp in
+    let dp = DirPath.make (List.rev dp) in
     let mind = Globnames.encode_mind dp id in
     (mind, unquote_int i)
 
@@ -345,12 +331,13 @@ struct
     | Univ0.Level.Coq_lProp -> Univ.Level.prop
     | Univ0.Level.Coq_lSet -> Univ.Level.set
     | Univ0.Level.Level s ->
-      let s = unquote_string s in
+      let s = list_to_string s in
       let comps = CString.split '.' s in
       let last, dp = CList.sep_last comps in
       let dp = DirPath.make (List.map Id.of_string comps) in
       let idx = int_of_string last in
       Univ.Level.make dp idx
+      (* should this level be added to the environment. Denote.unquote_level does that *)
     | Univ0.Level.Var n -> Univ.Level.var (unquote_int n)
 
   let unquote_level_expr (trm : Univ0.Level.t) (b : quoted_bool) : Univ.Universe.t =
@@ -367,12 +354,23 @@ struct
           let u' = unquote_level_expr l b in Univ.Universe.sup u u')
         (unquote_level_expr l b) q
 
-  let print_term (u: t) : Pp.t = failwith "print_term in term_quoter.ml not yet implemented"
-
+  let quote_global_reference : Globnames.global_reference -> quoted_global_reference = function
+    | Globnames.VarRef _ -> CErrors.user_err (Pp.str "VarRef unsupported")
+    | Globnames.ConstRef c ->
+      let kn = quote_kn (Names.Constant.canonical c) in
+      BasicAst.ConstRef kn
+    | Globnames.IndRef (i, n) ->
+      let kn = quote_kn (Names.MutInd.canonical i) in
+      let n = quote_int n in
+      BasicAst.IndRef (quote_inductive (kn,n))
+    | Globnames.ConstructRef ((i, n), k) ->
+       let kn = quote_kn (Names.MutInd.canonical i) in
+       let n = quote_int n in
+       let k = (quote_int (k - 1)) in
+       BasicAst.ConstructRef (quote_inductive (kn,n), k)
 end
 
-
-
 module TemplateASTReifier = Reify(TemplateASTQuoter)
 
+include TemplateASTQuoter
 include TemplateASTReifier
diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml
new file mode 100644
index 000000000..7e3148d4a
--- /dev/null
+++ b/template-coq/src/constr_denoter.ml
@@ -0,0 +1,314 @@
+open Pp
+open Names
+open Univ
+open Tm_util
+open Quoted
+open Denote
+open Constr_quoted
+
+
+
+(* If strict unquote universe mode is on then fail when unquoting a non *)
+(* declared universe / an empty list of level expressions. *)
+(* Otherwise, add it / a fresh level the global environnment. *)
+
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "strict unquote universe mode";
+      optkey   = ["Strict"; "Unquote"; "Universe"; "Mode"];
+      optread  = (fun () -> !strict_unquote_universe_mode);
+      optwrite = (fun b -> strict_unquote_universe_mode := b) }
+
+
+module CoqLiveDenoter =
+struct
+  include ConstrQuoted
+
+  type quoted_reduction_strategy = Constr.t (* of type Ast.reductionStrategy *)
+
+
+  let unquote_ident trm =
+    Names.Id.of_string (unquote_string trm)
+
+  let unquote_cast_kind trm =
+    if Constr.equal trm kVmCast then
+      Constr.VMcast
+    else if Constr.equal trm kCast then
+      Constr.DEFAULTcast
+    else if Constr.equal trm kRevertCast then
+      Constr.REVERTcast
+    else if Constr.equal trm kNative then
+      Constr.VMcast
+    else
+      not_supported_verb trm "unquote_cast_kind"
+
+  let unquote_name trm =
+    let (h,args) = app_full trm [] in
+    if Constr.equal h nAnon then
+      Names.Anonymous
+    else if Constr.equal h nNamed then
+      match args with
+        n :: [] -> Names.Name (unquote_ident n)
+      | _ -> bad_term_verb trm "unquote_name"
+    else
+      not_supported_verb trm "unquote_name"
+
+  let get_level evm s =
+    if CString.string_contains ~where:s ~what:"." then
+      match List.rev (CString.split '.' s) with
+      | [] -> CErrors.anomaly (str"Invalid universe name " ++ str s ++ str".")
+      | n :: dp ->
+        let num = int_of_string n in
+        let dp = DirPath.make (List.map Id.of_string dp) in
+        let l = Univ.Level.make dp num in
+        try
+          let evm = Evd.add_global_univ evm l in
+          if !strict_unquote_universe_mode then
+            CErrors.user_err ~hdr:"unquote_level" (str ("Level "^s^" is not a declared level and you are in Strict Unquote Universe Mode."))
+          else (Feedback.msg_info (str"Fresh universe " ++ Level.pr l ++ str" was added to the context.");
+                evm, l)
+        with
+        | UGraph.AlreadyDeclared -> evm, l
+    else
+      try
+        evm, Evd.universe_of_name evm (Id.of_string s)
+      with Not_found ->
+      try
+        let univ, k = Nametab.locate_universe (Libnames.qualid_of_string s) in
+        evm, Univ.Level.make univ k
+      with Not_found ->
+        CErrors.user_err ~hdr:"unquote_level" (str ("Level "^s^" is not a declared level."))
+
+
+
+
+
+  let unquote_level evm trm (* of type level *) : Evd.evar_map * Univ.Level.t =
+    let (h,args) = app_full trm [] in
+    if Constr.equal h lProp then
+      match args with
+      | [] -> evm, Univ.Level.prop
+      | _ -> bad_term_verb trm "unquote_level"
+    else if Constr.equal h lSet then
+      match args with
+      | [] -> evm, Univ.Level.set
+      | _ -> bad_term_verb trm "unquote_level"
+    else if Constr.equal h tLevel then
+      match args with
+      | s :: [] -> debug (fun () -> str "Unquoting level " ++ pr_constr trm);
+        get_level evm (unquote_string s)
+      | _ -> bad_term_verb trm "unquote_level"
+    else if Constr.equal h tLevelVar then
+      match args with
+      | l :: [] -> evm, Univ.Level.var (unquote_nat l)
+      | _ -> bad_term_verb trm "unquote_level"
+    else
+      not_supported_verb trm "unquote_level"
+
+  let unquote_level_expr evm trm (* of type level *) b (* of type bool *) : Evd.evar_map * Univ.Universe.t =
+    let evm, l = unquote_level evm trm in
+    let u = Univ.Universe.make l in
+    evm, if unquote_bool b then Univ.Universe.super u else u
+
+
+  let unquote_universe evm trm (* of type universe *) =
+    let levels = List.map unquote_pair (unquote_list trm) in
+    match levels with
+    | [] -> if !strict_unquote_universe_mode then
+        CErrors.user_err ~hdr:"unquote_universe" (str "It is not possible to unquote an empty universe in Strict Unquote Universe Mode.")
+      else
+        let evm, u = Evd.new_univ_variable (Evd.UnivFlexible false) evm in
+        Feedback.msg_info (str"Fresh universe " ++ Universe.pr u ++ str" was added to the context.");
+        evm, u
+    | (l,b)::q -> List.fold_left (fun (evm,u) (l,b) -> let evm, u' = unquote_level_expr evm l b
+                                   in evm, Univ.Universe.sup u u')
+                    (unquote_level_expr evm l b) q
+
+
+  let unquote_universe_instance evm trm (* of type universe_instance *) =
+    let l = unquote_list trm in
+    let evm, l = map_evm unquote_level evm l in
+    evm, Univ.Instance.of_array (Array.of_list l)
+
+
+  let unquote_kn (k : quoted_kernel_name) : Libnames.qualid =
+    Libnames.qualid_of_string (Quoted.clean_name (unquote_string k))
+
+  let unquote_proj (qp : quoted_proj) : (quoted_inductive * quoted_int * quoted_int) =
+    let (h,args) = app_full qp [] in
+    match args with
+    | tyin::tynat::indpars::idx::[] ->
+      let (h',args') = app_full indpars [] in
+      (match args' with
+       | tyind :: tynat :: ind :: n :: [] -> (ind, n, idx)
+       | _ -> bad_term_verb qp "unquote_proj")
+    | _ -> bad_term_verb qp "unquote_proj"
+
+  let unquote_inductive trm =
+    let (h,args) = app_full trm [] in
+    if Constr.equal h tmkInd then
+      match args with
+        nm :: num :: _ ->
+        let s = unquote_string nm in
+        let (dp, nm) = Quoted.split_name s in
+        (try
+           match Nametab.locate (Libnames.make_qualid dp nm) with
+           | Globnames.ConstRef c ->  CErrors.user_err (str "this not an inductive constant. use tConst instead of tInd : " ++ str s)
+           | Globnames.IndRef i -> (fst i, unquote_nat  num)
+           | Globnames.VarRef _ -> CErrors.user_err (str "the constant is a variable. use tVar : " ++ str s)
+           | Globnames.ConstructRef _ -> CErrors.user_err (str "the constant is a consructor. use tConstructor : " ++ str s)
+         with
+           Not_found ->   CErrors.user_err (str "Constant not found : " ++ str s))
+      | _ -> assert false
+    else
+      bad_term_verb trm "non-constructor"
+
+
+  let unquote_ident=unquote_ident
+  let unquote_name=unquote_name
+  let unquote_int=unquote_nat
+  let print_term=print_term
+
+  let inspect_term (t:Constr.t)
+  : (Constr.t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term =
+    let (h,args) = app_full t [] in
+    if Constr.equal h tRel then
+      match args with
+        x :: _ -> ACoq_tRel x
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tVar then
+      match args with
+        x :: _ -> ACoq_tVar x
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tSort then
+      match args with
+        x :: _ -> ACoq_tSort x
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tCast then
+      match args with
+        x :: y :: z :: _ -> ACoq_tCast (x, y, z)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tProd then
+      match args with
+        n :: t :: b :: _ -> ACoq_tProd (n,t,b)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tLambda then
+      match args with
+        n  :: t :: b :: _ -> ACoq_tLambda (n,t,b)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tLetIn then
+      match args with
+        n :: e :: t :: b :: _ -> ACoq_tLetIn (n,e,t,b)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tApp then
+      match args with
+        f::xs::_ -> ACoq_tApp (f, unquote_list xs)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tConst then
+      match args with
+        s::u::_ -> ACoq_tConst (s, u)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tInd then
+      match args with
+        i::u::_ -> ACoq_tInd (i,u)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tConstructor then
+      match args with
+        i::idx::u::_ -> ACoq_tConstruct (i,idx,u)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure: constructor case"))
+    else if Constr.equal h tCase then
+      match args with
+        info::ty::d::brs::_ -> ACoq_tCase (unquote_pair info, ty, d, List.map unquote_pair (unquote_list brs))
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tFix then
+      match args with
+        bds::i::_ ->
+        let unquoteFbd  b  =
+          let (_,args) = app_full b [] in
+          match args with
+          | _(*type*) :: na :: ty :: body :: rarg :: [] ->
+            { adtype = ty;
+              adname = na;
+              adbody = body;
+              rarg
+            }
+          |_ -> raise (Failure " (mkdef must take exactly 5 arguments)")
+        in
+        let lbd = List.map unquoteFbd (unquote_list bds) in
+        ACoq_tFix (lbd, i)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tCoFix then
+      match args with
+        bds::i::_ ->
+        let unquoteFbd  b  =
+          let (_,args) = app_full b [] in
+          match args with
+          | _(*type*) :: na :: ty :: body :: rarg :: [] ->
+            { adtype = ty;
+              adname = na;
+              adbody = body;
+              rarg
+            }
+          |_ -> raise (Failure " (mkdef must take exactly 5 arguments)")
+        in
+        let lbd = List.map unquoteFbd (unquote_list bds) in
+        ACoq_tCoFix (lbd, i)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if Constr.equal h tProj then
+      match args with
+        proj::t::_ -> ACoq_tProj (proj, t)
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+
+    else
+      CErrors.user_err (str"inspect_term: cannot recognize " ++ print_term t ++ str" (maybe you forgot to reduce it?)")
+
+  let unquote_universe_instance=unquote_universe_instance
+
+  let unquote_universe=unquote_universe
+  let unquote_proj=unquote_proj
+  let unquote_inductive=unquote_inductive
+  let unquote_kn=unquote_kn
+  let unquote_cast_kind=unquote_cast_kind
+  let unquote_bool=unquote_bool
+
+
+
+  let mkAnon = mkAnon
+  let mkName = mkName
+  let quote_kn = quote_kn
+  let mkRel = mkRel
+  let mkVar = mkVar
+  let mkEvar = mkEvar
+  let mkSort = mkSort
+  let mkCast = mkCast
+  let mkConst = mkConst
+  let mkProd = mkProd
+
+  let mkLambda = mkLambda
+  let mkApp = mkApp
+
+  let mkLetIn = mkLetIn
+
+  let mkFix = mkFix
+
+  let mkConstruct = mkConstruct
+
+  let mkCoFix = mkCoFix
+
+  let mkInd = mkInd
+
+  let mkCase = mkCase
+
+  let quote_proj = quote_proj
+
+  let mkProj = mkProj
+end
+
+
+
+module CoqLiveDenote = Denote(CoqLiveDenoter)
+
+let denote_term=CoqLiveDenote.denote_term
diff --git a/template-coq/src/constr_quoted.ml b/template-coq/src/constr_quoted.ml
new file mode 100644
index 000000000..e0d85b3be
--- /dev/null
+++ b/template-coq/src/constr_quoted.ml
@@ -0,0 +1,605 @@
+open Univ
+open Entries
+open Names
+open Pp
+open Tm_util
+open Quoted
+
+(** The reifier to Coq values *)
+module ConstrQuoted =
+struct
+  type t = Constr.t
+
+  type quoted_ident = Constr.t (* of type Ast.ident *)
+  type quoted_int = Constr.t (* of type nat *)
+  type quoted_bool = Constr.t (* of type bool *)
+  type quoted_name = Constr.t (* of type Ast.name *)
+  type quoted_sort = Constr.t (* of type Ast.universe *)
+  type quoted_cast_kind = Constr.t  (* of type Ast.cast_kind *)
+  type quoted_kernel_name = Constr.t (* of type Ast.kername *)
+  type quoted_inductive = Constr.t (* of type Ast.inductive *)
+  type quoted_proj = Constr.t (* of type Ast.projection *)
+  type quoted_global_reference = Constr.t (* of type Ast.global_reference *)
+
+  type quoted_sort_family = Constr.t (* of type Ast.sort_family *)
+  type quoted_constraint_type = Constr.t (* of type univ.constraint_type *)
+  type quoted_univ_constraint = Constr.t (* of type univ.univ_constraint *)
+  type quoted_univ_constraints = Constr.t (* of type univ.constraints *)
+  type quoted_univ_instance = Constr.t (* of type univ.universe_instance *)
+  type quoted_univ_context = Constr.t (* of type univ.universe_context *)
+  type quoted_inductive_universes = Constr.t (* of type univ.universe_context *)
+
+  type quoted_mind_params = Constr.t (* of type list (Ast.ident * list (ident * local_entry)local_entry) *)
+  type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list
+  type quoted_definition_entry = t * t option * quoted_univ_context
+  type quoted_mind_entry = Constr.t (* of type Ast.mutual_inductive_entry *)
+  type quoted_mind_finiteness = Constr.t (* of type Ast.mutual_inductive_entry ?? *)
+  type quoted_entry = Constr.t (* of type option (constant_entry + mutual_inductive_entry) *)
+
+  type quoted_context_decl = Constr.t (* in Ast *)
+  type quoted_context = Constr.t (* in Ast *)
+
+  type quoted_one_inductive_body = Constr.t (* of type Ast.one_inductive_body *)
+  type quoted_mutual_inductive_body = Constr.t (* of type Ast.mutual_inductive_body *)
+  type quoted_constant_body = Constr.t (* of type Ast.constant_body *)
+  type quoted_global_decl = Constr.t (* of type Ast.global_decl *)
+  type quoted_global_declarations = Constr.t (* of type Ast.global_declarations *)
+  type quoted_program = Constr.t (* of type Ast.program *)
+
+(*
+  type quoted_reduction_strategy = Constr.t (* of type Ast.reductionStrategy *)
+*)
+
+  let resolve_symbol (path : string list) (tm : string) : Constr.t =
+    gen_constant_in_modules contrib_name [path] tm
+
+  let resolve_symbol_p (path : string list) (tm : string) : Globnames.global_reference =
+    Coqlib.gen_reference_in_modules contrib_name [path] tm
+
+  let pkg_datatypes = ["Coq";"Init";"Datatypes"]
+  let pkg_string = ["Coq";"Strings";"String"]
+  let pkg_base_reify = ["Template";"BasicAst"]
+  let pkg_reify = ["Template";"Ast"]
+  let pkg_template_monad = ["Template";"TemplateMonad"]
+  let pkg_univ = ["Template";"kernel";"univ"]
+  let pkg_level = ["Template";"kernel";"univ";"Level"]
+  let pkg_variance = ["Template";"kernel";"univ";"Variance"]
+  let pkg_ugraph = ["Template";"kernel";"uGraph"]
+  let ext_pkg_univ s = List.append pkg_univ [s]
+
+  let r_base_reify = resolve_symbol pkg_base_reify
+  let r_reify = resolve_symbol pkg_reify
+  let r_template_monad = resolve_symbol pkg_template_monad
+  let r_template_monad_p = resolve_symbol_p pkg_template_monad
+
+  let tString = resolve_symbol pkg_string "String"
+  let tEmptyString = resolve_symbol pkg_string "EmptyString"
+  let tO = resolve_symbol pkg_datatypes "O"
+  let tS = resolve_symbol pkg_datatypes "S"
+  let tnat = resolve_symbol pkg_datatypes "nat"
+  let ttrue = resolve_symbol pkg_datatypes "true"
+  let cSome = resolve_symbol pkg_datatypes "Some"
+  let cNone = resolve_symbol pkg_datatypes "None"
+  let tfalse = resolve_symbol pkg_datatypes "false"
+  let unit_tt = resolve_symbol pkg_datatypes "tt"
+  let tAscii = resolve_symbol ["Coq";"Strings";"Ascii"] "Ascii"
+  let tlist = resolve_symbol pkg_datatypes "list"
+  let c_nil = resolve_symbol pkg_datatypes "nil"
+  let c_cons = resolve_symbol pkg_datatypes "cons"
+  let prod_type = resolve_symbol pkg_datatypes "prod"
+  let sum_type = resolve_symbol pkg_datatypes "sum"
+  let option_type = resolve_symbol pkg_datatypes "option"
+  let bool_type = resolve_symbol pkg_datatypes "bool"
+  let cInl = resolve_symbol pkg_datatypes "inl"
+  let cInr = resolve_symbol pkg_datatypes "inr"
+  let prod a b = Constr.mkApp (prod_type, [| a ; b |])
+  let c_pair = resolve_symbol pkg_datatypes "pair"
+  let pair a b f s = Constr.mkApp (c_pair, [| a ; b ; f ; s |])
+
+    (* reify the constructors in Template.Ast.v, which are the building blocks of reified terms *)
+  let nAnon = r_base_reify "nAnon"
+  let nNamed = r_base_reify "nNamed"
+  let kVmCast = r_base_reify "VmCast"
+  let kNative = r_base_reify "NativeCast"
+  let kCast = r_base_reify "Cast"
+  let kRevertCast = r_base_reify "RevertCast"
+  let lProp = resolve_symbol pkg_level "lProp"
+  let lSet = resolve_symbol pkg_level "lSet"
+  let sfProp = r_base_reify "InProp"
+  let sfSet = r_base_reify "InSet"
+  let sfType = r_base_reify "InType"
+  let tident = r_base_reify "ident"
+  let tname = r_base_reify "name"
+  let tIndTy = r_base_reify "inductive"
+  let tmkInd = r_base_reify "mkInd"
+  let tsort_family = r_base_reify "sort_family"
+  let tmkdecl = r_reify "mkdecl"
+  let (tTerm,tRel,tVar,tEvar,tSort,tCast,tProd,
+       tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tCoFix,tProj) =
+    (r_reify "term", r_reify "tRel", r_reify "tVar", r_reify "tEvar",
+     r_reify "tSort", r_reify "tCast", r_reify "tProd", r_reify "tLambda",
+     r_reify "tLetIn", r_reify "tApp", r_reify "tCase", r_reify "tFix",
+     r_reify "tConstruct", r_reify "tConst", r_reify "tInd", r_reify "tCoFix", r_reify "tProj")
+
+  let tlevel = resolve_symbol pkg_level "t"
+  let tLevel = resolve_symbol pkg_level "Level"
+  let tLevelVar = resolve_symbol pkg_level "Var"
+  let tunivLe = resolve_symbol (ext_pkg_univ "ConstraintType") "Le"
+  let tunivLt = resolve_symbol (ext_pkg_univ "ConstraintType") "Lt"
+  let tunivEq = resolve_symbol (ext_pkg_univ "ConstraintType") "Eq"
+  (* let tunivcontext = resolve_symbol pkg_univ "universe_context" *)
+  let tVariance = resolve_symbol pkg_variance "t"
+  let cIrrelevant = resolve_symbol pkg_variance "Irrelevant"
+  let cCovariant = resolve_symbol pkg_variance "Covariant"
+  let cInvariant = resolve_symbol pkg_variance "Invariant"
+  let cMonomorphic_ctx = resolve_symbol pkg_univ "Monomorphic_ctx"
+  let cPolymorphic_ctx = resolve_symbol pkg_univ "Polymorphic_ctx"
+  let cCumulative_ctx = resolve_symbol pkg_univ "Cumulative_ctx"
+  let tUContext = resolve_symbol (ext_pkg_univ "UContext") "t"
+  let tUContextmake = resolve_symbol (ext_pkg_univ "UContext") "make"
+  (* let tConstraintSetempty = resolve_symbol (ext_pkg_univ "ConstraintSet") "empty" *)
+  let tConstraintSetempty = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "ConstraintSet") "empty")
+  let tConstraintSetadd = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "ConstraintSet") "add")
+  let tmake_univ_constraint = resolve_symbol pkg_univ "make_univ_constraint"
+  let tinit_graph = resolve_symbol pkg_ugraph "init_graph"
+  let tadd_global_constraints = resolve_symbol pkg_ugraph  "add_global_constraints"
+
+  let (tdef,tmkdef) = (r_base_reify "def", r_base_reify "mkdef")
+  let (tLocalDef,tLocalAssum,tlocal_entry) = (r_reify "LocalDef", r_reify "LocalAssum", r_reify "local_entry")
+
+  let (cFinite,cCoFinite,cBiFinite) = (r_reify "Finite", r_reify "CoFinite", r_reify "BiFinite")
+  let tone_inductive_body = r_reify "one_inductive_body"
+  let tBuild_one_inductive_body = r_reify "Build_one_inductive_body"
+  let tBuild_mutual_inductive_body = r_reify "Build_mutual_inductive_body"
+  let tBuild_constant_body = r_reify "Build_constant_body"
+  let tglobal_decl = r_reify "global_decl"
+  let tConstantDecl = r_reify "ConstantDecl"
+  let tInductiveDecl = r_reify "InductiveDecl"
+  let tglobal_declarations = r_reify "global_declarations"
+
+  let tcontext_decl = r_reify "context_decl"
+  let tcontext = r_reify "context"
+
+  let tMutual_inductive_entry = r_reify "mutual_inductive_entry"
+  let tOne_inductive_entry = r_reify "one_inductive_entry"
+  let tBuild_mutual_inductive_entry = r_reify "Build_mutual_inductive_entry"
+  let tBuild_one_inductive_entry = r_reify "Build_one_inductive_entry"
+  let tConstant_entry = r_reify "constant_entry"
+  let cParameterEntry = r_reify "ParameterEntry"
+  let cDefinitionEntry = r_reify "DefinitionEntry"
+  let cParameter_entry = r_reify "Build_parameter_entry"
+  let cDefinition_entry = r_reify "Build_definition_entry"
+
+  let (tcbv, tcbn, thnf, tall, tlazy, tunfold) = (r_template_monad "cbv", r_template_monad "cbn", r_template_monad "hnf", r_template_monad "all", r_template_monad "lazy", r_template_monad "unfold")
+
+  let (tglobal_reference, tConstRef, tIndRef, tConstructRef) =
+    (r_base_reify "global_reference", r_base_reify "ConstRef", r_base_reify "IndRef", r_base_reify "ConstructRef")
+
+  (* let pkg_specif = ["Coq";"Init";"Specif"] *)
+  (* let texistT = resolve_symbol pkg_specif "existT" *)
+  (* let texistT_typed_term = r_template_monad "existT_typed_term" *)
+  let texistT_typed_term = r_template_monad_p "existT_typed_term"
+
+  let unquote_pair trm =
+    let (h,args) = app_full trm [] in
+    if Constr.equal h c_pair then
+      match args with
+        _ :: _ :: x :: y :: [] -> (x, y)
+      | _ -> bad_term_verb trm "unquote_pair"
+    else
+      not_supported_verb trm "unquote_pair"
+
+  let rec unquote_list trm =
+    let (h,args) = app_full trm [] in
+    if Constr.equal h c_nil then
+      []
+    else if Constr.equal h c_cons then
+      match args with
+        _ :: x :: xs :: [] -> x :: unquote_list xs
+      | _ -> bad_term_verb trm "unquote_list"
+    else
+      not_supported_verb trm "unquote_list"
+
+  (* Unquote Coq nat to OCaml int *)
+  let rec unquote_nat trm =
+    let (h,args) = app_full trm [] in
+    if Constr.equal h tO then
+      0
+    else if Constr.equal h tS then
+      match args with
+        n :: [] -> 1 + unquote_nat n
+      | _ -> bad_term_verb trm "unquote_nat"
+    else
+      not_supported_verb trm "unquote_nat"
+
+  let unquote_bool trm =
+    if Constr.equal trm ttrue then
+      true
+    else if Constr.equal trm tfalse then
+      false
+    else not_supported_verb trm "from_bool"
+
+  let unquote_char trm =
+    let (h,args) = app_full trm [] in
+    if Constr.equal h tAscii then
+      match args with
+        a :: b :: c :: d :: e :: f :: g :: h :: [] ->
+        let bits = List.rev [a;b;c;d;e;f;g;h] in
+        let v = List.fold_left (fun a n -> (a lsl 1) lor if unquote_bool n then 1 else 0) 0 bits in
+        char_of_int v
+      | _ -> bad_term_verb trm "unquote_char"
+    else
+      not_supported trm
+
+  let unquote_string trm =
+    let rec go n trm =
+      let (h,args) = app_full trm [] in
+      if Constr.equal h tEmptyString then
+        Bytes.create n
+      else if Constr.equal h tString then
+        match args with
+          c :: s :: [] ->
+          let res = go (n + 1) s in
+          let _ = Bytes.set res n (unquote_char c) in
+          res
+        | _ -> bad_term_verb trm "unquote_string"
+      else
+        not_supported_verb trm "unquote_string"
+    in
+    Bytes.to_string (go 0 trm)
+
+
+
+  let to_coq_list typ =
+    let the_nil = Constr.mkApp (c_nil, [| typ |]) in
+    let rec to_list (ls : Constr.t list) : Constr.t =
+      match ls with
+	[] -> the_nil
+      | l :: ls ->
+	Constr.mkApp (c_cons, [| typ ; l ; to_list ls |])
+    in to_list
+
+  let quote_option ty = function
+    | Some tm -> Constr.mkApp (cSome, [|ty; tm|])
+    | None -> Constr.mkApp (cNone, [|ty|])
+
+  (* Quote OCaml int to Coq nat *)
+  let quote_int =
+    (* the cache is global but only accessible through quote_int *)
+    let cache = Hashtbl.create 10 in
+    let rec recurse i =
+      try Hashtbl.find cache i
+      with
+	Not_found ->
+	  if i = 0 then
+	    let result = tO in
+	    let _ = Hashtbl.add cache i result in
+	    result
+	  else
+	    let result = Constr.mkApp (tS, [| recurse (i - 1) |]) in
+	    let _ = Hashtbl.add cache i result in
+	    result
+    in
+    fun i ->
+    if i >= 0 then recurse i else
+      CErrors.anomaly Pp.(str "Negative int can't be unquoted to nat.")
+
+  let quote_bool b =
+    if b then ttrue else tfalse
+
+  let quote_char i =
+    Constr.mkApp (tAscii, Array.of_list (List.map (fun m -> quote_bool ((i land m) = m))
+					 (List.rev [128;64;32;16;8;4;2;1])))
+
+  let chars = Array.init 255 quote_char
+
+  let quote_char c = chars.(int_of_char c)
+
+  let string_hash = Hashtbl.create 420
+
+  let to_string s =
+    let len = String.length s in
+    let rec go from acc =
+      if from < 0 then acc
+      else
+        let term = Constr.mkApp (tString, [| quote_char (String.get s from) ; acc |]) in
+        go (from - 1) term
+    in
+    go (len - 1) tEmptyString
+
+  let quote_string s =
+    try Hashtbl.find string_hash s
+    with Not_found ->
+      let term = to_string s in
+      Hashtbl.add string_hash s term; term
+
+  let quote_ident i =
+    let s = Names.Id.to_string i in
+    quote_string s
+
+  let quote_name n =
+    match n with
+      Names.Name id -> Constr.mkApp (nNamed, [| quote_ident id |])
+    | Names.Anonymous -> nAnon
+
+  let quote_cast_kind k =
+    match k with
+      Constr.VMcast -> kVmCast
+    | Constr.DEFAULTcast -> kCast
+    | Constr.REVERTcast -> kRevertCast
+    | Constr.NATIVEcast -> kNative
+
+  let string_of_level s =
+    to_string (Univ.Level.to_string s)
+
+  let quote_level l =
+    let open Univ in
+    debug (fun () -> str"quote_level " ++ Level.pr l);
+    if Level.is_prop l then lProp
+    else if Level.is_set l then lSet
+    else match Level.var_index l with
+         | Some x -> Constr.mkApp (tLevelVar, [| quote_int x |])
+         | None -> Constr.mkApp (tLevel, [| string_of_level l|])
+
+  let quote_universe s =
+    let levels = Universe.map (fun (l,i) -> pair tlevel bool_type (quote_level l) (if i > 0 then ttrue else tfalse)) s in
+    to_coq_list (prod tlevel bool_type) levels
+
+  (* todo : can be deduced from quote_level, hence shoud be in the Reify module *)
+  let quote_univ_instance u =
+    let arr = Univ.Instance.to_array u in
+    to_coq_list tlevel (CArray.map_to_list quote_level arr)
+
+  let quote_constraint_type (c : Univ.constraint_type) =
+    match c with
+    | Lt -> tunivLt
+    | Le -> tunivLe
+    | Eq -> tunivEq
+
+  let quote_univ_constraint ((l1, ct, l2) : Univ.univ_constraint) =
+    let l1 = quote_level l1 in
+    let l2 = quote_level l2 in
+    let ct = quote_constraint_type ct in
+    Constr.mkApp (tmake_univ_constraint, [| l1; ct; l2 |])
+
+  let quote_univ_constraints const =
+    let const = Univ.Constraint.elements const in
+    List.fold_left (fun tm c ->
+        let c = quote_univ_constraint c in
+        Constr.mkApp (tConstraintSetadd, [| c; tm|])
+      ) tConstraintSetempty const
+
+  let quote_variance v =
+    match v with
+    | Univ.Variance.Irrelevant -> cIrrelevant
+    | Univ.Variance.Covariant -> cCovariant
+    | Univ.Variance.Invariant -> cInvariant
+
+  let quote_cuminfo_variance var =
+    let var_list = CArray.map_to_list quote_variance var in
+    to_coq_list tVariance var_list
+
+  let quote_ucontext inst const =
+    let inst' = quote_univ_instance inst in
+    let const' = quote_univ_constraints const in
+    Constr.mkApp (tUContextmake, [|inst'; const'|])
+
+  let quote_univ_context uctx =
+    let inst = Univ.UContext.instance uctx in
+    let const = Univ.UContext.constraints uctx in
+    Constr.mkApp (cMonomorphic_ctx, [| quote_ucontext inst const |])
+
+  let quote_cumulative_univ_context cumi =
+    let uctx = Univ.CumulativityInfo.univ_context cumi in
+    let inst = Univ.UContext.instance uctx in
+    let const = Univ.UContext.constraints uctx in
+    let var = Univ.CumulativityInfo.variance cumi in
+    let uctx' = quote_ucontext inst const in
+    let var' = quote_cuminfo_variance var in
+    let listvar = Constr.mkApp (tlist, [| tVariance |]) in
+    let cumi' = pair tUContext listvar uctx' var' in
+    Constr.mkApp (cCumulative_ctx, [| cumi' |])
+
+  let quote_abstract_univ_context_aux uctx =
+    let inst = Univ.UContext.instance uctx in
+    let const = Univ.UContext.constraints uctx in
+    Constr.mkApp (cPolymorphic_ctx, [| quote_ucontext inst const |])
+
+  let quote_abstract_univ_context uctx =
+    let uctx = Univ.AUContext.repr uctx in
+    quote_abstract_univ_context_aux uctx
+
+  let quote_inductive_universes uctx =
+    match uctx with
+    | Monomorphic_ind_entry uctx -> quote_univ_context (Univ.ContextSet.to_context uctx)
+    | Polymorphic_ind_entry uctx -> quote_abstract_univ_context_aux uctx
+    | Cumulative_ind_entry info ->
+      quote_abstract_univ_context_aux (CumulativityInfo.univ_context info) (* FIXME lossy *)
+
+  let quote_ugraph (g : UGraph.t) =
+    let inst' = quote_univ_instance Univ.Instance.empty in
+    let const' = quote_univ_constraints (UGraph.constraints_of_universes g) in
+    let uctx = Constr.mkApp (tUContextmake, [|inst' ; const'|]) in
+    Constr.mkApp (tadd_global_constraints, [|Constr.mkApp (cMonomorphic_ctx, [| uctx |]); tinit_graph|])
+
+  let quote_sort s =
+    quote_universe (Sorts.univ_of_sort s)
+
+  let quote_sort_family = function
+    | Sorts.InProp -> sfProp
+    | Sorts.InSet -> sfSet
+    | Sorts.InType -> sfType
+
+  let quote_context_decl na b t =
+    Constr.mkApp (tmkdecl, [| na; quote_option tTerm b; t |])
+
+  let quote_context ctx =
+    to_coq_list tcontext_decl ctx
+
+  let mk_ctor_list =
+    let ctor_list =
+      let ctor_info_typ = prod (prod tident tTerm) tnat in
+      to_coq_list ctor_info_typ
+    in
+    fun ls ->
+    let ctors = List.map (fun (a,b,c) -> pair (prod tident tTerm) tnat
+				              (pair tident tTerm a b) c) ls in
+    ctor_list ctors
+
+  let mk_proj_list d =
+    to_coq_list (prod tident tTerm)
+                (List.map (fun (a, b) -> pair tident tTerm a b) d)
+
+  let quote_inductive (kn, i) =
+    Constr.mkApp (tmkInd, [| kn; i |])
+
+  let rec seq f t =
+    if f < t then f :: seq (f + 1) t
+    else []
+
+  let quote_proj ind pars args =
+    pair (prod tIndTy tnat) tnat (pair tIndTy tnat ind pars) args
+
+  let mkAnon = nAnon
+  let mkName id = Constr.mkApp (nNamed, [| id |])
+  let quote_kn kn = quote_string (KerName.to_string kn)
+
+  let mkRel i = Constr.mkApp (tRel, [| i |])
+  let mkVar id = Constr.mkApp (tVar, [| id |])
+  let mkEvar n args = Constr.mkApp (tEvar, [| n; to_coq_list tTerm (Array.to_list args) |])
+  let mkSort s = Constr.mkApp (tSort, [| s |])
+  let mkCast c k t = Constr.mkApp (tCast, [| c ; k ; t |])
+  let mkConst kn u = Constr.mkApp (tConst, [| kn ; u |])
+  let mkProd na t b =
+    Constr.mkApp (tProd, [| na ; t ; b |])
+  let mkLambda na t b =
+    Constr.mkApp (tLambda, [| na ; t ; b |])
+  let mkApp f xs =
+    Constr.mkApp (tApp, [| f ; to_coq_list tTerm (Array.to_list xs) |])
+
+  let mkLetIn na t t' b =
+    Constr.mkApp (tLetIn, [| na ; t ; t' ; b |])
+
+  let mkFix ((a,b),(ns,ts,ds)) =
+    let mk_fun xs i =
+      Constr.mkApp (tmkdef, [| tTerm ; Array.get ns i ;
+                             Array.get ts i ; Array.get ds i ; Array.get a i |]) :: xs
+    in
+    let defs = List.fold_left mk_fun [] (seq 0 (Array.length a)) in
+    let block = to_coq_list (Constr.mkApp (tdef, [| tTerm |])) (List.rev defs) in
+    Constr.mkApp (tFix, [| block ; b |])
+
+  let mkConstruct (ind, i) u =
+    Constr.mkApp (tConstructor, [| ind ; i ; u |])
+
+  let mkCoFix (a,(ns,ts,ds)) =
+    let mk_fun xs i =
+      Constr.mkApp (tmkdef, [| tTerm ; Array.get ns i ;
+                             Array.get ts i ; Array.get ds i ; tO |]) :: xs
+    in
+    let defs = List.fold_left mk_fun [] (seq 0 (Array.length ns)) in
+    let block = to_coq_list (Constr.mkApp (tdef, [| tTerm |])) (List.rev defs) in
+    Constr.mkApp (tCoFix, [| block ; a |])
+
+  let mkInd i u = Constr.mkApp (tInd, [| i ; u |])
+
+  let mkCase (ind, npar) nargs p c brs =
+    let info = pair tIndTy tnat ind npar in
+    let branches = List.map2 (fun br nargs ->  pair tnat tTerm nargs br) brs nargs in
+    let tl = prod tnat tTerm in
+    Constr.mkApp (tCase, [| info ; p ; c ; to_coq_list tl branches |])
+
+  let mkProj kn t =
+    Constr.mkApp (tProj, [| kn; t |])
+
+  let mk_one_inductive_body (a, b, c, d, e) =
+    let c = to_coq_list tsort_family c in
+    let d = mk_ctor_list d in
+    let e = mk_proj_list e in
+    Constr.mkApp (tBuild_one_inductive_body, [| a; b; c; d; e |])
+
+  let mk_mutual_inductive_body npars params inds uctx =
+    let inds = to_coq_list tone_inductive_body inds in
+    Constr.mkApp (tBuild_mutual_inductive_body, [|npars; params; inds; uctx|])
+
+  let mk_constant_body ty tm uctx =
+    let tm = quote_option tTerm tm in
+    Constr.mkApp (tBuild_constant_body, [|ty; tm; uctx|])
+
+  let mk_inductive_decl kn mind =
+    Constr.mkApp (tInductiveDecl, [|kn; mind|])
+
+  let mk_constant_decl kn bdy =
+    Constr.mkApp (tConstantDecl, [|kn; bdy|])
+
+  let empty_global_declartions =
+    Constr.mkApp (c_nil, [| tglobal_decl |])
+
+  let add_global_decl d l =
+    Constr.mkApp (c_cons, [|tglobal_decl; d; l|])
+
+  let mk_program = pair tglobal_declarations tTerm
+
+  let quote_mind_finiteness (f: Declarations.recursivity_kind) =
+    match f with
+    | Declarations.Finite -> cFinite
+    | Declarations.CoFinite -> cCoFinite
+    | Declarations.BiFinite -> cBiFinite
+
+  let make_one_inductive_entry (iname, arity, templatePoly, consnames, constypes) =
+    let consnames = to_coq_list tident consnames in
+    let constypes = to_coq_list tTerm constypes in
+    Constr.mkApp (tBuild_one_inductive_entry, [| iname; arity; templatePoly; consnames; constypes |])
+
+  let quote_mind_params l =
+    let pair i l = pair tident tlocal_entry i l in
+    let map (id, ob) =
+      match ob with
+      | Left b -> pair id (Constr.mkApp (tLocalDef,[|b|]))
+      | Right t -> pair id (Constr.mkApp (tLocalAssum,[|t|]))
+    in
+    let the_prod = Constr.mkApp (prod_type,[|tident; tlocal_entry|]) in
+    to_coq_list the_prod (List.map map l)
+
+  let quote_mutual_inductive_entry (mf, mp, is, mpol) =
+    let is = to_coq_list tOne_inductive_entry (List.map make_one_inductive_entry is) in
+    let mpr = Constr.mkApp (cNone, [|bool_type|]) in
+    let mr = Constr.mkApp (cNone, [|Constr.mkApp (option_type, [|tident|])|])  in
+    Constr.mkApp (tBuild_mutual_inductive_entry, [| mr; mf; mp; is; mpol; mpr |])
+
+
+  let quote_constant_entry (ty, body, ctx) =
+    match body with
+    | None ->
+      Constr.mkApp (cParameterEntry, [| Constr.mkApp (cParameter_entry, [|ty; ctx|]) |])
+    | Some body ->
+      Constr.mkApp (cDefinitionEntry,
+                  [| Constr.mkApp (cDefinition_entry, [|ty;body;ctx;tfalse (*FIXME*)|]) |])
+
+  let quote_entry decl =
+    let opType = Constr.mkApp(sum_type, [|tConstant_entry;tMutual_inductive_entry|]) in
+    let mkSome c t = Constr.mkApp (cSome, [|opType; Constr.mkApp (c, [|tConstant_entry;tMutual_inductive_entry; t|] )|]) in
+    let mkSomeDef = mkSome cInl in
+    let mkSomeInd  = mkSome cInr in
+    match decl with
+    | Some (Left centry) -> mkSomeDef (quote_constant_entry centry)
+    | Some (Right mind) -> mkSomeInd mind
+    | None -> Constr.mkApp (cNone, [| opType |])
+
+
+  let quote_global_reference : Globnames.global_reference -> quoted_global_reference = function
+    | Globnames.VarRef _ -> CErrors.user_err (str "VarRef unsupported")
+    | Globnames.ConstRef c ->
+       let kn = quote_kn (Names.Constant.canonical c) in
+       Constr.mkApp (tConstRef, [|kn|])
+    | Globnames.IndRef (i, n) ->
+       let kn = quote_kn (Names.MutInd.canonical i) in
+       let n = quote_int n in
+       Constr.mkApp (tIndRef, [|quote_inductive (kn ,n)|])
+    | Globnames.ConstructRef ((i, n), k) ->
+       let kn = quote_kn (Names.MutInd.canonical i) in
+       let n = quote_int n in
+       let k = (quote_int (k - 1)) in
+       Constr.mkApp (tConstructRef, [|quote_inductive (kn ,n); k|])
+
+end
diff --git a/template-coq/src/constr_quoter.ml b/template-coq/src/constr_quoter.ml
index 81740d03c..7a6610777 100644
--- a/template-coq/src/constr_quoter.ml
+++ b/template-coq/src/constr_quoter.ml
@@ -2,186 +2,15 @@ open Univ
 open Entries
 open Names
 open Pp
-
+open Tm_util
+open Quoted
 open Quoter
-
-let contrib_name = "template-coq"
-
-let gen_constant_in_modules locstr dirs s =
-  Universes.constr_of_global (Coqlib.gen_reference_in_modules locstr dirs s)
+open Constr_quoted
 
 (** The reifier to Coq values *)
 module TemplateCoqQuoter =
 struct
-  type t = Constr.t
-
-  type quoted_ident = Constr.t (* of type Ast.ident *)
-  type quoted_int = Constr.t (* of type nat *)
-  type quoted_bool = Constr.t (* of type bool *)
-  type quoted_name = Constr.t (* of type Ast.name *)
-  type quoted_sort = Constr.t (* of type Ast.universe *)
-  type quoted_cast_kind = Constr.t  (* of type Ast.cast_kind *)
-  type quoted_kernel_name = Constr.t (* of type Ast.kername *)
-  type quoted_inductive = Constr.t (* of type Ast.inductive *)
-  type quoted_proj = Constr.t (* of type Ast.projection *)
-  type quoted_global_reference = Constr.t (* of type Ast.global_reference *)
-
-  type quoted_sort_family = Constr.t (* of type Ast.sort_family *)
-  type quoted_constraint_type = Constr.t (* of type univ.constraint_type *)
-  type quoted_univ_constraint = Constr.t (* of type univ.univ_constraint *)
-  type quoted_univ_constraints = Constr.t (* of type univ.constraints *)
-  type quoted_univ_instance = Constr.t (* of type univ.universe_instance *)
-  type quoted_univ_context = Constr.t (* of type univ.universe_context *)
-  type quoted_inductive_universes = Constr.t (* of type univ.universe_context *)
-
-  type quoted_mind_params = Constr.t (* of type list (Ast.ident * list (ident * local_entry)local_entry) *)
-  type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list
-  type quoted_definition_entry = t * t option * quoted_univ_context
-  type quoted_mind_entry = Constr.t (* of type Ast.mutual_inductive_entry *)
-  type quoted_mind_finiteness = Constr.t (* of type Ast.mutual_inductive_entry ?? *)
-  type quoted_entry = Constr.t (* of type option (constant_entry + mutual_inductive_entry) *)
-
-  type quoted_context_decl = Constr.t (* in Ast *)
-  type quoted_context = Constr.t (* in Ast *)
-
-  type quoted_one_inductive_body = Constr.t (* of type Ast.one_inductive_body *)
-  type quoted_mutual_inductive_body = Constr.t (* of type Ast.mutual_inductive_body *)
-  type quoted_constant_body = Constr.t (* of type Ast.constant_body *)
-  type quoted_global_decl = Constr.t (* of type Ast.global_decl *)
-  type quoted_global_declarations = Constr.t (* of type Ast.global_declarations *)
-  type quoted_program = Constr.t (* of type Ast.program *)
-
-  type quoted_reduction_strategy = Constr.t (* of type Ast.reductionStrategy *)
-
-  let resolve_symbol (path : string list) (tm : string) : Constr.t =
-    gen_constant_in_modules contrib_name [path] tm
-
-  let resolve_symbol_p (path : string list) (tm : string) : global_reference =
-    Coqlib.gen_reference_in_modules contrib_name [path] tm
-
-  let pkg_datatypes = ["Coq";"Init";"Datatypes"]
-  let pkg_string = ["Coq";"Strings";"String"]
-  let pkg_base_reify = ["Template";"BasicAst"]
-  let pkg_reify = ["Template";"Ast"]
-  let pkg_template_monad = ["Template";"TemplateMonad"]
-  let pkg_univ = ["Template";"kernel";"univ"]
-  let pkg_level = ["Template";"kernel";"univ";"Level"]
-  let pkg_variance = ["Template";"kernel";"univ";"Variance"]
-  let pkg_ugraph = ["Template";"kernel";"uGraph"]
-  let ext_pkg_univ s = List.append pkg_univ [s]
-
-  let r_base_reify = resolve_symbol pkg_base_reify
-  let r_reify = resolve_symbol pkg_reify
-  let r_template_monad = resolve_symbol pkg_template_monad
-  let r_template_monad_p = resolve_symbol_p pkg_template_monad
-
-  let tString = resolve_symbol pkg_string "String"
-  let tEmptyString = resolve_symbol pkg_string "EmptyString"
-  let tO = resolve_symbol pkg_datatypes "O"
-  let tS = resolve_symbol pkg_datatypes "S"
-  let tnat = resolve_symbol pkg_datatypes "nat"
-  let ttrue = resolve_symbol pkg_datatypes "true"
-  let cSome = resolve_symbol pkg_datatypes "Some"
-  let cNone = resolve_symbol pkg_datatypes "None"
-  let tfalse = resolve_symbol pkg_datatypes "false"
-  let unit_tt = resolve_symbol pkg_datatypes "tt"
-  let tAscii = resolve_symbol ["Coq";"Strings";"Ascii"] "Ascii"
-  let tlist = resolve_symbol pkg_datatypes "list"
-  let c_nil = resolve_symbol pkg_datatypes "nil"
-  let c_cons = resolve_symbol pkg_datatypes "cons"
-  let prod_type = resolve_symbol pkg_datatypes "prod"
-  let sum_type = resolve_symbol pkg_datatypes "sum"
-  let option_type = resolve_symbol pkg_datatypes "option"
-  let bool_type = resolve_symbol pkg_datatypes "bool"
-  let cInl = resolve_symbol pkg_datatypes "inl"
-  let cInr = resolve_symbol pkg_datatypes "inr"
-  let prod a b = Constr.mkApp (prod_type, [| a ; b |])
-  let c_pair = resolve_symbol pkg_datatypes "pair"
-  let pair a b f s = Constr.mkApp (c_pair, [| a ; b ; f ; s |])
-
-    (* reify the constructors in Template.Ast.v, which are the building blocks of reified terms *)
-  let nAnon = r_base_reify "nAnon"
-  let nNamed = r_base_reify "nNamed"
-  let kVmCast = r_base_reify "VmCast"
-  let kNative = r_base_reify "NativeCast"
-  let kCast = r_base_reify "Cast"
-  let kRevertCast = r_base_reify "RevertCast"
-  let lProp = resolve_symbol pkg_level "lProp"
-  let lSet = resolve_symbol pkg_level "lSet"
-  let sfProp = r_base_reify "InProp"
-  let sfSet = r_base_reify "InSet"
-  let sfType = r_base_reify "InType"
-  let tident = r_base_reify "ident"
-  let tname = r_base_reify "name"
-  let tIndTy = r_base_reify "inductive"
-  let tmkInd = r_base_reify "mkInd"
-  let tsort_family = r_base_reify "sort_family"
-  let tmkdecl = r_reify "mkdecl"
-  let (tTerm,tRel,tVar,tEvar,tSort,tCast,tProd,
-       tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tCoFix,tProj) =
-    (r_reify "term", r_reify "tRel", r_reify "tVar", r_reify "tEvar",
-     r_reify "tSort", r_reify "tCast", r_reify "tProd", r_reify "tLambda",
-     r_reify "tLetIn", r_reify "tApp", r_reify "tCase", r_reify "tFix",
-     r_reify "tConstruct", r_reify "tConst", r_reify "tInd", r_reify "tCoFix", r_reify "tProj")
-
-  let tlevel = resolve_symbol pkg_level "t"
-  let tLevel = resolve_symbol pkg_level "Level"
-  let tLevelVar = resolve_symbol pkg_level "Var"
-  let tunivLe = resolve_symbol (ext_pkg_univ "ConstraintType") "Le"
-  let tunivLt = resolve_symbol (ext_pkg_univ "ConstraintType") "Lt"
-  let tunivEq = resolve_symbol (ext_pkg_univ "ConstraintType") "Eq"
-  (* let tunivcontext = resolve_symbol pkg_univ "universe_context" *)
-  let tVariance = resolve_symbol pkg_variance "t"
-  let cIrrelevant = resolve_symbol pkg_variance "Irrelevant"
-  let cCovariant = resolve_symbol pkg_variance "Covariant"
-  let cInvariant = resolve_symbol pkg_variance "Invariant"
-  let cMonomorphic_ctx = resolve_symbol pkg_univ "Monomorphic_ctx"
-  let cPolymorphic_ctx = resolve_symbol pkg_univ "Polymorphic_ctx"
-  let cCumulative_ctx = resolve_symbol pkg_univ "Cumulative_ctx"
-  let tUContext = resolve_symbol (ext_pkg_univ "UContext") "t"
-  let tUContextmake = resolve_symbol (ext_pkg_univ "UContext") "make"
-  (* let tConstraintSetempty = resolve_symbol (ext_pkg_univ "ConstraintSet") "empty" *)
-  let tConstraintSetempty = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "ConstraintSet") "empty")
-  let tConstraintSetadd = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "ConstraintSet") "add")
-  let tmake_univ_constraint = resolve_symbol pkg_univ "make_univ_constraint"
-  let tinit_graph = resolve_symbol pkg_ugraph "init_graph"
-  let tadd_global_constraints = resolve_symbol pkg_ugraph  "add_global_constraints"
-
-  let (tdef,tmkdef) = (r_base_reify "def", r_base_reify "mkdef")
-  let (tLocalDef,tLocalAssum,tlocal_entry) = (r_reify "LocalDef", r_reify "LocalAssum", r_reify "local_entry")
-
-  let (cFinite,cCoFinite,cBiFinite) = (r_reify "Finite", r_reify "CoFinite", r_reify "BiFinite")
-  let tone_inductive_body = r_reify "one_inductive_body"
-  let tBuild_one_inductive_body = r_reify "Build_one_inductive_body"
-  let tBuild_mutual_inductive_body = r_reify "Build_mutual_inductive_body"
-  let tBuild_constant_body = r_reify "Build_constant_body"
-  let tglobal_decl = r_reify "global_decl"
-  let tConstantDecl = r_reify "ConstantDecl"
-  let tInductiveDecl = r_reify "InductiveDecl"
-  let tglobal_declarations = r_reify "global_declarations"
-
-  let tcontext_decl = r_reify "context_decl"
-  let tcontext = r_reify "context"
-
-  let tMutual_inductive_entry = r_reify "mutual_inductive_entry"
-  let tOne_inductive_entry = r_reify "one_inductive_entry"
-  let tBuild_mutual_inductive_entry = r_reify "Build_mutual_inductive_entry"
-  let tBuild_one_inductive_entry = r_reify "Build_one_inductive_entry"
-  let tConstant_entry = r_reify "constant_entry"
-  let cParameterEntry = r_reify "ParameterEntry"
-  let cDefinitionEntry = r_reify "DefinitionEntry"
-  let cParameter_entry = r_reify "Build_parameter_entry"
-  let cDefinition_entry = r_reify "Build_definition_entry"
-
-  let (tcbv, tcbn, thnf, tall, tlazy, tunfold) = (r_template_monad "cbv", r_template_monad "cbn", r_template_monad "hnf", r_template_monad "all", r_template_monad "lazy", r_template_monad "unfold")
-
-  let (tglobal_reference, tConstRef, tIndRef, tConstructRef) =
-    (r_base_reify "global_reference", r_base_reify "ConstRef", r_base_reify "IndRef", r_base_reify "ConstructRef")
-
-  (* let pkg_specif = ["Coq";"Init";"Specif"] *)
-  (* let texistT = resolve_symbol pkg_specif "existT" *)
-  (* let texistT_typed_term = r_template_monad "existT_typed_term" *)
-  let texistT_typed_term = r_template_monad_p "existT_typed_term"
+  include ConstrQuoted
 
   let to_coq_list typ =
     let the_nil = Constr.mkApp (c_nil, [| typ |]) in
diff --git a/template-coq/src/denote.ml b/template-coq/src/denote.ml
index 7bf8ca0e3..80abaa9e8 100644
--- a/template-coq/src/denote.ml
+++ b/template-coq/src/denote.ml
@@ -1,418 +1,109 @@
-open Univ
-open Names
+(* open Univ
+ * open Names *)
 open Pp (* this adds the ++ to the current scope *)
 
-open Tm_util
-open Quoter
-open Constr_quoter
-open TemplateCoqQuoter
+open Quoted
+open Denoter
 
 (* todo: the recursive call is uneeded provided we call it on well formed terms *)
 
-let print_term (u: t) : Pp.t = pr_constr u
+let print_term (u: Constr.t) : Pp.t = Printer.pr_constr u
 
-let unquote_pair trm =
-  let (h,args) = app_full trm [] in
-  if Constr.equal h c_pair then
-    match args with
-      _ :: _ :: x :: y :: [] -> (x, y)
-    | _ -> bad_term_verb trm "unquote_pair"
-  else
-    not_supported_verb trm "unquote_pair"
-
-let rec unquote_list trm =
-  let (h,args) = app_full trm [] in
-  if Constr.equal h c_nil then
-    []
-  else if Constr.equal h c_cons then
-    match args with
-      _ :: x :: xs :: [] -> x :: unquote_list xs
-    | _ -> bad_term_verb trm "unquote_list"
-  else
-    not_supported_verb trm "unquote_list"
-
-
-let inspect_term (t:Constr.t) :  (Constr.t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term =
-  let (h,args) = app_full t [] in
-  if Constr.equal h tRel then
-    match args with
-      x :: _ -> ACoq_tRel x
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tVar then
-    match args with
-      x :: _ -> ACoq_tVar x
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tSort then
-    match args with
-      x :: _ -> ACoq_tSort x
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tCast then
-    match args with
-      x :: y :: z :: _ -> ACoq_tCast (x, y, z)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tProd then
-    match args with
-      n :: t :: b :: _ -> ACoq_tProd (n,t,b)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tLambda then
-    match args with
-      n  :: t :: b :: _ -> ACoq_tLambda (n,t,b)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tLetIn then
-    match args with
-      n :: e :: t :: b :: _ -> ACoq_tLetIn (n,e,t,b)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tApp then
-    match args with
-      f::xs::_ -> ACoq_tApp (f, unquote_list xs)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tConst then
-    match args with
-      s::u::_ -> ACoq_tConst (s, u)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tInd then
-    match args with
-      i::u::_ -> ACoq_tInd (i,u)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tConstructor then
-    match args with
-      i::idx::u::_ -> ACoq_tConstruct (i,idx,u)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure: constructor case"))
-  else if Constr.equal h tCase then
-    match args with
-      info::ty::d::brs::_ -> ACoq_tCase (unquote_pair info, ty, d, List.map unquote_pair (unquote_list brs))
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tFix then
-    match args with
-      bds::i::_ ->
-      let unquoteFbd  b  =
-        let (_,args) = app_full b [] in
-        match args with
-        | _(*type*) :: na :: ty :: body :: rarg :: [] ->
-           { adtype = ty;
-             adname = na;
-             adbody = body;
-             rarg
-           }
-        |_ -> raise (Failure " (mkdef must take exactly 5 arguments)")
-      in
-      let lbd = List.map unquoteFbd (unquote_list bds) in
-      ACoq_tFix (lbd, i)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tCoFix then
-    match args with
-      bds::i::_ ->
-      let unquoteFbd  b  =
-        let (_,args) = app_full b [] in
-        match args with
-        | _(*type*) :: na :: ty :: body :: rarg :: [] ->
-           { adtype = ty;
-             adname = na;
-             adbody = body;
-             rarg
-           }
-        |_ -> raise (Failure " (mkdef must take exactly 5 arguments)")
-      in
-      let lbd = List.map unquoteFbd (unquote_list bds) in
-      ACoq_tCoFix (lbd, i)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-  else if Constr.equal h tProj then
-    match args with
-      proj::t::_ -> ACoq_tProj (proj, t)
-    | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
-
-  else
-    CErrors.user_err (str"inspect_term: cannot recognize " ++ print_term t ++ str" (maybe you forgot to reduce it?)")
-
-(* Unquote Coq nat to OCaml int *)
-let rec unquote_nat trm =
-  let (h,args) = app_full trm [] in
-  if Constr.equal h tO then
-    0
-  else if Constr.equal h tS then
-    match args with
-      n :: [] -> 1 + unquote_nat n
-    | _ -> bad_term_verb trm "unquote_nat"
-  else
-    not_supported_verb trm "unquote_nat"
-
-let unquote_bool trm =
-  if Constr.equal trm ttrue then
-    true
-  else if Constr.equal trm tfalse then
-    false
-  else not_supported_verb trm "from_bool"
-
-let unquote_char trm =
-  let (h,args) = app_full trm [] in
-  if Constr.equal h tAscii then
-    match args with
-      a :: b :: c :: d :: e :: f :: g :: h :: [] ->
-      let bits = List.rev [a;b;c;d;e;f;g;h] in
-      let v = List.fold_left (fun a n -> (a lsl 1) lor if unquote_bool n then 1 else 0) 0 bits in
-      char_of_int v
-    | _ -> bad_term_verb trm "unquote_char"
-  else
-    not_supported trm
-
-let unquote_string trm =
-  let rec go n trm =
-    let (h,args) = app_full trm [] in
-    if Constr.equal h tEmptyString then
-      Bytes.create n
-    else if Constr.equal h tString then
-      match args with
-        c :: s :: [] ->
-        let res = go (n + 1) s in
-        let _ = Bytes.set res n (unquote_char c) in
-        res
-      | _ -> bad_term_verb trm "unquote_string"
-    else
-      not_supported_verb trm "unquote_string"
-  in
-  Bytes.to_string (go 0 trm)
-
-let unquote_ident trm =
-  Id.of_string (unquote_string trm)
-
-let unquote_cast_kind trm =
-  if Constr.equal trm kVmCast then
-    Constr.VMcast
-  else if Constr.equal trm kCast then
-    Constr.DEFAULTcast
-  else if Constr.equal trm kRevertCast then
-    Constr.REVERTcast
-  else if Constr.equal trm kNative then
-    Constr.VMcast
-  else
-    not_supported_verb trm "unquote_cast_kind"
-
-
-let unquote_name trm =
-  let (h,args) = app_full trm [] in
-  if Constr.equal h nAnon then
-    Names.Anonymous
-  else if Constr.equal h nNamed then
-    match args with
-      n :: [] -> Names.Name (unquote_ident n)
-    | _ -> bad_term_verb trm "unquote_name"
-  else
-    not_supported_verb trm "unquote_name"
+let strict_unquote_universe_mode = ref true
 
 
-(* If strict unquote universe mode is on then fail when unquoting a non *)
-(* declared universe / an empty list of level expressions. *)
-(* Otherwise, add it / a fresh level the global environnment. *)
 
-let strict_unquote_universe_mode = ref true
 
-let _ =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "strict unquote universe mode";
-      optkey   = ["Strict"; "Unquote"; "Universe"; "Mode"];
-      optread  = (fun () -> !strict_unquote_universe_mode);
-      optwrite = (fun b -> strict_unquote_universe_mode := b) }
 
 let map_evm (f : 'a -> 'b -> 'a * 'c) (evm : 'a) (l : 'b list) : 'a * ('c list) =
   let evm, res = List.fold_left (fun (evm, l) b -> let evm, c = f evm b in evm, c :: l) (evm, []) l in
   evm, List.rev res
 
 
-
-let get_level evm s =
-  if CString.string_contains ~where:s ~what:"." then
-    match List.rev (CString.split '.' s) with
-    | [] -> CErrors.anomaly (str"Invalid universe name " ++ str s ++ str".")
-    | n :: dp ->
-       let num = int_of_string n in
-       let dp = DirPath.make (List.map Id.of_string dp) in
-       let l = Univ.Level.make dp num in
-       try
-         let evm = Evd.add_global_univ evm l in
-         if !strict_unquote_universe_mode then
-           CErrors.user_err ~hdr:"unquote_level" (str ("Level "^s^" is not a declared level and you are in Strict Unquote Universe Mode."))
-         else (Feedback.msg_info (str"Fresh universe " ++ Level.pr l ++ str" was added to the context.");
-               evm, l)
-       with
-       | UGraph.AlreadyDeclared -> evm, l
-  else
-    try
-      evm, Evd.universe_of_name evm (Id.of_string s)
-    with Not_found ->
-         try
-           let univ, k = Nametab.locate_universe (Libnames.qualid_of_string s) in
-           evm, Univ.Level.make univ k
-         with Not_found ->
-           CErrors.user_err ~hdr:"unquote_level" (str ("Level "^s^" is not a declared level."))
-
-
-
-
-
-let unquote_level evm trm (* of type level *) : Evd.evar_map * Univ.Level.t =
-  let (h,args) = app_full trm [] in
-  if Constr.equal h lProp then
-    match args with
-    | [] -> evm, Univ.Level.prop
-    | _ -> bad_term_verb trm "unquote_level"
-  else if Constr.equal h lSet then
-    match args with
-    | [] -> evm, Univ.Level.set
-    | _ -> bad_term_verb trm "unquote_level"
-  else if Constr.equal h tLevel then
-    match args with
-    | s :: [] -> debug (fun () -> str "Unquoting level " ++ pr_constr trm);
-                 get_level evm (unquote_string s)
-    | _ -> bad_term_verb trm "unquote_level"
-  else if Constr.equal h tLevelVar then
-    match args with
-    | l :: [] -> evm, Univ.Level.var (unquote_nat l)
-    | _ -> bad_term_verb trm "unquote_level"
-  else
-    not_supported_verb trm "unquote_level"
-
-let unquote_level_expr evm trm (* of type level *) b (* of type bool *) : Evd.evar_map * Univ.Universe.t =
-  let evm, l = unquote_level evm trm in
-  let u = Univ.Universe.make l in
-  evm, if unquote_bool b then Univ.Universe.super u else u
-
-
-let unquote_universe evm trm (* of type universe *) =
-  let levels = List.map unquote_pair (unquote_list trm) in
-  match levels with
-  | [] -> if !strict_unquote_universe_mode then
-            CErrors.user_err ~hdr:"unquote_universe" (str "It is not possible to unquote an empty universe in Strict Unquote Universe Mode.")
-          else
-            let evm, u = Evd.new_univ_variable (Evd.UnivFlexible false) evm in
-            Feedback.msg_info (str"Fresh universe " ++ Universe.pr u ++ str" was added to the context.");
-            evm, u
-  | (l,b)::q -> List.fold_left (fun (evm,u) (l,b) -> let evm, u' = unquote_level_expr evm l b
-                                                     in evm, Univ.Universe.sup u u')
-                               (unquote_level_expr evm l b) q
-
-let unquote_universe_instance evm trm (* of type universe_instance *) =
-  let l = unquote_list trm in
-  let evm, l = map_evm unquote_level evm l in
-  evm, Univ.Instance.of_array (Array.of_list l)
-
-
-
-let unquote_kn (k : quoted_kernel_name) : Libnames.qualid =
-  Libnames.qualid_of_string (clean_name (unquote_string k))
-
-let unquote_proj (qp : quoted_proj) : (quoted_inductive * quoted_int * quoted_int) =
-  let (h,args) = app_full qp [] in
-  match args with
-  | tyin::tynat::indpars::idx::[] ->
-     let (h',args') = app_full indpars [] in
-     (match args' with
-      | tyind :: tynat :: ind :: n :: [] -> (ind, n, idx)
-      | _ -> bad_term_verb qp "unquote_proj")
-  | _ -> bad_term_verb qp "unquote_proj"
-
-let unquote_inductive trm =
-  let (h,args) = app_full trm [] in
-  if Constr.equal h tmkInd then
-    match args with
-      nm :: num :: _ ->
-      let s = (unquote_string nm) in
-      let (dp, nm) = split_name s in
-      (try
-         match Nametab.locate (Libnames.make_qualid dp nm) with
-         | Globnames.ConstRef c ->  CErrors.user_err (str "this not an inductive constant. use tConst instead of tInd : " ++ str s)
-         | Globnames.IndRef i -> (fst i, unquote_nat  num)
-         | Globnames.VarRef _ -> CErrors.user_err (str "the constant is a variable. use tVar : " ++ str s)
-         | Globnames.ConstructRef _ -> CErrors.user_err (str "the constant is a consructor. use tConstructor : " ++ str s)
-       with
-         Not_found ->   CErrors.user_err (str "Constant not found : " ++ str s))
-    | _ -> assert false
-  else
-    bad_term_verb trm "non-constructor"
-
-
-
-(* TODO: replace app_full by this abstract version?*)
-let rec app_full_abs (trm: Constr.t) (acc: Constr.t list) =
-  match inspect_term trm with
-    ACoq_tApp (f, xs) -> app_full_abs f (xs @ acc)
-  | _ -> (trm, acc)
-
-
-let denote_term evm (trm: Constr.t) : Evd.evar_map * Constr.t =
-  let rec aux evm (trm: Constr.t) : _ * Constr.t =
-    debug (fun () -> Pp.(str "denote_term" ++ spc () ++ pr_constr trm)) ;
-    match inspect_term trm with
-    | ACoq_tRel x -> evm, Constr.mkRel (unquote_nat x + 1)
-    | ACoq_tVar x -> evm, Constr.mkVar (unquote_ident x)
-    | ACoq_tSort x -> let evm, u = unquote_universe evm x in evm, Constr.mkType u
-    | ACoq_tCast (t,c,ty) -> let evm, t = aux evm t in
-                             let evm, ty = aux evm ty in
-                             evm, Constr.mkCast (t, unquote_cast_kind c, ty)
-    | ACoq_tProd (n,t,b) -> let evm, t = aux evm t in
-                            let evm, b = aux evm b in
-                            evm, Constr.mkProd (unquote_name n, t, b)
-    | ACoq_tLambda (n,t,b) -> let evm, t = aux evm t in
-                              let evm, b = aux evm b in
-                              evm, Constr.mkLambda (unquote_name n, t, b)
-    | ACoq_tLetIn (n,e,t,b) -> let evm, e = aux evm e in
-                               let evm, t = aux evm t in
-                               let evm, b = aux evm b in
-                               evm, Constr.mkLetIn (unquote_name n, e, t, b)
-    | ACoq_tApp (f,xs) -> let evm, f = aux evm f in
-                          let evm, xs = map_evm aux evm xs in
-                          evm, Constr.mkApp (f, Array.of_list xs)
-    | ACoq_tConst (s,u) ->
-       let s = unquote_kn s in
-       let evm, u = unquote_universe_instance evm u in
-       (try
-          match Nametab.locate s with
-          | Globnames.ConstRef c -> evm, Constr.mkConstU (c, u)
-          | Globnames.IndRef _ -> CErrors.user_err (str"The constant " ++ Libnames.pr_qualid s ++ str" is an inductive, use tInd.")
-          | Globnames.VarRef _ -> CErrors.user_err (str"The constant " ++ Libnames.pr_qualid s ++ str" is a variable, use tVar.")
-          | Globnames.ConstructRef _ -> CErrors.user_err (str"The constant " ++ Libnames.pr_qualid s ++ str" is a constructor, use tConstructor.")
-        with
-          Not_found -> CErrors.user_err (str"Constant not found: " ++ Libnames.pr_qualid s))
-    | ACoq_tConstruct (i,idx,u) ->
-       let ind = unquote_inductive i in
-       let evm, u = unquote_universe_instance evm u in
-       evm, Constr.mkConstructU ((ind, unquote_nat idx + 1), u)
-    | ACoq_tInd (i, u) ->
-       let i = unquote_inductive i in
-       let evm, u = unquote_universe_instance evm u in
-       evm, Constr.mkIndU (i, u)
-    | ACoq_tCase ((i, _), ty, d, brs) ->
-       let ind = unquote_inductive i in
-       let evm, ty = aux evm ty in
-       let evm, d = aux evm d in
-       let evm, brs = map_evm aux evm (List.map snd brs) in
-       (* todo: reify better case_info *)
-       let ci = Inductiveops.make_case_info (Global.env ()) ind Constr.RegularStyle in
-       evm, Constr.mkCase (ci, ty, d, Array.of_list brs)
-    | ACoq_tFix (lbd, i) ->
-       let (names,types,bodies,rargs) = (List.map (fun p->p.adname) lbd,  List.map (fun p->p.adtype) lbd, List.map (fun p->p.adbody) lbd,
-                                         List.map (fun p->p.rarg) lbd) in
-       let evm, types = map_evm aux evm types in
-       let evm, bodies = map_evm aux evm bodies in
-       let (names,rargs) = (List.map unquote_name names, List.map unquote_nat rargs) in
-       let la = Array.of_list in
-       evm, Constr.mkFix ((la rargs,unquote_nat i), (la names, la types, la bodies))
-    | ACoq_tCoFix (lbd, i) ->
-       let (names,types,bodies,rargs) = (List.map (fun p->p.adname) lbd,  List.map (fun p->p.adtype) lbd, List.map (fun p->p.adbody) lbd,
-                                         List.map (fun p->p.rarg) lbd) in
-       let evm, types = map_evm aux evm types in
-       let evm, bodies = map_evm aux evm bodies in
-       let (names,rargs) = (List.map unquote_name names, List.map unquote_nat rargs) in
-       let la = Array.of_list in
-       evm, Constr.mkCoFix (unquote_nat i, (la names, la types, la bodies))
-    | ACoq_tProj (proj,t) ->
-       let (ind, _, narg) = unquote_proj proj in (* todo: is narg the correct projection? *)
-       let ind' = unquote_inductive ind in
-       let projs = Recordops.lookup_projections ind' in
-       let evm, t = aux evm t in
-       (match List.nth projs (unquote_nat narg) with
-        | Some p -> evm, Constr.mkProj (Names.Projection.make p false, t)
-        | None -> bad_term trm)
-    | _ ->  not_supported_verb trm "big_case"
-  in aux evm trm
+module Denote (D : Denoter) =
+struct
+
+  (* TODO: replace app_full by this abstract version?*)
+  let rec app_full_abs (trm: D.t) (acc: D.t list) =
+    match D.inspect_term trm with
+      ACoq_tApp (f, xs) -> app_full_abs f (xs @ acc)
+    | _ -> (trm, acc)
+
+  let denote_term (evm : Evd.evar_map) (trm: D.t) : Evd.evar_map * Constr.t =
+    let rec aux evm (trm: D.t) : _ * Constr.t =
+      (*    debug (fun () -> Pp.(str "denote_term" ++ spc () ++ pr_constr trm)) ; *)
+      match D.inspect_term trm with
+      | ACoq_tRel x -> evm, Constr.mkRel (D.unquote_int x + 1)
+      | ACoq_tVar x -> evm, Constr.mkVar (D.unquote_ident x)
+      | ACoq_tSort x -> let evm, u = D.unquote_universe evm x in evm, Constr.mkType u
+      | ACoq_tCast (t,c,ty) -> let evm, t = aux evm t in
+        let evm, ty = aux evm ty in
+        evm, Constr.mkCast (t, D.unquote_cast_kind c, ty)
+      | ACoq_tProd (n,t,b) -> let evm, t = aux evm t in
+        let evm, b = aux evm b in
+        evm, Constr.mkProd (D.unquote_name n, t, b)
+      | ACoq_tLambda (n,t,b) -> let evm, t = aux evm t in
+        let evm, b = aux evm b in
+        evm, Constr.mkLambda (D.unquote_name n, t, b)
+      | ACoq_tLetIn (n,e,t,b) -> let evm, e = aux evm e in
+        let evm, t = aux evm t in
+        let evm, b = aux evm b in
+        evm, Constr.mkLetIn (D.unquote_name n, e, t, b)
+      | ACoq_tApp (f,xs) -> let evm, f = aux evm f in
+        let evm, xs = map_evm aux evm xs in
+        evm, Constr.mkApp (f, Array.of_list xs)
+      | ACoq_tConst (s,u) ->
+        let s = D.unquote_kn s in
+        let evm, u = D.unquote_universe_instance evm u in
+        (try
+           match Nametab.locate s with
+           | Globnames.ConstRef c -> evm, Constr.mkConstU (c, u)
+           | Globnames.IndRef _ -> CErrors.user_err (str"The constant " ++ Libnames.pr_qualid s ++ str" is an inductive, use tInd.")
+           | Globnames.VarRef _ -> CErrors.user_err (str"The constant " ++ Libnames.pr_qualid s ++ str" is a variable, use tVar.")
+           | Globnames.ConstructRef _ -> CErrors.user_err (str"The constant " ++ Libnames.pr_qualid s ++ str" is a constructor, use tConstructor.")
+         with
+           Not_found -> CErrors.user_err (str"Constant not found: " ++ Libnames.pr_qualid s))
+      | ACoq_tConstruct (i,idx,u) ->
+        let ind = D.unquote_inductive i in
+        let evm, u = D.unquote_universe_instance evm u in
+        evm, Constr.mkConstructU ((ind, D.unquote_int idx + 1), u)
+      | ACoq_tInd (i, u) ->
+        let i = D.unquote_inductive i in
+        let evm, u = D.unquote_universe_instance evm u in
+        evm, Constr.mkIndU (i, u)
+      | ACoq_tCase ((i, _), ty, d, brs) ->
+        let ind = D.unquote_inductive i in
+        let evm, ty = aux evm ty in
+        let evm, d = aux evm d in
+        let evm, brs = map_evm aux evm (List.map snd brs) in
+        (* todo: reify better case_info *)
+        let ci = Inductiveops.make_case_info (Global.env ()) ind Constr.RegularStyle in
+        evm, Constr.mkCase (ci, ty, d, Array.of_list brs)
+      | ACoq_tFix (lbd, i) ->
+        let (names,types,bodies,rargs) = (List.map (fun p->p.adname) lbd,  List.map (fun p->p.adtype) lbd, List.map (fun p->p.adbody) lbd,
+                                          List.map (fun p->p.rarg) lbd) in
+        let evm, types = map_evm aux evm types in
+        let evm, bodies = map_evm aux evm bodies in
+        let (names,rargs) = (List.map D.unquote_name names, List.map D.unquote_int rargs) in
+        let la = Array.of_list in
+        evm, Constr.mkFix ((la rargs, D.unquote_int i), (la names, la types, la bodies))
+      | ACoq_tCoFix (lbd, i) ->
+        let (names,types,bodies,rargs) = (List.map (fun p->p.adname) lbd,  List.map (fun p->p.adtype) lbd, List.map (fun p->p.adbody) lbd,
+                                          List.map (fun p->p.rarg) lbd) in
+        let evm, types = map_evm aux evm types in
+        let evm, bodies = map_evm aux evm bodies in
+        let (names,rargs) = (List.map D.unquote_name names, List.map D.unquote_int rargs) in
+        let la = Array.of_list in
+        evm, Constr.mkCoFix (D.unquote_int i, (la names, la types, la bodies))
+      | ACoq_tProj (proj,t) ->
+        let (ind, _, narg) = D.unquote_proj proj in (* todo: is narg the correct projection? *)
+        let ind' = D.unquote_inductive ind in
+        let projs = Recordops.lookup_projections ind' in
+        let evm, t = aux evm t in
+        (match List.nth projs (D.unquote_int narg) with
+         | Some p -> evm, Constr.mkProj (Names.Projection.make p false, t)
+         | None -> (*bad_term trm *) failwith "tproj case of denote_term")
+      | _ -> failwith "big case of denote_term"
+    in aux evm trm
+
+end
diff --git a/template-coq/src/denote.mli b/template-coq/src/denote.mli
deleted file mode 100644
index 4aba23cf1..000000000
--- a/template-coq/src/denote.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-val unquote_pair : Constr.t -> Constr.t * Constr.t
-
-val unquote_list : Constr.t -> Constr.t list
-
-val unquote_bool : Constr.t -> bool
-
-val unquote_ident : Constr.t -> Names.Id.t
-
-val unquote_string : Constr.t -> string
-
-val unquote_kn : Constr.t -> Libnames.qualid
-
-(* ^^ above this is completely generic *)
-
-val unquote_level : Evd.evar_map -> Constr.constr -> Evd.evar_map * Univ.Level.t
-
-val unquote_universe_instance : Evd.evar_map -> Constr.constr -> Evd.evar_map * Univ.Instance.t
-
-val map_evm : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
-
-val denote_term : Evd.evar_map -> Constr.t -> Evd.evar_map * Constr.t
diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml
new file mode 100644
index 000000000..b68b86c41
--- /dev/null
+++ b/template-coq/src/denoter.ml
@@ -0,0 +1,25 @@
+open Names
+open Quoted
+
+module type Denoter =
+sig
+  include Quoted
+
+  val unquote_ident : quoted_ident -> Id.t
+  val unquote_name : quoted_name -> Name.t
+  val unquote_int :  quoted_int -> int
+  val unquote_bool : quoted_bool -> bool
+  (* val unquote_sort : quoted_sort -> Sorts.t *)
+  (* val unquote_sort_family : quoted_sort_family -> Sorts.family *)
+  val unquote_cast_kind : quoted_cast_kind -> Constr.cast_kind
+  val unquote_kn :  quoted_kernel_name -> Libnames.qualid
+  val unquote_inductive :  quoted_inductive -> Names.inductive
+  (*val unquote_univ_instance :  quoted_univ_instance -> Univ.Instance.t *)
+  val unquote_proj : quoted_proj -> (quoted_inductive * quoted_int * quoted_int)
+  val unquote_universe : Evd.evar_map -> quoted_sort -> Evd.evar_map * Univ.Universe.t
+  val print_term : t -> Pp.t
+  val unquote_universe_instance: Evd.evar_map -> quoted_univ_instance -> Evd.evar_map * Univ.Instance.t
+  (* val representsIndConstuctor : quoted_inductive -> Term.constr -> bool *)
+  val inspect_term : t -> (t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term
+
+end
diff --git a/template-coq/src/g_template_coq.ml4 b/template-coq/src/g_template_coq.ml4
index f35f23f93..4617b31ec 100644
--- a/template-coq/src/g_template_coq.ml4
+++ b/template-coq/src/g_template_coq.ml4
@@ -48,7 +48,6 @@ let to_ltac_val c = Tacinterp.Value.of_constr c
 let run_template_program env evm pgm =
   Run_template_monad.run_template_program_rec (fun _ -> ()) env (evm, pgm)
 
-
 (** ********* Commands ********* *)
 
 VERNAC COMMAND EXTEND Make_tests CLASSIFIED AS QUERY
@@ -134,7 +133,7 @@ TACTIC EXTEND denote_term
     | [ "denote_term" constr(c) tactic(tac) ] ->
       [ Proofview.Goal.enter (begin fun gl ->
          let evm = Proofview.Goal.sigma gl in
-         let evm, c = Denote.denote_term evm (EConstr.to_constr evm c) in
+         let evm, c = Constr_denoter.denote_term evm (EConstr.to_constr evm c) in
          Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm)
 	   (ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c]))
       end) ]
@@ -150,7 +149,7 @@ TACTIC EXTEND run_program
          match !ret with
            Some (env, evm, t) ->
             Proofview.tclTHEN
-              (Proofview.Unsafe.tclEVARS evm) 
+              (Proofview.Unsafe.tclEVARS evm)
               (ltac_apply tac (List.map to_ltac_val [EConstr.of_constr t]))
          | None -> Proofview.tclUNIT ()
        end) ]
diff --git a/template-coq/src/monad_extraction.mlpack b/template-coq/src/monad_extraction.mlpack
new file mode 100644
index 000000000..153ad83e5
--- /dev/null
+++ b/template-coq/src/monad_extraction.mlpack
@@ -0,0 +1,50 @@
+Utils
+Ascii
+Ast0
+Univ0
+AstUtils
+BasicAst
+Basics
+BinInt
+BinNat
+BinNums
+BinPosDef
+BinPos
+Bool
+Common
+Config0
+Datatypes
+DecidableType
+Decimal
+Equalities
+Extractable
+FMapWeakList
+List0
+Logic
+MSetWeakList
+Nat0
+OrderedType0
+Orders
+OrdersTac
+PeanoNat
+Specif
+String0
+UGraph0
+
+
+
+
+
+Tm_util
+Quoter
+Constr_quoter
+Template_monad
+Denote
+Denoter
+Plugin_core
+Ast_quoter
+Ast_denoter
+
+Extractable
+
+Run_extractable
\ No newline at end of file
diff --git a/template-coq/src/pluginCore.ml b/template-coq/src/plugin_core.ml
similarity index 81%
rename from template-coq/src/pluginCore.ml
rename to template-coq/src/plugin_core.ml
index 7885625e9..d5d88f2dc 100644
--- a/template-coq/src/pluginCore.ml
+++ b/template-coq/src/plugin_core.ml
@@ -28,16 +28,26 @@ let rs_unfold (env : Environ.env) (gr : global_reference) =
 type 'a tm =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> 'a -> unit) ->
-  (string -> unit) -> unit
+  (Pp.t -> unit) -> unit
 
 let run (c : 'a tm) env evm (k : Environ.env -> Evd.evar_map -> 'a -> unit) : unit =
-  c env evm k (fun x -> CErrors.user_err (Pp.str x))
+  c env evm k (fun x -> CErrors.user_err x)
+
+let run_vernac (c : 'a tm) : unit =
+  let (evm,env) = Pfedit.get_current_context () in
+  run c env evm (fun _ _ _ -> ())
+
+let with_env_evm (c : Environ.env -> Evd.evar_map -> 'a tm) : 'a tm =
+  fun env evm success fail -> c env evm env evm success fail
 
 let tmReturn (x : 'a) : 'a tm =
   fun env evd k _fail -> k env evd x
 let tmBind (x : 'a tm) (k : 'a -> 'b tm) : 'b tm =
   fun env evd success fail ->
         x env evd (fun env evd v -> k v env evd success fail) fail
+let tmMap (f : 'a -> 'b) (x : 'a tm) : 'b tm =
+  fun env evd success fail ->
+        x env evd (fun env evd v -> success env evd (f v)) fail
 
 let tmPrint (t : term) : unit tm =
   fun env evd success _fail ->
@@ -48,8 +58,10 @@ let tmMsg  (s : string) : unit tm =
     let _ = Feedback.msg_info (Pp.str s) in
     success env evd ()
 
-let tmFail (s : string) : 'a tm =
+let tmFail (s : Pp.t) : 'a tm =
   fun _ _ _ fail -> fail s
+let tmFailString (s : string) : 'a tm =
+  tmFail Pp.(str s)
 
 let tmEval (rd : reduction_strategy) (t : term) : term tm =
   fun env evd k _fail ->
@@ -114,19 +126,26 @@ let tmAbout (qualid : qualid) : global_reference option tm =
       let gr = Smartlocate.locate_global_with_alias (CAst.make qualid) in
       success env evd (Some gr)
     with
-    | Not_found -> success env evd None
+      Not_found -> success env evd None
+
+let tmAboutString (s : string) : global_reference option tm =
+  fun env evd success fail ->
+    let (dp, nm) = Quoted.split_name s in
+    let q = Libnames.make_qualid dp nm in
+    tmAbout q env evd success fail
 
 let tmCurrentModPath : Names.ModPath.t tm =
   fun env evd success _fail ->
     let mp = Lib.current_mp () in success env evd mp
 
-let tmQuoteInductive (kn : kername) : mutual_inductive_body option tm =
+let tmQuoteInductive (kn : kername) : (Names.MutInd.t * mutual_inductive_body) option tm =
   fun env evm success _fail ->
     try
-      let mind = Environ.lookup_mind (Names.MutInd.make1 kn) env in
-      success env evm (Some mind)
+      let mi = Names.MutInd.make1 kn in
+      let mind = Environ.lookup_mind mi env in
+      success env evm (Some (mi, mind))
     with
-      _ -> success env evm None
+      Not_found -> success env evm None
 
 let tmQuoteUniverses : UGraph.t tm =
   fun env evm success _fail ->
@@ -134,9 +153,13 @@ let tmQuoteUniverses : UGraph.t tm =
 
 (* get the definition associated to a kername *)
 let tmQuoteConstant (kn : kername) (bypass : bool) : constant_entry tm =
-  fun env evd success _fail ->
-    let cnst = Environ.lookup_constant (Names.Constant.make1 kn) env in
-    success env evd cnst
+  fun env evd success fail ->
+    (* todo(gmm): there is a bug here *)
+    try
+      let cnst = Environ.lookup_constant (Names.Constant.make1 kn) env in
+      success env evd cnst
+    with
+      Not_found -> fail Pp.(str "constant not found " ++ Names.KerName.print kn)
 
 let tmInductive (mi : mutual_inductive_entry) : unit tm =
   fun env evd success _fail ->
diff --git a/template-coq/src/pluginCore.mli b/template-coq/src/plugin_core.mli
similarity index 84%
rename from template-coq/src/pluginCore.mli
rename to template-coq/src/plugin_core.mli
index c56584c70..3b8a1bfb5 100644
--- a/template-coq/src/pluginCore.mli
+++ b/template-coq/src/plugin_core.mli
@@ -22,13 +22,19 @@ type 'a tm
 
 val run : 'a tm -> Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> 'a -> unit) -> unit
 
+val with_env_evm : (Environ.env -> Evd.evar_map -> 'a tm) -> 'a tm
+
+val run_vernac : 'a tm -> unit
+
 val tmReturn : 'a -> 'a tm
 val tmBind : 'a tm -> ('a -> 'b tm) -> 'b tm
+val tmMap  : ('a -> 'b) -> 'a tm -> 'b tm
 
 val tmPrint : term -> unit tm
 val tmMsg  : string -> unit tm
 
-val tmFail : string -> 'a tm
+val tmFail : Pp.t -> 'a tm
+val tmFailString : string -> 'a tm
 val tmEval : reduction_strategy -> term -> term tm
 
 val tmDefinition : ident -> ?poly:bool -> term option -> term -> kername tm
@@ -38,9 +44,10 @@ val tmLemma : ident -> ?poly:bool -> term -> kername tm
 val tmFreshName : ident -> ident tm
 
 val tmAbout : qualid -> global_reference option tm
+val tmAboutString : string -> global_reference option tm
 val tmCurrentModPath : Names.ModPath.t tm
 
-val tmQuoteInductive : kername -> mutual_inductive_body option tm
+val tmQuoteInductive : kername -> (Names.MutInd.t * mutual_inductive_body) option tm
 val tmQuoteUniverses : UGraph.t tm
 val tmQuoteConstant : kername -> bool -> constant_entry tm
 
diff --git a/template-coq/src/quoted.ml b/template-coq/src/quoted.ml
new file mode 100644
index 000000000..3ab3a18eb
--- /dev/null
+++ b/template-coq/src/quoted.ml
@@ -0,0 +1,122 @@
+type ('a,'b) sum =
+  Left of 'a | Right of 'b
+
+type ('term, 'name, 'nat) adef = { adname : 'name; adtype : 'term; adbody : 'term; rarg : 'nat }
+
+type ('term, 'name, 'nat) amfixpoint = ('term, 'name, 'nat) adef list
+
+type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'universe_instance, 'projection) structure_of_term =
+  | ACoq_tRel of 'nat
+  | ACoq_tVar of 'ident
+  | ACoq_tEvar of 'nat * 'term list
+  | ACoq_tSort of 'quoted_sort
+  | ACoq_tCast of 'term * 'cast_kind * 'term
+  | ACoq_tProd of 'name * 'term * 'term
+  | ACoq_tLambda of 'name * 'term * 'term
+  | ACoq_tLetIn of 'name * 'term * 'term * 'term
+  | ACoq_tApp of 'term * 'term list
+  | ACoq_tConst of 'kername * 'universe_instance
+  | ACoq_tInd of 'inductive * 'universe_instance
+  | ACoq_tConstruct of 'inductive * 'nat * 'universe_instance
+  | ACoq_tCase of ('inductive * 'nat) * 'term * 'term * ('nat * 'term) list
+  | ACoq_tProj of 'projection * 'term
+  | ACoq_tFix of ('term, 'name, 'nat) amfixpoint * 'nat
+  | ACoq_tCoFix of ('term, 'name, 'nat) amfixpoint * 'nat
+
+(* todo(gmm): these are helper functions *)
+let string_to_list s =
+  let rec aux acc i =
+    if i < 0 then acc
+    else aux (s.[i] :: acc) (i - 1)
+  in aux [] (String.length s - 1)
+
+let list_to_string l =
+  let buf = Bytes.create (List.length l) in
+  let rec aux i = function
+    | [] -> ()
+    | c :: cs ->
+      Bytes.set buf i c; aux (succ i) cs
+  in
+  aux 0 l;
+  Bytes.to_string buf
+
+(* Remove '#' from names *)
+let clean_name s =
+  let l = List.rev (CString.split '#' s) in
+  match l with
+    s :: rst -> s
+  | [] -> raise (Failure "Empty name cannot be quoted")
+
+let split_name s : (Names.DirPath.t * Names.Id.t) =
+  let ss = List.rev (CString.split '.' s) in
+  match ss with
+    nm :: rst ->
+     let nm = clean_name nm in
+     let dp = (Names.DirPath.make (List.map Names.Id.of_string rst)) in (dp, Names.Id.of_string nm)
+  | [] -> raise (Failure "Empty name cannot be quoted")
+
+
+
+module type Quoted =
+sig
+  type t (* this represented quoted Gallina terms *)
+
+  type quoted_ident
+  type quoted_int
+  type quoted_bool
+  type quoted_name
+  type quoted_sort
+  type quoted_cast_kind
+  type quoted_kernel_name
+  type quoted_inductive
+  type quoted_proj
+  type quoted_global_reference
+
+  type quoted_sort_family
+  type quoted_constraint_type
+  type quoted_univ_constraint
+  type quoted_univ_instance
+  type quoted_univ_constraints
+  type quoted_univ_context
+  type quoted_inductive_universes
+
+  type quoted_mind_params
+  type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list
+  type quoted_definition_entry = t * t option * quoted_univ_context
+  type quoted_mind_entry
+  type quoted_mind_finiteness
+  type quoted_entry
+
+  (* Local contexts *)
+  type quoted_context_decl
+  type quoted_context
+
+  type quoted_one_inductive_body
+  type quoted_mutual_inductive_body
+  type quoted_constant_body
+  type quoted_global_decl
+  type quoted_global_declarations
+  type quoted_program  (* the return type of quote_recursively *)
+
+  val mkRel : quoted_int -> t
+  val mkVar : quoted_ident -> t
+  val mkEvar : quoted_int -> t array -> t
+  val mkSort : quoted_sort -> t
+  val mkCast : t -> quoted_cast_kind -> t -> t
+  val mkProd : quoted_name -> t -> t -> t
+  val mkLambda : quoted_name -> t -> t -> t
+  val mkLetIn : quoted_name -> t -> t -> t -> t
+  val mkApp : t -> t array -> t
+  val mkConst : quoted_kernel_name -> quoted_univ_instance -> t
+  val mkInd : quoted_inductive -> quoted_univ_instance -> t
+  val mkConstruct : quoted_inductive * quoted_int -> quoted_univ_instance -> t
+  val mkCase : (quoted_inductive * quoted_int) -> quoted_int list -> t -> t ->
+               t list -> t
+  val mkProj : quoted_proj -> t -> t
+  val mkFix : (quoted_int array * quoted_int) * (quoted_name array * t array * t array) -> t
+  val mkCoFix : quoted_int * (quoted_name array * t array * t array) -> t
+
+  val mkName : quoted_ident -> quoted_name
+  val mkAnon : quoted_name
+
+end
diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
index 3f7ee2133..46d7f8312 100644
--- a/template-coq/src/quoter.ml
+++ b/template-coq/src/quoter.ml
@@ -3,18 +3,14 @@ open Entries
 open Declarations
 open Pp
 
+open Tm_util
+open Quoted
+
 let cast_prop = ref (false)
 
 (* whether Set Template Cast Propositions is on, as needed for erasure in Certicoq *)
 let is_cast_prop () = !cast_prop
 
-let opt_debug = ref false
-
-let debug (m : unit ->Pp.t) =
-  if !opt_debug then
-    Feedback.(msg_debug (m ()))
-  else
-    ()
 
 let toDecl (old: Name.t * ((Constr.constr) option) * Constr.constr) : Context.Rel.Declaration.t =
   let (name,value,typ) = old in
@@ -25,23 +21,6 @@ let toDecl (old: Name.t * ((Constr.constr) option) * Constr.constr) : Context.Re
 let getType env (t:Constr.t) : Constr.t =
     EConstr.to_constr Evd.empty (Retyping.get_type_of env Evd.empty (EConstr.of_constr t))
 
-let pr_constr trm =
-  let (evm, env) = Pfedit.get_current_context () in
-  Printer.pr_constr_env env evm trm
-
-let not_supported trm =
-  CErrors.user_err (str "Not Supported:" ++ spc () ++ pr_constr trm)
-
-let not_supported_verb trm rs =
-  CErrors.user_err (str "Not Supported raised at " ++ str rs ++ str ":" ++ spc () ++ pr_constr trm)
-
-let bad_term trm =
-  CErrors.user_err (str "Bad term:" ++ spc () ++ pr_constr trm)
-
-let bad_term_verb trm rs =
-  CErrors.user_err (str "Bad term:" ++ spc () ++ pr_constr trm
-                    ++ spc () ++ str " Error: " ++ str rs)
-
 (* TODO: remove? *)
 let opt_hnf_ctor_types = ref false
 
@@ -57,86 +36,9 @@ let hnf_type env ty =
   in
   hnf_type true ty
 
-(* Remove '#' from names *)
-let clean_name s =
-  let l = List.rev (CString.split '#' s) in
-  match l with
-    s :: rst -> s
-  | [] -> raise (Failure "Empty name cannot be quoted")
-
-let split_name s : (Names.DirPath.t * Names.Id.t) =
-  let ss = List.rev (CString.split '.' s) in
-  match ss with
-    nm :: rst ->
-     let nm = clean_name nm in
-     let dp = (DirPath.make (List.map Id.of_string rst)) in (dp, Names.Id.of_string nm)
-  | [] -> raise (Failure "Empty name cannot be quoted")
-
-
-type ('a,'b) sum =
-  Left of 'a | Right of 'b
-
-type ('term, 'name, 'nat) adef = { adname : 'name; adtype : 'term; adbody : 'term; rarg : 'nat }
-
-type ('term, 'name, 'nat) amfixpoint = ('term, 'name, 'nat) adef list
-
-type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'universe_instance, 'projection) structure_of_term =
-  | ACoq_tRel of 'nat
-  | ACoq_tVar of 'ident
-  | ACoq_tEvar of 'nat * 'term list
-  | ACoq_tSort of 'quoted_sort
-  | ACoq_tCast of 'term * 'cast_kind * 'term
-  | ACoq_tProd of 'name * 'term * 'term
-  | ACoq_tLambda of 'name * 'term * 'term
-  | ACoq_tLetIn of 'name * 'term * 'term * 'term
-  | ACoq_tApp of 'term * 'term list
-  | ACoq_tConst of 'kername * 'universe_instance
-  | ACoq_tInd of 'inductive * 'universe_instance
-  | ACoq_tConstruct of 'inductive * 'nat * 'universe_instance
-  | ACoq_tCase of ('inductive * 'nat) * 'term * 'term * ('nat * 'term) list
-  | ACoq_tProj of 'projection * 'term
-  | ACoq_tFix of ('term, 'name, 'nat) amfixpoint * 'nat
-  | ACoq_tCoFix of ('term, 'name, 'nat) amfixpoint * 'nat
-
-module type Quoter = sig
-  type t
-
-  type quoted_ident
-  type quoted_int
-  type quoted_bool
-  type quoted_name
-  type quoted_sort
-  type quoted_cast_kind
-  type quoted_kernel_name
-  type quoted_inductive
-  type quoted_proj
-  type quoted_global_reference
-
-  type quoted_sort_family
-  type quoted_constraint_type
-  type quoted_univ_constraint
-  type quoted_univ_instance
-  type quoted_univ_constraints
-  type quoted_univ_context
-  type quoted_inductive_universes
-
-  type quoted_mind_params
-  type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list
-  type quoted_definition_entry = t * t option * quoted_univ_context
-  type quoted_mind_entry
-  type quoted_mind_finiteness
-  type quoted_entry
-
-  (* Local contexts *)
-  type quoted_context_decl
-  type quoted_context
-
-  type quoted_one_inductive_body
-  type quoted_mutual_inductive_body
-  type quoted_constant_body
-  type quoted_global_decl
-  type quoted_global_declarations
-  type quoted_program  (* the return type of quote_recursively *)
+module type Quoter =
+sig
+  include Quoted
 
   val quote_ident : Id.t -> quoted_ident
   val quote_name : Name.t -> quoted_name
@@ -167,27 +69,6 @@ module type Quoter = sig
 
   val quote_entry : (quoted_definition_entry, quoted_mind_entry) sum option -> quoted_entry
 
-  val mkName : quoted_ident -> quoted_name
-  val mkAnon : quoted_name
-
-  val mkRel : quoted_int -> t
-  val mkVar : quoted_ident -> t
-  val mkEvar : quoted_int -> t array -> t
-  val mkSort : quoted_sort -> t
-  val mkCast : t -> quoted_cast_kind -> t -> t
-  val mkProd : quoted_name -> t -> t -> t
-  val mkLambda : quoted_name -> t -> t -> t
-  val mkLetIn : quoted_name -> t -> t -> t -> t
-  val mkApp : t -> t array -> t
-  val mkConst : quoted_kernel_name -> quoted_univ_instance -> t
-  val mkInd : quoted_inductive -> quoted_univ_instance -> t
-  val mkConstruct : quoted_inductive * quoted_int -> quoted_univ_instance -> t
-  val mkCase : (quoted_inductive * quoted_int) -> quoted_int list -> t -> t ->
-               t list -> t
-  val mkProj : quoted_proj -> t -> t
-  val mkFix : (quoted_int array * quoted_int) * (quoted_name array * t array * t array) -> t
-  val mkCoFix : quoted_int * (quoted_name array * t array * t array) -> t
-
   val quote_context_decl : quoted_name -> t option -> t -> quoted_context_decl
   val quote_context : quoted_context_decl list -> quoted_context
 
@@ -348,6 +229,7 @@ struct
          let kn = Names.Constant.canonical (Names.Projection.constant p) in
          let t', acc = quote_term acc env c in
          (Q.mkProj p' t', add_constant kn acc)
+      | Constr.Meta _ -> failwith "found a Meta!"
       in
       let in_prop, env' = env in
       if is_cast_prop () && not in_prop then
@@ -612,30 +494,33 @@ since  [absrt_info] is a private type *)
    let uctx = Q.quote_inductive_universes t.mind_entry_universes in
     Q.quote_mutual_inductive_entry (mf, mp, is, uctx)
 
+  let quote_constant_body bypass env evm (cd : constant_body) =
+    let ty = quote_term env cd.const_type in
+    let body =
+      match cd.const_body with
+      | Undef _ -> None
+      | Def cs -> Some (quote_term env (Mod_subst.force_constr cs))
+      | OpaqueDef cs ->
+        if bypass
+        then Some (quote_term env (Opaqueproof.force_proof (Global.opaque_tables ()) cs))
+        else None
+    in
+    let uctx = quote_constant_uctx cd.const_universes in
+    (ty, body, uctx)
+
   let quote_entry_aux bypass env evm (name:string) =
     let (dp, nm) = split_name name in
     let entry =
       match Nametab.locate (Libnames.make_qualid dp nm) with
       | Globnames.ConstRef c ->
-         let cd = Environ.lookup_constant c env in
-         (*CHANGE :  template polymorphism for definitions was removed.
-                     See: https://github.com/coq/coq/commit/d9530632321c0b470ece6337cda2cf54d02d61eb *)
-         let ty = quote_term env cd.const_type in
-         let body = match cd.const_body with
-           | Undef _ -> None
-           | Def cs -> Some (quote_term env (Mod_subst.force_constr cs))
-           | OpaqueDef cs ->
-              if bypass
-              then Some (quote_term env (Opaqueproof.force_proof (Global.opaque_tables ()) cs))
-              else None
-         in
-         let uctx = quote_constant_uctx cd.const_universes in
-         Some (Left (ty, body, uctx))
-
+        let cd = Environ.lookup_constant c env in
+        (*CHANGE :  template polymorphism for definitions was removed.
+                    See: https://github.com/coq/coq/commit/d9530632321c0b470ece6337cda2cf54d02d61eb *)
+        Some (Left (quote_constant_body bypass env evm cd))
       | Globnames.IndRef ni ->
-         let c = Environ.lookup_mind (fst ni) env in (* FIX: For efficienctly, we should also export (snd ni)*)
-         let miq = quote_mut_ind env c in
-         Some (Right miq)
+        let c = Environ.lookup_mind (fst ni) env in (* FIX: For efficienctly, we should also export (snd ni)*)
+        let miq = quote_mut_ind env c in
+        Some (Right miq)
       | Globnames.ConstructRef _ -> None (* FIX?: return the enclusing mutual inductive *)
       | Globnames.VarRef _ -> None
     in entry
diff --git a/template-coq/src/run_extractable.ml b/template-coq/src/run_extractable.ml
new file mode 100644
index 000000000..1a389e65c
--- /dev/null
+++ b/template-coq/src/run_extractable.ml
@@ -0,0 +1,254 @@
+open Extractable
+open Plugin_core
+open BasicAst
+
+open Quoter
+open Ast_quoter
+
+
+let of_constr (env : Environ.env) (t : Constr.t) : Ast0.term =
+  Ast_quoter.quote_term env t
+
+let to_string : char list -> string =
+  Quoted.list_to_string
+
+let of_string : string -> char list =
+  Quoted.string_to_list
+
+let to_reduction_strategy (s : Common0.reductionStrategy) : Plugin_core.reduction_strategy =
+  match s with
+   | Common0.Coq_cbv -> Plugin_core.rs_cbv
+   | Common0.Coq_cbn -> Plugin_core.rs_cbn
+   | Common0.Coq_hnf -> Plugin_core.rs_hnf
+   | Common0.Coq_all -> Plugin_core.rs_all
+   | Common0.Coq_lazy -> Plugin_core.rs_lazy
+   | Common0.Coq_unfold x -> failwith "not yet implemented: to_reduction_strategy"
+
+let to_ident : char list ->  Names.Id.t =
+  Ast_quoter.unquote_ident
+
+let of_ident (id : Names.Id.t) : char list =
+  of_string (Names.Id.to_string id)
+
+let of_global_reference : Plugin_core.global_reference -> BasicAst.global_reference =
+  Ast_quoter.quote_global_reference
+
+let to_qualid (c : char list) : Libnames.qualid =
+  Libnames.qualid_of_string (to_string c)
+
+let of_qualid (q : Libnames.qualid) : char list =
+  of_string (Libnames.string_of_qualid q)
+
+let of_kername : Names.KerName.t -> char list =
+  Ast_quoter.quote_kn
+
+(* TODO: check that [s] was fully qualified *)
+let to_kername (s : char list) : Names.KerName.t =
+  match Nametab.locate (Ast_quoter.unquote_kn s) with
+   | Globnames.VarRef vr -> failwith "not yet implemented"
+   | Globnames.ConstRef c -> Names.Constant.canonical c
+   | Globnames.IndRef i -> Names.MutInd.canonical (fst i)
+   | Globnames.ConstructRef c -> failwith "not yet implemented"
+
+(* todo(gmm): this definition adapted from quoter.ml *)
+let quote_rel_decl env = function
+  | Context.Rel.Declaration.LocalAssum (na, t) ->
+    let t' = Ast_quoter.quote_term env t in
+    Ast_quoter.quote_context_decl (Ast_quoter.quote_name na) None t'
+  | Context.Rel.Declaration.LocalDef (na, b, t) ->
+    let b' = Ast_quoter.quote_term env b in
+    let t' = Ast_quoter.quote_term env t in
+    Ast_quoter.quote_context_decl (Ast_quoter.quote_name na) (Some b') t'
+
+(* todo(gmm): this definition adapted from quoter.ml *)
+let quote_rel_context env ctx =
+  let decls, env =
+    List.fold_right (fun decl (ds, env) ->
+        let x = quote_rel_decl env decl in
+        (x :: ds, Environ.push_rel decl env))
+      ctx ([],env) in
+  Ast_quoter.quote_context decls
+
+(* todo(gmm): this definition adapted from quoter.ml (the body of quote_minductive_type) *)
+let of_mib (env : Environ.env) (t : Names.MutInd.t) (mib : Plugin_core.mutual_inductive_body) : Ast0.mutual_inductive_body =
+  let open Declarations in
+  let uctx = get_abstract_inductive_universes mib.mind_universes in
+  let inst = Univ.UContext.instance uctx in
+  let indtys =
+    (CArray.map_to_list (fun oib ->
+         let ty = Inductive.type_of_inductive env ((mib,oib),inst) in
+         (Context.Rel.Declaration.LocalAssum (Names.Name oib.mind_typename, ty))) mib.mind_packets)
+  in
+  let envind = Environ.push_rel_context (List.rev indtys) env in
+  let (ls,acc) =
+    List.fold_left (fun (ls,acc) oib ->
+	let named_ctors =
+	  CList.combine3
+	    (Array.to_list oib.mind_consnames)
+	    (Array.to_list oib.mind_user_lc)
+	    (Array.to_list oib.mind_consnrealargs)
+	in
+        let indty = Inductive.type_of_inductive env ((mib,oib),inst) in
+        let indty = Ast_quoter.quote_term env indty in
+	let (reified_ctors,acc) =
+	  List.fold_left (fun (ls,acc) (nm,ty,ar) ->
+	      Tm_util.debug (fun () -> Pp.(str "opt_hnf_ctor_types:" ++ spc () ++
+                                   bool !opt_hnf_ctor_types)) ;
+	      let ty = if !opt_hnf_ctor_types then hnf_type envind ty else ty in
+	      let ty = quote_term acc ty in
+	      ((Ast_quoter.quote_ident nm, ty, Ast_quoter.quote_int ar) :: ls, acc))
+	    ([],acc) named_ctors
+	in
+        let projs, acc =
+          match mib.mind_record with
+          | Some (Some (id, csts, ps)) ->
+            let ctxwolet = Termops.smash_rel_context mib.mind_params_ctxt in
+            let indty = Constr.mkApp (Constr.mkIndU ((t,0),inst),
+                                      Context.Rel.to_extended_vect Constr.mkRel 0 ctxwolet) in
+            let indbinder = Context.Rel.Declaration.LocalAssum (Names.Name id,indty) in
+            let envpars = Environ.push_rel_context (indbinder :: ctxwolet) env in
+            let ps, acc = CArray.fold_right2 (fun cst pb (ls,acc) ->
+                let ty = quote_term envpars pb.proj_type in
+                let kn = Names.KerName.label (Names.Constant.canonical cst) in
+                let na = Ast_quoter.quote_ident (Names.Label.to_id kn) in
+                ((na, ty) :: ls, acc)) csts ps ([],acc)
+            in ps, acc
+          | _ -> [], acc
+        in
+        let sf = List.map Ast_quoter.quote_sort_family oib.mind_kelim in
+	(Ast_quoter.quote_ident oib.mind_typename, indty, sf, (List.rev reified_ctors), projs) :: ls, acc)
+      ([],env) (Array.to_list mib.mind_packets)
+  in
+  let nparams = Ast_quoter.quote_int mib.mind_nparams in
+  let paramsctx = quote_rel_context env mib.mind_params_ctxt in
+  let uctx = quote_abstract_inductive_universes mib.mind_universes in
+  let bodies = List.map Ast_quoter.mk_one_inductive_body (List.rev ls) in
+  Ast_quoter.mk_mutual_inductive_body nparams paramsctx bodies uctx
+
+let to_mie (x : Ast0.mutual_inductive_entry) : Plugin_core.mutual_inductive_entry =
+  failwith "to_mie"
+
+(* note(gmm): code taken from quoter.ml (quote_entry_aux) *)
+let of_constant_entry (env : Environ.env) (cd : Plugin_core.constant_entry) : Ast0.constant_entry =
+  let open Declarations in
+  let ty = quote_term env cd.const_type in
+  let body = match cd.const_body with
+    | Undef _ -> None
+    | Def cs -> Some (Ast_quoter.quote_term env (Mod_subst.force_constr cs))
+    | OpaqueDef cs ->
+      if true
+      then Some (Ast_quoter.quote_term env (Opaqueproof.force_proof (Global.opaque_tables ()) cs))
+      else None
+  in
+  let uctx = quote_constant_uctx cd.const_universes in
+  Ast_quoter.quote_constant_entry (ty, body, uctx)
+
+(* what about the overflow?
+  efficiency? extract to bigint using Coq directives and convert to int here? *)
+let of_nat (t : Datatypes.nat) : int =
+  failwith "of_constr"
+
+let of_cast_kind (ck: BasicAst.cast_kind) : Constr.cast_kind =
+  match ck with
+  | VmCast -> Constr.VMcast
+  | NativeCast -> Constr.VMcast
+  | Cast -> Constr.DEFAULTcast
+  | RevertCast -> Constr.REVERTcast
+
+open Ast_denoter
+  (* todo(gmm): determine what of these already exist. *)
+let rec to_constr_ev (evm : Evd.evar_map) (t : Ast0.term) : Evd.evar_map * Constr.t =
+  ExtractionDenote.denote_term evm t
+
+let to_constr (t : Ast0.term) : Constr.t =
+  snd (to_constr_ev Evd.empty t)
+
+let tmOfConstr (t : Constr.t) : Ast0.term tm =
+  Plugin_core.with_env_evm (fun env _ -> tmReturn (of_constr env t))
+
+let tmOfMib (ti : Names.MutInd.t) (t : Plugin_core.mutual_inductive_body) : Ast0.mutual_inductive_body tm =
+  Plugin_core.with_env_evm (fun env _ -> tmReturn (of_mib env ti t))
+
+let tmOfConstantEntry (t : Plugin_core.constant_entry) : Ast0.constant_entry tm =
+  Plugin_core.with_env_evm (fun env _ -> tmReturn (of_constant_entry env t))
+
+(*
+let dbg = function
+    Coq_tmReturn _ -> "tmReturn"
+  | Coq_tmBind _ -> "tmBind"
+  | Coq_tmPrint _ -> "tmPrint"
+  | Coq_tmMsg msg -> "tmMsg"
+  | Coq_tmFail err -> "tmFail"
+  | Coq_tmEval (r,t) -> "tmEval"
+  | Coq_tmDefinition (nm, typ, trm) -> "tmDefinition"
+  | Coq_tmAxiom (nm, typ) -> "tmAxiom"
+  | Coq_tmLemma (nm, typ) -> "tmLemma"
+  | Coq_tmFreshName nm -> "tmFreshName"
+  | Coq_tmAbout id -> "tmAbout"
+  | Coq_tmCurrentModPath -> "tmCurrentModPath"
+  | Coq_tmQuoteInductive kn -> "tmQuoteInductive"
+  | Coq_tmQuoteUniverses -> "tmQuoteUniverses"
+  | Coq_tmQuoteConstant (kn, b) -> "tmQuoteConstant"
+  | Coq_tmInductive i -> "tmInductive"
+  | Coq_tmExistingInstance k -> "tmExistingInstance"
+  | Coq_tmInferInstance t -> "tmInferInstance"
+*)
+
+let rec interp_tm (t : 'a coq_TM) : 'a tm =
+(*  Feedback.msg_debug Pp.(str (dbg t)) ; *)
+  match t with
+  | Coq_tmReturn x -> tmReturn x
+  | Coq_tmBind (c, k) -> tmBind (interp_tm c) (fun x -> interp_tm (k x))
+  | Coq_tmPrint t -> Obj.magic (tmPrint (to_constr t))
+  | Coq_tmMsg msg -> Obj.magic (tmMsg (to_string msg))
+  | Coq_tmFail err -> tmFailString (to_string err)
+  | Coq_tmEval (r,t) ->
+    tmBind (tmEval (to_reduction_strategy r) (to_constr t))
+           (fun x -> Obj.magic (tmOfConstr x))
+  | Coq_tmDefinition (nm, typ, trm) ->
+    let typ =
+      match typ with
+        None -> None
+      | Some typ -> Some (to_constr typ)
+    in
+    tmMap (fun x -> Obj.magic (of_kername x))
+          (tmDefinition (to_ident nm) typ (to_constr trm))
+  | Coq_tmAxiom (nm, typ) ->
+    tmMap (fun x -> Obj.magic (of_kername x))
+          (tmAxiom (to_ident nm) (to_constr typ))
+  | Coq_tmLemma (nm, typ) ->
+    tmMap (fun x -> Obj.magic (of_kername x))
+          (tmLemma (to_ident nm) (to_constr typ))
+  | Coq_tmFreshName nm ->
+    tmMap (fun x -> Obj.magic (of_ident x))
+          (tmFreshName (to_ident nm))
+  | Coq_tmAbout id ->
+    tmMap (function
+             None -> Obj.magic None
+           | Some gr -> Obj.magic (Some (of_global_reference gr)))
+          (tmAbout (to_qualid id))
+  | Coq_tmCurrentModPath ->
+    tmMap (fun mp -> Obj.magic (of_string (Names.ModPath.to_string mp)))
+          tmCurrentModPath
+  | Coq_tmQuoteInductive kn ->
+    tmBind (tmQuoteInductive (to_kername kn))
+           (function
+             None -> Obj.magic (tmFail Pp.(str "inductive does not exist"))
+           | Some (mi, mib) -> Obj.magic (tmOfMib mi mib))
+  | Coq_tmQuoteUniverses ->
+    tmMap (fun x -> failwith "tmQuoteUniverses") tmQuoteUniverses
+  | Coq_tmQuoteConstant (kn, b) ->
+    tmBind (tmQuoteConstant (to_kername kn) b)
+           (fun x -> Obj.magic (tmOfConstantEntry x))
+  | Coq_tmInductive i ->
+    tmMap (fun _ -> Obj.magic ()) (tmInductive (to_mie i))
+  | Coq_tmExistingInstance k ->
+    Obj.magic (tmExistingInstance (to_kername k))
+  | Coq_tmInferInstance t ->
+    tmBind (tmInferInstance (to_constr t))
+      (function
+          None -> Obj.magic None
+        | Some inst -> Obj.magic (tmMap (fun x -> Some x) (tmOfConstr inst)))
+
+let run_vernac (c : 'a coq_TM) : unit =
+  Plugin_core.run_vernac (interp_tm (Obj.magic c))
diff --git a/template-coq/src/run_extractable.mli b/template-coq/src/run_extractable.mli
new file mode 100644
index 000000000..28ab45e4c
--- /dev/null
+++ b/template-coq/src/run_extractable.mli
@@ -0,0 +1,11 @@
+open Extractable
+open Plugin_core
+open BasicAst
+
+open Quoter
+open Ast_quoter
+
+
+val interp_tm : Extractable.__ coq_TM -> Extractable.__ Plugin_core.tm
+
+val run_vernac : 'a coq_TM -> unit
diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
index 151fb0f0b..f627da330 100644
--- a/template-coq/src/run_template_monad.ml
+++ b/template-coq/src/run_template_monad.ml
@@ -6,11 +6,14 @@ open Redops
 open Genredexpr
 open Pp (* this adds the ++ to the current scope *)
 
+open Tm_util
 open Quoter
+open Denote
 open Constr_quoter
-open TemplateCoqQuoter
 open Template_monad
-open Denote
+open Constr_denoter
+
+open CoqLiveDenoter
 
 let unquote_reduction_strategy env evm trm (* of type reductionStrategy *) : Redexpr.red_expr =
   let (trm, args) = app_full trm [] in
@@ -71,7 +74,7 @@ let unquote_map_option f trm =
   else
     not_supported_verb trm "unquote_map_option"
 
-let denote_option = unquote_map_option (fun x -> x)
+let unquote_option = unquote_map_option (fun x -> x)
 
 
 
@@ -233,14 +236,14 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
       let name = unquote_ident (reduce_all env evm name) in
       let evm,body = denote_term evm (reduce_all env evm body) in
       let evm,typ =
-        match denote_option typ with
+        match unquote_option typ with
         | None -> (evm, None)
         | Some t ->
           let (evm, t) = denote_term evm (reduce_all env evm t) in
           (evm, Some t)
       in
       let poly = Flags.is_universe_polymorphism () in
-      PluginCore.run (PluginCore.tmDefinition name ~poly typ body) env evm
+      Plugin_core.run (Plugin_core.tmDefinition name ~poly typ body) env evm
         (fun env evm res -> k (env, evm, quote_kn res))
 
   | TmAxiom (name,typ) ->
@@ -259,7 +262,7 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
       let name = unquote_ident (reduce_all env evm name) in
       let evm,typ = denote_term evm (reduce_all env evm typ) in
       let poly = Flags.is_universe_polymorphism () in
-      PluginCore.run (PluginCore.tmAxiom name ~poly typ) env evm
+      Plugin_core.run (Plugin_core.tmAxiom name ~poly typ) env evm
         (fun a b c -> k (a,b,quote_kn c))
 
   | TmLemma (name,typ) ->
@@ -287,7 +290,7 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
     let ident = unquote_ident (reduce_all env evm name) in
     let evm,typ = denote_term evm (reduce_all env evm typ) in
     let poly = Flags.is_universe_polymorphism () in
-    PluginCore.run (PluginCore.tmLemma ident ~poly typ) env evm
+    Plugin_core.run (Plugin_core.tmLemma ident ~poly typ) env evm
       (fun env evm kn -> k (env, evm, quote_kn kn))
 
   | TmQuote (false, trm) ->
@@ -297,32 +300,49 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
   | TmQuote (true, trm) ->
     let qt = TermReify.quote_term_rec env trm in
     k (env, evm, qt)
-  | TmQuoteInd name ->
+  | TmQuoteInd (name, strict) ->
        let name = unquote_string (reduce_all env evm name) in
-       let (dp, nm) = split_name name in
+       let (dp, nm) = Quoted.split_name name in
        (match Nametab.locate (Libnames.make_qualid dp nm) with
-        | Globnames.IndRef ni ->
-           let t = TermReify.quote_mind_decl env (fst ni) in
-           let _, args = Constr.destApp t in
-           (match args with
-            | [|kn; decl|] ->
-               k (env, evm, decl)
-            | _ -> bad_term_verb t "anomaly in quoting of inductive types")
+        | Globnames.IndRef (ind, _) ->
+          let _ =
+            let kn = Names.KerName.to_string (Names.MutInd.canonical ind) in
+            if strict && kn <> name then
+              CErrors.user_err (str "strict mode not canonical: \"" ++ str name ++ str "\" <> \"" ++ str kn ++ str "\"")
+            else ()
+          in
+          let t = TermReify.quote_mind_decl env ind in
+          let _, args = Constr.destApp t in
+          (match args with
+           | [|kn; decl|] ->
+             k (env, evm, decl)
+           | _ -> bad_term_verb t "anomaly in quoting of inductive types")
         (* quote_mut_ind produce an entry rather than a decl *)
         (* let c = Environ.lookup_mind (fst ni) env in (\* FIX: For efficienctly, we should also export (snd ni)*\) *)
         (* TermReify.quote_mut_ind env c *)
         | _ -> CErrors.user_err (str name ++ str " does not seem to be an inductive."))
-  | TmQuoteConst (name,bypass) ->
+  | TmQuoteConst (name, bypass, strict) ->
+    begin
        let name = unquote_string (reduce_all env evm name) in
        let bypass = unquote_bool (reduce_all env evm bypass) in
-       let entry = TermReify.quote_entry_aux bypass env evm name in
-       let entry =
-         match entry with
-         | Some (Left cstentry) -> TemplateCoqQuoter.quote_constant_entry cstentry
-         | Some (Right _) -> CErrors.user_err (str name ++ str " refers to an inductive")
-         | None -> bad_term_verb pgm "anomaly in QuoteConstant"
+       let cmd =
+         let open Plugin_core in
+         tmBind (tmAboutString name)
+           (function
+               None -> tmFail (str "not found: " ++ str name)
+             | Some (Globnames.ConstRef cnst) ->
+               let kn = KerName.to_string (Names.Constant.canonical cnst) in
+               if strict && kn <> name then
+                 tmFail (str "strict mode not canonical: \"" ++ str name ++ str "\" <> \"" ++ str kn ++ str "\"")
+               else
+                 with_env_evm (fun env evm ->
+                     let cd = Environ.lookup_constant cnst env in
+                     tmReturn (TermReify.quote_constant_body bypass env evm cd))
+             | Some _ ->
+               tmFail (str "\"" ++ str name ++ str "\" does not refer to a constant"))
        in
-       k (env, evm, entry)
+       Plugin_core.run cmd env evm (fun a b c -> k (a,b, TemplateCoqQuoter.quote_constant_entry c))
+     end
   | TmQuoteUnivs ->
     let univs = Environ.universes env in
     k (env, evm, quote_ugraph univs)
@@ -331,14 +351,14 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
     k (env, evm, unit_tt)
   | TmMsg msg ->
      let msg = unquote_string (reduce_all env evm msg) in
-     PluginCore.run (PluginCore.tmMsg msg) env evm
+     Plugin_core.run (Plugin_core.tmMsg msg) env evm
       (fun env evm _ -> k (env, evm, unit_tt))
   | TmFail trm ->
     let err = unquote_string (reduce_all env evm trm) in
     CErrors.user_err (str err)
   | TmAbout id ->
     let id = Libnames.qualid_of_string (unquote_string id) in
-    PluginCore.run (PluginCore.tmAbout id) env evm
+    Plugin_core.run (Plugin_core.tmAbout id) env evm
       (fun env evm -> function
            None -> k (env, evm, Constr.mkApp (cNone, [|tglobal_reference|]))
          | Some gr ->
@@ -357,7 +377,7 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
   | TmEvalTerm (s,trm) ->
     let red = unquote_reduction_strategy env evm (reduce_all env evm s) in
     let evm,trm = denote_term evm (reduce_all env evm trm) in
-    PluginCore.run (PluginCore.tmEval red trm) env evm
+    Plugin_core.run (Plugin_core.tmEval red trm) env evm
       (fun env evm trm -> k (env, evm, TermReify.quote_term env trm))
   | TmMkInductive mind ->
     declare_inductive env evm mind;
@@ -399,7 +419,7 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
   | TmInferInstance (s, typ) ->
     begin
       let evm, typ =
-        match denote_option s with
+        match unquote_option s with
           Some s ->
           let red = unquote_reduction_strategy env evm s in
           reduce env evm red typ
@@ -412,7 +432,7 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
     end
   | TmInferInstanceTerm typ ->
     let evm,typ = denote_term evm (reduce_all env evm typ) in
-    PluginCore.run (PluginCore.tmInferInstance typ) env evm
+    Plugin_core.run (Plugin_core.tmInferInstance typ) env evm
       (fun env evm -> function
            None -> k (env, evm, Constr.mkApp (cNone, [| tTerm|]))
          | Some trm ->
@@ -420,5 +440,5 @@ let rec run_template_program_rec ?(intactic=false) (k : Environ.env * Evd.evar_m
            k (env, evm, Constr.mkApp (cSome, [| tTerm; qtrm |])))
   | TmPrintTerm trm ->
     let evm,trm = denote_term evm (reduce_all env evm trm) in
-    PluginCore.run (PluginCore.tmPrint trm) env evm
+    Plugin_core.run (Plugin_core.tmPrint trm) env evm
       (fun env evm _ -> k (env, evm, unit_tt))
diff --git a/template-coq/src/template_coq.mlpack b/template-coq/src/template_coq.mlpack
index b97bb642d..f1093ea95 100644
--- a/template-coq/src/template_coq.mlpack
+++ b/template-coq/src/template_coq.mlpack
@@ -1,8 +1,12 @@
 Tm_util
+Quoted
 Quoter
+Denote
+Constr_quoted
 Constr_quoter
+Constr_denoter
 Template_monad
-Denote
-PluginCore
+
+Plugin_core
 Run_template_monad
 G_template_coq
diff --git a/template-coq/src/template_monad.ml b/template-coq/src/template_monad.ml
index 9f46527da..90c420af4 100644
--- a/template-coq/src/template_monad.ml
+++ b/template-coq/src/template_monad.ml
@@ -1,9 +1,8 @@
 open Univ
 open Names
-open Constr_quoter
 open Pp
 
-open Quoter
+open Tm_util
 
 
 let resolve_symbol_p (path : string list) (tm : string) : global_reference =
@@ -128,8 +127,8 @@ let (ttmReturn,
    r_template_monad_type_p "tmCurrentModPath",
 
    r_template_monad_type_p "tmQuoteInductive",
-   r_template_monad_type_p "tmQuoteUniverses",
    r_template_monad_type_p "tmQuoteConstant",
+   r_template_monad_type_p "tmQuoteUniverses",
 
    r_template_monad_type_p "tmInductive",
 
@@ -168,8 +167,8 @@ type template_monad =
 
     (* quoting *)
   | TmQuote of bool * Constr.t  (* only Prop *)
-  | TmQuoteInd of Constr.t
-  | TmQuoteConst of Constr.t * Constr.t
+  | TmQuoteInd of Constr.t * bool (* strict *)
+  | TmQuoteConst of Constr.t * Constr.t * bool (* strict *)
   | TmQuoteUnivs
 
   | TmUnquote of Constr.t                   (* only Prop *)
@@ -309,22 +308,31 @@ let next_action env evd (pgm : constr) : template_monad * _ =
       (TmQuote (true,trm), universes)
     | _ -> monad_failure "tmQuoteRec" 2
 
-  else if Globnames.eq_gr glob_ref ptmQuoteInductive || Globnames.eq_gr glob_ref ttmQuoteInductive then
+  else if Globnames.eq_gr glob_ref ptmQuoteInductive then
+    match args with
+    | name::[] ->
+      (TmQuoteInd (name, false), universes)
+    | _ -> monad_failure "tmQuoteInductive" 1
+  else if Globnames.eq_gr glob_ref ttmQuoteInductive then
     match args with
     | name::[] ->
-      (TmQuoteInd name, universes)
+      (TmQuoteInd (name, true), universes)
     | _ -> monad_failure "tmQuoteInductive" 1
   else if Globnames.eq_gr glob_ref ptmQuoteUniverses || Globnames.eq_gr glob_ref ttmQuoteUniverses then
     match args with
     | [] ->
       (TmQuoteUnivs, universes)
     | _ -> monad_failure "tmQuoteUniverses" 0
-  else if Globnames.eq_gr glob_ref ptmQuoteConstant || Globnames.eq_gr glob_ref ttmQuoteConstant then
+  else if Globnames.eq_gr glob_ref ptmQuoteConstant then
     match args with
     | name::bypass::[] ->
-      (TmQuoteConst (name, bypass), universes)
+      (TmQuoteConst (name, bypass, false), universes)
+    | _ -> monad_failure "tmQuoteConstant" 2
+  else if Globnames.eq_gr glob_ref ttmQuoteConstant then
+    match args with
+    | name::bypass::[] ->
+      (TmQuoteConst (name, bypass, true), universes)
     | _ -> monad_failure "tmQuoteConstant" 2
-
   else if Globnames.eq_gr glob_ref ptmMkInductive then
     match args with
     | mind::[] -> (TmMkInductive mind, universes)
diff --git a/template-coq/src/template_monad.mli b/template-coq/src/template_monad.mli
index 8bd0b8e46..bb67f6a35 100644
--- a/template-coq/src/template_monad.mli
+++ b/template-coq/src/template_monad.mli
@@ -37,8 +37,8 @@ type template_monad =
 
     (* quoting *)
   | TmQuote of bool * Constr.t  (* only Prop *)
-  | TmQuoteInd of Constr.t
-  | TmQuoteConst of Constr.t * Constr.t
+  | TmQuoteInd of Constr.t * bool
+  | TmQuoteConst of Constr.t * Constr.t * bool
   | TmQuoteUnivs
 
   | TmUnquote of Constr.t                   (* only Prop *)
diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml
index 507ffa3bc..e9e811fbd 100644
--- a/template-coq/src/tm_util.ml
+++ b/template-coq/src/tm_util.ml
@@ -1,4 +1,37 @@
+open Pp
+
+let contrib_name = "template-coq"
+
+let gen_constant_in_modules locstr dirs s =
+  Universes.constr_of_global (Coqlib.gen_reference_in_modules locstr dirs s)
+
+
+let opt_debug = ref false
+
+let debug (m : unit ->Pp.t) =
+  if !opt_debug then
+    Feedback.(msg_debug (m ()))
+  else
+    ()
+
 let rec app_full trm acc =
   match Constr.kind trm with
     Constr.App (f, xs) -> app_full f (Array.to_list xs @ acc)
   | _ -> (trm, acc)
+
+let pr_constr trm =
+  let (evm, env) = Pfedit.get_current_context () in
+  Printer.pr_constr_env env evm trm
+
+let not_supported trm =
+  CErrors.user_err (str "Not Supported:" ++ spc () ++ pr_constr trm)
+
+let not_supported_verb trm rs =
+  CErrors.user_err (str "Not Supported raised at " ++ str rs ++ str ":" ++ spc () ++ pr_constr trm)
+
+let bad_term trm =
+  CErrors.user_err (str "Bad term:" ++ spc () ++ pr_constr trm)
+
+let bad_term_verb trm rs =
+  CErrors.user_err (str "Bad term:" ++ spc () ++ pr_constr trm
+                    ++ spc () ++ str " Error: " ++ str rs)
diff --git a/template-coq/test-plugin/test.v b/template-coq/test-plugin/test.v
new file mode 100644
index 000000000..bd2287f22
--- /dev/null
+++ b/template-coq/test-plugin/test.v
@@ -0,0 +1 @@
+Declare ML Module "meta_coq_plugin_template".
\ No newline at end of file
diff --git a/template-coq/theories/.gitignore b/template-coq/theories/.gitignore
new file mode 100644
index 000000000..d3646e2a9
--- /dev/null
+++ b/template-coq/theories/.gitignore
@@ -0,0 +1,2 @@
+*.mli
+*.ml
\ No newline at end of file
diff --git a/template-coq/theories/Extraction.v b/template-coq/theories/Extraction.v
index cbe4384b8..45222293a 100644
--- a/template-coq/theories/Extraction.v
+++ b/template-coq/theories/Extraction.v
@@ -4,8 +4,8 @@
     should use these same directives for consistency.
 *)
 
-From Template Require All.
-
+(* From Template Require All. *)
+Require Import Template.utils.
 Require Import FSets.
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlString ExtrOcamlZInt.
@@ -18,9 +18,15 @@ Extract Constant utils.ascii_compare =>
  "fun x y -> match Char.compare x y with 0 -> Eq | x when x < 0 -> Lt | _ -> Gt".
 
 Extraction Blacklist config uGraph univ Ast String List Nat Int
-           UnivSubst Typing Checker Retyping OrderedType.
+           UnivSubst Typing Checker Retyping OrderedType Logic Common.
 Set Warnings "-extraction-opaque-accessed".
 
-Recursive Extraction Library TypingWf.
-Recursive Extraction Library Checker.
-Recursive Extraction Library Retyping.
+Require Export Template.Ast.
+
+Cd "gen-src".
+
+Require Import Template.TemplateMonad.Extractable.
+
+Recursive Extraction Library Extractable.
+
+Cd "..".
\ No newline at end of file
diff --git a/template-coq/theories/TemplateMonad/Extractable.v b/template-coq/theories/TemplateMonad/Extractable.v
index 054079e6d..a6a382c2b 100644
--- a/template-coq/theories/TemplateMonad/Extractable.v
+++ b/template-coq/theories/TemplateMonad/Extractable.v
@@ -14,7 +14,6 @@ Set Printing Universes.
 
  *)
 
-
 Cumulative Inductive TM@{t} : Type@{t} -> Type :=
 (* Monadic operations *)
 | tmReturn {A:Type@{t}}
@@ -43,16 +42,17 @@ Cumulative Inductive TM@{t} : Type@{t} -> Type :=
 (* Guaranteed to not cause "... already declared" error *)
 | tmFreshName : ident -> TM ident
 
-| tmAbout : ident -> TM (option global_reference)
+| tmAbout : qualid -> TM (option global_reference)
 | tmCurrentModPath : TM string
 
 (* Quote the body of a definition or inductive. *)
-| tmQuoteInductive (nm : kername)
+| tmQuoteInductive (nm : kername) (* nm is the kernel name of the mutind *)
   : TM mutual_inductive_body
-| tmQuoteUniverses : TM uGraph.t
 | tmQuoteConstant (nm : kername) (bypass_opacity : bool)
   : TM constant_entry
 
+| tmQuoteUniverses : TM uGraph.t
+
 (* unquote before making the definition *)
 (* FIXME take an optional universe context as well *)
 | tmInductive : mutual_inductive_entry -> TM unit
@@ -98,4 +98,4 @@ Definition tmDefinitionRed (i : ident) (rd : reductionStrategy)
 
 Definition tmInferInstanceRed (rd : reductionStrategy) (type : Ast.term)
   : TM (option Ast.term) :=
-  tmBind (tmEval rd type) (fun type => tmInferInstance type).
\ No newline at end of file
+  tmBind (tmEval rd type) (fun type => tmInferInstance type).
diff --git a/test-suite/extractable.v b/test-suite/extractable.v
index 5906586c9..8459221a1 100644
--- a/test-suite/extractable.v
+++ b/test-suite/extractable.v
@@ -7,7 +7,8 @@ From Template.TemplateMonad Require Import
 
 Local Open Scope string_scope.
 
-Notation "<% x %>" := (ltac:(let p y := exact y in quote_term x p)).
+Notation "<% x %>" := (ltac:(let p y := exact y in quote_term x p))
+   (only parsing).
 
 Run TemplateProgram
     (tmBind (tmReturn 1) (fun x => tmMsg (utils.string_of_nat x))).
@@ -73,3 +74,10 @@ Print thing.
 Run TemplateProgram
     (tmBind tmCurrentModPath
             tmMsg).
+
+
+Fail Run TemplateProgram (tmQuoteInductive "nat").
+Run TemplateProgram (tmQuoteInductive "Coq.Init.Datatypes.nat").
+
+Fail Run TemplateProgram (tmQuoteConstant "plus" true).
+Run TemplateProgram (tmQuoteConstant "Coq.Init.Nat.add" true).
\ No newline at end of file