DoubleTypeInference: added a comment on "does_not_occur"

[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 3602e9df526ad60c25e27500baca1ba1bb9c6cab..1b73d62de66dc638df803e136309da1e7fc645d3 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -32,6 +32,7 @@ let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
 
 let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
+let pp_hyps idents = String.concat " " idents
 
 let pp_reduction_kind ~term_pp = function
   | `Normalize -> "normalize"
@@ -101,8 +102,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       pp_intros_specs (None, idents) 
   | Change (_, where, with_what) ->
       Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
-  | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_idents ids)
-  | ClearBody (_,id) -> Printf.sprintf "clearbody %s" id
+  | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
+  | ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id])
   | Constructor (_,n) -> "constructor " ^ string_of_int n
   | Contradiction _ -> "contradiction"
   | Cut (_, ident, term) ->
@@ -305,9 +306,9 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
   | Note (_,"") -> Printf.sprintf "\n"
-  | Note (_,str) -> Printf.sprintf "(* %s *)\n" str
+  | Note (_,str) -> Printf.sprintf "\n(* %s *)" str
   | Code (_,code) ->
-      Printf.sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
+      Printf.sprintf "\n(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
 
 let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
   function