From: Ferruccio Guidi Date: Tue, 8 May 2007 19:04:10 +0000 (+0000) Subject: DoubleTypeInference: added a comment on "does_not_occur" X-Git-Tag: 0.4.95@7852~484 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=36856cfaefdb29efec317eb072e06a2b13ed8da6;p=helm.git DoubleTypeInference: added a comment on "does_not_occur" GrafiteAstPp: rendering of clear tactic fixed --- diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml index ca5848369..905d1e6bc 100644 --- a/components/cic_acic/doubleTypeInference.ml +++ b/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/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 67f771fbe..1b73d62de 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/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) ->