DoubleTypeInference: added a comment on "does_not_occur"

GrafiteAstPp: rendering of clear tactic fixed

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index ca5848369c8f735bf410d5308daa67dfe7c9c72a..905d1e6bc0be63568a8998ac6936f48cb59d2a78 100644 (file)
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -51,6 +51,8 @@ let rec does_not_occur n =
   function
      C.Rel m when m = n -> false
    | C.Rel _
+(* FG/CSC: maybe we assume the meta is guarded so we do not recur on its *)
+(*         explicit subsitutions (copied from the kernel) ???            *)
    | C.Meta _
    | C.Sort _
    | C.Implicit _ -> true 

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 67f771fbe5e45d23e7aa1fb99d941091c6d2b52b..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) ->