From 36856cfaefdb29efec317eb072e06a2b13ed8da6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 8 May 2007 19:04:10 +0000 Subject: [PATCH] DoubleTypeInference: added a comment on "does_not_occur" GrafiteAstPp: rendering of clear tactic fixed --- components/cic_acic/doubleTypeInference.ml | 2 ++ components/grafite/grafiteAstPp.ml | 5 +++-- 2 files changed, 5 insertions(+), 2 deletions(-) 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) -> -- 2.39.2