auto => auto new everywhere + minor updates to make more tests pass

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 569b6839928467763c75a2f27886fbc3d6563af7..5644d33d3e8a0cd144a20661d18d31b026de342f 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -158,9 +158,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term 
   | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "("  ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
   | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
-  | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ "(" ^ident^ ")" ^
+  | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
        (match term2 with  None -> " " | Some term2 -> term_pp term2)
-  | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+  | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
   | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
   | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
@@ -198,8 +198,9 @@ let pp_macro ~term_pp =
   | WElim (_, t) -> "whelp elim " ^ term_pp t
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
-  | Check (_, term) -> sprintf "Check %s" (term_pp term)
+  | Check (_, term) -> sprintf "check %s" (term_pp term)
   | Hint _ -> "hint"
+  | Inline (_,suri) -> sprintf "inline %s" suri
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"