From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 8 May 2007 19:04:10 +0000 (+0000)
Subject: DoubleTypeInference: added a comment on "does_not_occur"
X-Git-Tag: make_still_working~6343
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf45f0f766c147324e587522a4a3761b5ac13415;p=helm.git

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 ca5848369..905d1e6bc 100644
--- 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 67f771fbe..1b73d62de 100644
--- 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) ->