]> matita.cs.unibo.it Git - helm.git/commitdiff
DoubleTypeInference: added a comment on "does_not_occur"
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 8 May 2007 19:04:10 +0000 (19:04 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 8 May 2007 19:04:10 +0000 (19:04 +0000)
GrafiteAstPp: rendering of clear tactic fixed

helm/software/components/cic_acic/doubleTypeInference.ml
helm/software/components/grafite/grafiteAstPp.ml

index ca5848369c8f735bf410d5308daa67dfe7c9c72a..905d1e6bc0be63568a8998ac6936f48cb59d2a78 100644 (file)
@@ -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 
index 67f771fbe5e45d23e7aa1fb99d941091c6d2b52b..1b73d62de66dc638df803e136309da1e7fc645d3 100644 (file)
@@ -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) ->