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

1 files changed, 9 insertions, 0 deletions

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