New tactic cases (still to be documented).

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 0704863f5a779ee28282863c16b38741221ee6a6..0530697ada6b252b580405a4837ef7eca0e5eb68 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -83,6 +83,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
+  | Cases (_, term, idents) -> sprintf "cases " ^ term_pp term ^
+      pp_intros_specs (None, idents) 
   | Change (_, where, with_what) ->
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids)
@@ -140,7 +142,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
         (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
-  | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident
+  | LetIn (_, term, ident) -> sprintf "letin %s \\def %s" ident (term_pp term)
   | Reduce (_, kind, pat) ->
       sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
   | Reflexivity _ -> "reflexivity"
@@ -298,6 +300,7 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
+  | Note (_,"") -> sprintf "\n"
   | Note (_,str) -> sprintf "(* %s *)\n" str
   | Code (_,code) ->
       sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)