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

4 files changed, 28 insertions, 0 deletions

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))