From d391cece149b0eae79d5a23023a7f58508437083 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 13 May 2006 15:12:04 +0000 Subject: [PATCH] fixed some bugs --- helm/software/components/grafite/grafiteAstPp.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 412fd57d5..ab27e853e 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -72,6 +72,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = function | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term + | Auto (_,_,_,Some kind,_) -> "auto " ^ kind | Auto _ -> "auto" | Assumption _ -> "assumption" | Change (_, where, with_what) -> @@ -117,7 +118,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Fourier _ -> "fourier" | IdTac _ -> "id" | Injection (_, term) -> "injection " ^ term_pp term - | Intros (_, None, []) -> "intro" + | Intros (_, None, []) -> "intros" | Inversion (_, term) -> "inversion " ^ term_pp term | Intros (_, num, idents) -> sprintf "intros%s%s" @@ -202,7 +203,7 @@ let pp_coercion uri do_composites = (if do_composites then "compounds" else "no compounds") let pp_command ~obj_pp = function - | Include (_,path) -> "include " ^ path + | Include (_,path) -> "include \"" ^ path ^ "\"" | Qed _ -> "qed" | Drop _ -> "drop" | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value @@ -243,12 +244,12 @@ and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs = let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = function - | Macro (_, macro) -> pp_macro ~term_pp macro + | Macro (_, macro) -> pp_macro ~term_pp macro ^ "." | Tactical (_, tac, Some punct) -> pp_tactical ~lazy_term_pp ~term_pp tac ^ pp_tactical ~lazy_term_pp ~term_pp punct | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac - | Command (_, cmd) -> pp_command ~obj_pp cmd + | Command (_, cmd) -> pp_command ~obj_pp cmd ^ "." let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function @@ -258,5 +259,5 @@ let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function - | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex ^ "." + | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c -- 2.39.2