diff --git a/src/reify.ml4 b/src/reify.ml4
index 6c6e36f8d..16c586f4c 100644
--- a/src/reify.ml4
+++ b/src/reify.ml4
@@ -13,8 +13,8 @@ let _ = Goptions.declare_bool_option {
 }
 
 (* whether Set Template Cast Propositions is on, as needed for erasure in Certicoq *)
-let is_cast_prop () = !cast_prop                     
-                     
+let is_cast_prop () = !cast_prop
+
 let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x)
 
 module TermReify =
@@ -99,7 +99,7 @@ struct
   let sSet = r_reify "sSet"
   let sType = r_reify "sType"
   let tident = r_reify "ident"
-  let tInd = r_reify "inductive"
+  let tIndTy = r_reify "inductive"
   let tmkInd = r_reify "mkInd"
   let (tTerm,tRel,tVar,tMeta,tEvar,tSort,tCast,tProd,
        tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tUnknown) =
@@ -164,19 +164,32 @@ struct
 
   let quote_bool b =
     if b then ttrue else tfalse
-
-  let quote_char c =
-    let i = int_of_char c in
+                           
+  let quote_char i =
     Term.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 quote_string s =
+    let len = String.length s in
     let rec go from acc =
       if from < 0 then acc
       else
-	go (from - 1) (Term.mkApp (tString, [| quote_char (String.get s from) ; acc |]))
+        let term = Term.mkApp (tString, [| quote_char (String.get s from) ; acc |]) in
+        go (from - 1) term
     in
-    go (String.length s - 1) tEmptyString
+    go (len - 1) tEmptyString
+                      
+  let quote_string s =
+    try Hashtbl.find string_hash s
+    with Not_found ->
+      let term = quote_string s in
+      Hashtbl.add string_hash s term; term
 
   let quote_ident i =
     let s = Names.string_of_id i in
@@ -288,7 +301,7 @@ struct
       | Term.Case (ci,a,b,e) ->
         let ind = quote_inductive env ci.Term.ci_ind in
         let npar = int_to_nat ci.Term.ci_npar in
-        let info = pair tInd tnat ind npar in
+        let info = pair tIndTy tnat ind npar in
 	let (a',acc) = quote_term acc env a in
 	let (b',acc) = quote_term acc env b in
 	let (branches,acc) =
@@ -761,7 +774,7 @@ let check_inside_section () =
     Errors.errorlabstrm "Quote" (Pp.str "You can not quote within a section.")
   else ()
 
-
+open Pp
 
 TACTIC EXTEND get_goal
     | [ "quote_term" constr(c) tactic(tac) ] ->
@@ -797,10 +810,8 @@ VERNAC COMMAND EXTEND Make_vernac CLASSIFIED AS SIDEFF
 	let (evm,env) = Lemmas.get_current_context () in
 	let def = Constrintern.interp_constr env evm def in
 	let trm = TermReify.quote_term env (fst def) in
-	let result = Constrextern.extern_constr true env evm trm in
-	declare_definition name
-	  (Decl_kinds.Global, false, Decl_kinds.Definition)
-	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
+	ignore(Declare.declare_definition ~kind:Decl_kinds.Definition name
+                                          (trm, Univ.ContextSet.empty)) ]
 END;;
 
 VERNAC COMMAND EXTEND Make_vernac_reduce CLASSIFIED AS SIDEFF
@@ -812,10 +823,8 @@ VERNAC COMMAND EXTEND Make_vernac_reduce CLASSIFIED AS SIDEFF
 	let red = fst (Redexpr.reduction_of_red_expr env red) in
 	let def = red env evm2 (fst def) in
 	let trm = TermReify.quote_term env (snd def) in
-	let result = Constrextern.extern_constr true env (fst def) trm in
-	declare_definition name
-	  (Decl_kinds.Global, false, Decl_kinds.Definition)
-	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
+	ignore(Declare.declare_definition ~kind:Decl_kinds.Definition
+                                          name (trm, Univ.ContextSet.empty)) ]
 END;;
 
 
@@ -825,12 +834,12 @@ VERNAC COMMAND EXTEND Make_recursive CLASSIFIED AS SIDEFF
 	let (evm,env) = Lemmas.get_current_context () in
 	let def = Constrintern.interp_constr env evm def in
 	let trm = TermReify.quote_term_rec env (fst def) in
-	let result = Constrextern.extern_constr true env evm trm in
-	declare_definition name
-	  (Decl_kinds.Global, false, Decl_kinds.Definition)
-	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
+	ignore(Declare.declare_definition 
+	  ~kind:Decl_kinds.Definition name
+	  (trm, (* No new universe constraints can be generated by typing the AST *)
+           Univ.ContextSet.empty)) ]
 END;;
-
+        
 VERNAC COMMAND EXTEND Unquote_vernac CLASSIFIED AS SIDEFF
     | [ "Make" "Definition" ident(name) ":=" constr(def) ] ->
       [ check_inside_section () ;