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

5 files changed, 23 insertions, 5 deletions

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