X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=9d8d41537fdcbbb198c67a3b031c278a06a82b40;hb=63e7ef727ce32552106c4d8f3030fd264532fffe;hp=df436e7097cefe67fb842f59414a9f3258ad6b12;hpb=6a5e51c1cf9a56c74a8b53a9b8bc5aa686c9780e;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index df436e709..9d8d41537 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -114,6 +114,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   (* First order tactics *)
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyRule (_, term) -> "apply rule " ^ term_pp term
   | ApplyP (_, term) -> "applyP " ^ term_pp term
   | ApplyS (_, term, params) ->
      "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
@@ -248,7 +249,7 @@ let pp_arg ~term_pp arg =
    else
      "(" ^ s ^ ")"
   
-let pp_macro ~term_pp = 
+let pp_macro ~term_pp ~lazy_term_pp = 
   let term_pp = pp_arg ~term_pp in
   let style_pp = function
      | Declarative         -> ""
@@ -260,15 +261,16 @@ let pp_macro ~term_pp =
   in
   let flavour_pp = function
      | None                   -> ""
-     | Some `Definition       -> "as definition"
-     | Some `MutualDefinition -> "as mutual"
-     | Some `Fact             -> "as fact"
-     | Some `Lemma            -> "as lemma"
-     | Some `Remark           -> "as remark"
-     | Some `Theorem          -> "as theorem"
-     | Some `Variant          -> "as variant"
-     | Some `Axiom            -> "as axiom"
+     | Some `Definition       -> " as definition"
+     | Some `MutualDefinition -> " as mutual"
+     | Some `Fact             -> " as fact"
+     | Some `Lemma            -> " as lemma"
+     | Some `Remark           -> " as remark"
+     | Some `Theorem          -> " as theorem"
+     | Some `Variant          -> " as variant"
+     | Some `Axiom            -> " as axiom"
   in
+  let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in
   function 
   (* Whelp *)
   | WInstance (_, term) -> "whelp instance " ^ term_pp term
@@ -277,6 +279,8 @@ let pp_macro ~term_pp =
   | WElim (_, t) -> "whelp elim " ^ term_pp t
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
+  | Eval (_, kind, term) -> 
+      Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term) 
   | Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
   | Hint (_, true) -> "hint rewrite"
   | Hint (_, false) -> "hint"
@@ -347,7 +351,7 @@ let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
 
 let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
   function
-  | Macro (_, macro) -> pp_macro ~term_pp macro ^ "."
+  | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
   | Tactic (_, Some tac, punct) ->
       pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac
       ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct