Ajout de dynamiques pour les quotations constr et tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 143 insertions, 59 deletions

diff --git a/.depend b/.depend
index bfd0cb40b8..4387bcdfed 100644
--- a/.depend
+++ b/.depend
@@ -37,7 +37,7 @@ library/global.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
     library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/univ.cmi 
-library/goptions.cmi: kernel/names.cmi lib/pp.cmi 
+library/goptions.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 library/impargs.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/term.cmi 
 library/indrec.cmi: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -104,11 +104,11 @@ pretyping/pattern.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
 pretyping/pretype_errors.cmi: kernel/environ.cmi kernel/evd.cmi \
     kernel/inductive.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \
     kernel/sign.cmi kernel/term.cmi 
-pretyping/pretyping.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
-    kernel/evd.cmi kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    kernel/term.cmi 
-pretyping/rawterm.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi 
+pretyping/pretyping.cmi: lib/dyn.cmi kernel/environ.cmi \
+    pretyping/evarutil.cmi kernel/evd.cmi kernel/names.cmi \
+    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
+pretyping/rawterm.cmi: lib/dyn.cmi kernel/names.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi 
 pretyping/recordops.cmi: pretyping/classops.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi kernel/term.cmi 
 pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
@@ -452,18 +452,22 @@ library/global.cmx: kernel/environ.cmx kernel/inductive.cmx \
     kernel/instantiate.cmx kernel/names.cmx library/nametab.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx library/summary.cmx \
     kernel/term.cmx lib/util.cmx library/global.cmi 
-library/goptions.cmo: library/lib.cmi library/libobject.cmi kernel/names.cmi \
-    lib/pp.cmi library/summary.cmi lib/util.cmi library/goptions.cmi 
-library/goptions.cmx: library/lib.cmx library/libobject.cmx kernel/names.cmx \
-    lib/pp.cmx library/summary.cmx lib/util.cmx library/goptions.cmi 
+library/goptions.cmo: library/global.cmi library/lib.cmi \
+    library/libobject.cmi kernel/names.cmi lib/pp.cmi library/summary.cmi \
+    kernel/term.cmi lib/util.cmi library/goptions.cmi 
+library/goptions.cmx: library/global.cmx library/lib.cmx \
+    library/libobject.cmx kernel/names.cmx lib/pp.cmx library/summary.cmx \
+    kernel/term.cmx lib/util.cmx library/goptions.cmi 
 library/impargs.cmo: kernel/declarations.cmi kernel/environ.cmi \
     kernel/evd.cmi library/global.cmi kernel/inductive.cmi library/lib.cmi \
     library/libobject.cmi kernel/names.cmi kernel/reduction.cmi \
-    library/summary.cmi kernel/term.cmi lib/util.cmi library/impargs.cmi 
+    kernel/sign.cmi library/summary.cmi kernel/term.cmi kernel/typeops.cmi \
+    lib/util.cmi library/impargs.cmi 
 library/impargs.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/evd.cmx library/global.cmx kernel/inductive.cmx library/lib.cmx \
     library/libobject.cmx kernel/names.cmx kernel/reduction.cmx \
-    library/summary.cmx kernel/term.cmx lib/util.cmx library/impargs.cmi 
+    kernel/sign.cmx library/summary.cmx kernel/term.cmx kernel/typeops.cmx \
+    lib/util.cmx library/impargs.cmi 
 library/indrec.cmo: kernel/declarations.cmi kernel/environ.cmi \
     kernel/indtypes.cmi kernel/inductive.cmi kernel/instantiate.cmi \
     kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
@@ -525,17 +529,17 @@ parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \
     parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi 
 parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+    lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     library/global.cmi library/impargs.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
+    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi pretyping/pretyping.cmi \
     pretyping/rawterm.cmi kernel/reduction.cmi pretyping/retyping.cmi \
     kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \
     parsing/termast.cmi pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi 
 parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \
+    lib/dyn.cmx kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \
     library/global.cmx library/impargs.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
+    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx pretyping/pretyping.cmx \
     pretyping/rawterm.cmx kernel/reduction.cmx pretyping/retyping.cmx \
     kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \
@@ -637,12 +641,12 @@ parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
     kernel/term.cmx kernel/typeops.cmx lib/util.cmx parsing/prettyp.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \
+    lib/dyn.cmi kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \
     library/global.cmi kernel/names.cmi lib/options.cmi pretyping/pattern.cmi \
     lib/pp.cmi kernel/sign.cmi kernel/term.cmi parsing/termast.cmi \
     lib/util.cmi parsing/printer.cmi 
 parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx parsing/esyntax.cmx parsing/extend.cmx \
+    lib/dyn.cmx kernel/environ.cmx parsing/esyntax.cmx parsing/extend.cmx \
     library/global.cmx kernel/names.cmx lib/options.cmx pretyping/pattern.cmx \
     lib/pp.cmx kernel/sign.cmx kernel/term.cmx parsing/termast.cmx \
     lib/util.cmx parsing/printer.cmi 
@@ -717,12 +721,12 @@ pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
     pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmx \
     kernel/term.cmx kernel/typeops.cmx lib/util.cmx pretyping/coercion.cmi 
 pretyping/detyping.cmo: kernel/declarations.cmi library/declare.cmi \
-    kernel/environ.cmi library/global.cmi library/goptions.cmi \
+    kernel/environ.cmi kernel/evd.cmi library/global.cmi library/goptions.cmi \
     library/impargs.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
     lib/util.cmi pretyping/detyping.cmi 
 pretyping/detyping.cmx: kernel/declarations.cmx library/declare.cmx \
-    kernel/environ.cmx library/global.cmx library/goptions.cmx \
+    kernel/environ.cmx kernel/evd.cmx library/global.cmx library/goptions.cmx \
     library/impargs.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
     pretyping/rawterm.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
     lib/util.cmx pretyping/detyping.cmi 
@@ -761,7 +765,7 @@ pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/evd.cmx \
     pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/type_errors.cmx pretyping/pretype_errors.cmi 
 pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
-    pretyping/coercion.cmi library/declare.cmi kernel/environ.cmi \
+    pretyping/coercion.cmi library/declare.cmi lib/dyn.cmi kernel/environ.cmi \
     pretyping/evarconv.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     library/indrec.cmi kernel/inductive.cmi kernel/instantiate.cmi \
     kernel/names.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
@@ -770,7 +774,7 @@ pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
     kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
     pretyping/pretyping.cmi 
 pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \
-    pretyping/coercion.cmx library/declare.cmx kernel/environ.cmx \
+    pretyping/coercion.cmx library/declare.cmx lib/dyn.cmx kernel/environ.cmx \
     pretyping/evarconv.cmx pretyping/evarutil.cmx kernel/evd.cmx \
     library/indrec.cmx kernel/inductive.cmx kernel/instantiate.cmx \
     kernel/names.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
@@ -778,10 +782,10 @@ pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \
     pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
     pretyping/pretyping.cmi 
-pretyping/rawterm.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi pretyping/rawterm.cmi 
-pretyping/rawterm.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx pretyping/rawterm.cmi 
+pretyping/rawterm.cmo: lib/dyn.cmi kernel/names.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/rawterm.cmi 
+pretyping/rawterm.cmx: lib/dyn.cmx kernel/names.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/rawterm.cmi 
 pretyping/recordops.cmo: pretyping/classops.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi lib/pp.cmi \
     library/summary.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
@@ -901,19 +905,21 @@ proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
     lib/dyn.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
     lib/gmap.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \
     library/nametab.cmi library/opaque.cmi lib/options.cmi \
-    pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi library/summary.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \
-    kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi 
+    pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \
+    pretyping/pretyping.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+    kernel/sign.cmi library/summary.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi 
 proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
     parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
     lib/dyn.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
     lib/gmap.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \
     library/nametab.cmx library/opaque.cmx lib/options.cmx \
-    pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx proofs/proof_type.cmx \
-    pretyping/rawterm.cmx kernel/sign.cmx library/summary.cmx \
-    proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \
-    kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi 
+    pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \
+    pretyping/pretyping.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+    kernel/sign.cmx library/summary.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx proofs/tactic_debug.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi 
 proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \
     kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evarutil.cmi \
     kernel/evd.cmi library/global.cmi kernel/instantiate.cmi proofs/logic.cmi \
@@ -999,15 +1005,15 @@ tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi
 tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \
     pretyping/evarutil.cmi kernel/evd.cmi lib/explore.cmi proofs/logic.cmi \
     kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi lib/util.cmi 
+    proofs/proof_type.cmi kernel/reduction.cmi parsing/search.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
 tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \
     pretyping/evarutil.cmx kernel/evd.cmx lib/explore.cmx proofs/logic.cmx \
     kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx lib/util.cmx 
+    proofs/proof_type.cmx kernel/reduction.cmx parsing/search.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
 tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi tactics/hiddentac.cmi \
     tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi kernel/reduction.cmi \
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3f79bed395..bfd4e6685f 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -478,6 +478,8 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	anomaly ("ast_to_rawconstr found operator "^opn^" with "^
 		 (string_of_int (List.length tl))^" arguments")
 
+    | Dynamic (loc,d) -> RDynamic (loc,d)
+
     | _ -> anomaly "ast_to_rawconstr: unexpected ast"
 
   and ast_to_eqn n (ids,impls as env) = function
@@ -669,6 +671,18 @@ let interp_rawconstr_wo_glob sigma env lvar com =
 
 (* Functions to parse and interpret constructions *)
 
+(* To embed constr in Coqast.t *)
+let constrIn t = Dynamic (dummy_loc,constr_in t)
+let constrOut = function
+  | Dynamic (_,d) ->
+    if (Dyn.tag d) = "constr" then
+      constr_out d
+    else
+      anomalylabstrm "constrOut" [<'sTR "Dynamic tag should be constr">]
+  | ast ->
+    anomalylabstrm "constrOut"
+      [<'sTR "Not a Dynamic ast: "; print_ast ast>]
+
 let interp_constr sigma env c =
   understand sigma env (interp_rawconstr sigma env c)
 
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index be9c7b1a75..31d96145a5 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -20,6 +20,10 @@ open Pattern
 
 (* Translation from AST to terms. *)
 
+(* To embed constr in Coqast.t *)
+val constrIn : constr -> Coqast.t
+val constrOut : Coqast.t -> constr
+
 val interp_rawconstr     : 'a evar_map -> env -> Coqast.t -> rawconstr
 val interp_constr        : 'a evar_map -> env -> Coqast.t -> constr
 val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
diff --git a/parsing/printer.ml b/parsing/printer.ml
index b1a0c65172..b1d85e53a0 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -56,6 +56,9 @@ let globpr gt = match gt with
       global_ind_name (section_path sl, tyi)
   | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
       global_constr_name ((section_path sl, tyi), i)
+  | Dynamic(_,d) ->
+    if (Dyn.tag d) = "constr" then [< 'sTR"<dynamic [constr]>" >]
+    else dfltpr gt
   | gt -> dfltpr gt
 
 let wrap_exception = function
@@ -152,6 +155,12 @@ and default_tacpr = function
     | Node(_,s,[]) -> [< 'sTR s >]
     | Node(_,s,ta) ->
 	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
+    | Dynamic(_,d) as gt ->
+      let tg = Dyn.tag d in
+      if tg = "tactic" then [< 'sTR"<dynamic [tactic]>" >]
+      else if tg = "value" then [< 'sTR"<dynamic [value]>" >]
+      else if tg = "constr" then [< 'sTR"<dynamic [constr]>" >]
+      else dfltpr gt
     | gt -> dfltpr gt 
 
 let pr_var_decl env (id,c,typ) =
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 431743f13a..922c09d28e 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -270,6 +270,7 @@ let rec ast_of_raw = function
 	 | RType _ -> ope("TYPE",[]))
   | RHole _ -> ope("ISEVAR",[])
   | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
+  | RDynamic (loc,d) -> Dynamic (loc,d)
 	
 and ast_of_eqn (_,ids,pl,c) =
   ope("EQN", (ast_of_raw c)::(List.map ast_of_cases_pattern pl))
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6f051b6e3e..2535c2b34e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -534,7 +534,7 @@ let occur_rawconstr id =
 	(array_exists occur tyl) or
 	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
     | RCast (loc,c,t) -> (occur c) or (occur t)
-    | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _) -> false
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5f6a418ebf..cb9e0abd6d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -26,6 +26,7 @@ open Pretype_errors
 open Rawterm
 open Evarconv
 open Coercion
+open Dyn
 
 
 (***********************************************************************)
@@ -102,6 +103,10 @@ let transform_rec loc env sigma (pj,c,lf) indt =
 
 (***********************************************************************)
 
+(* To embed constr in rawconstr *)
+let ((constr_in : constr -> Dyn.t),
+     (constr_out : Dyn.t -> constr)) = create "constr"
+
 let ctxt_of_ids cl = cl
 
 let mt_evd = Evd.empty
@@ -432,6 +437,15 @@ let rec pretype tycon env isevars lvar lmeta = function
       let cj = {uj_val = mkCast (cj.uj_val,tj.utj_val); uj_type=tj.utj_val} in
       inh_conv_coerce_to_tycon loc env isevars cj tycon
 
+  | RDynamic (loc,d) ->
+    if (tag d) = "constr" then
+      let c = constr_out d in
+      let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
+      j
+      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
+    else
+      user_err_loc (loc,"pretype",[< 'sTR "Not a constr tagged Dynamic" >])
+
 (* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *)
 and pretype_type valcon env isevars lvar lmeta = function
   | RHole loc ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index ae6161f502..bf48e305fe 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -60,6 +60,10 @@ val understand_judgment : 'a evar_map -> env -> rawconstr -> unsafe_judgment
 val understand_type_judgment : 'a evar_map -> env -> rawconstr 
   -> unsafe_type_judgment
 
+(* To embed constr in rawconstr *)
+val constr_in : constr -> Dyn.t
+val constr_out : Dyn.t -> constr
+
 (*i*)
 (* Internal of Pretyping...
  * Unused outside, but useful for debugging
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 053c6c39b7..a46a3f8b5b 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -56,6 +56,7 @@ type rawconstr =
   | RSort of loc * rawsort
   | RHole of loc option
   | RCast of loc * rawconstr * rawconstr
+  | RDynamic of loc * Dyn.t
 
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
@@ -87,6 +88,7 @@ let loc_of_rawconstr = function
   | RHole (Some loc) -> loc
   | RHole (None) -> dummy_loc
   | RCast (loc,_,_) -> loc
+  | RDynamic (loc,_) -> loc
 
 let set_loc_of_rawconstr loc = function
   | RRef (_,a)      -> RRef (loc,a)
@@ -103,9 +105,6 @@ let set_loc_of_rawconstr loc = function
   | RSort (_,a)      -> RSort (loc,a) 
   | RHole _          -> RHole (Some loc)
   | RCast (_,a,b)    -> RCast (loc,a,b) 
+  | RDynamic (_,d)   -> RDynamic (loc,d)
 
 let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
-
-
-
-
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 0106fc60ab..22492a6cc6 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -54,6 +54,7 @@ type rawconstr =
   | RSort of loc * rawsort
   | RHole of loc option
   | RCast of loc * rawconstr * rawconstr
+  | RDynamic of loc * Dyn.t
 
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 05d7df7467..ca67f73063 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -48,7 +48,6 @@ type value =
   | VRec of value ref
 
 (* Signature for interpretation: val_interp and interpretation functions *)
-
 and interp_sign =
   { evc : enamed_declarations;
     env : Environ.env;
@@ -145,16 +144,39 @@ let interp_openconstr ist c ocl =
   interp_openconstr_gen ist.evc ist.env
     (constr_list ist.goalopt ist.lfun) ist.lmatch c ocl
 
-(* For user tactics *)
-(*let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t),
-     (ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml"*)
+(* To embed several objects in Coqast.t *)
+let ((tactic_in : (interp_sign -> Coqast.t) -> Dyn.t),
+     (tactic_out : Dyn.t -> (interp_sign -> Coqast.t))) = create "tactic"
+
+let ((value_in : value -> Dyn.t),
+     (value_out : Dyn.t -> value)) = create "value"
+
+let tacticIn t = Dynamic (dummy_loc,tactic_in t)
+let tacticOut = function
+  | Dynamic (_,d) ->
+    if (tag d) = "tactic" then
+      tactic_out d
+    else
+      anomalylabstrm "tacticOut" [<'sTR "Dynamic tag should be tactic">]
+  | ast ->
+    anomalylabstrm "tacticOut"
+      [<'sTR "Not a Dynamic ast: "; print_ast ast>]
+
+let valueIn t = Dynamic (dummy_loc,value_in t)
+let valueOut = function
+  | Dynamic (_,d) ->
+    if (tag d) = "value" then
+      value_out d
+    else
+      anomalylabstrm "valueOut" [<'sTR "Dynamic tag should be value">]
+  | ast ->
+    anomalylabstrm "valueOut"
+      [<'sTR "Not a Dynamic ast: "; print_ast ast>]
 
-let ((ocamlIn : (interp_sign -> Coqast.t) -> Dyn.t),
-     (ocamlOut : Dyn.t -> (interp_sign -> Coqast.t))) = create "ocaml"
+let constrIn = constrIn
+let constrOut = constrOut
 
-(* To provide the tactic expressions *)
-let loc = (0,0)
-let tacticIn t = Dynamic (loc,ocamlIn t)
+let loc = dummy_loc
 
 (* Table of interpretation functions *)
 let interp_tab =
@@ -533,8 +555,13 @@ let rec val_interp ist ast =
            Not_found ->
              val_interp ist (Node(dummy_loc,"APPTACTIC",[ast])))
     | Dynamic(_,t) ->
-      if (tag t) = "ocaml" then
-        let f = (ocamlOut t) in val_interp ist (f ist)
+      let tg = (tag t) in
+      if tg = "tactic" then
+        let f = (tactic_out t) in val_interp ist (f ist)
+      else if tg = "value" then
+        value_out t
+      else if tg = "constr" then
+        VArg (Constr (Pretyping.constr_out t))
       else
         anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",
           [<'sTR "Unknown dynamic ast: "; print_ast ast>])
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 85dc1e2fb5..9a979ea74c 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -38,12 +38,17 @@ and interp_sign =
     goalopt : goal sigma option;
     debug : debug_info }
 
-(* Gives the constr corresponding to a CONSTR [tactic_arg] *)
+(* Gives the constr corresponding to a Constr [tactic_arg] *)
 val constr_of_Constr : tactic_arg -> constr
 
-(* To provide the tactic expressions *)
-val loc : Coqast.loc
+(* To embed several objects in Coqast.t *)
 val tacticIn : (interp_sign -> Coqast.t) -> Coqast.t
+val tacticOut : Coqast.t -> (interp_sign -> Coqast.t)
+val valueIn : value -> Coqast.t
+val valueOut: Coqast.t -> value
+val constrIn : constr -> Coqast.t
+val constrOut : Coqast.t -> constr
+val loc : Coqast.loc
 
 (* Sets the debugger mode *)
 val set_debug : debug_info -> unit