Bug fixed in the guarded_by_descructors function: in some cases the context

[helm.git] / helm / software / components / cic_proof_checking / cicPp.ml

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 32daa4945db882b85614c74d21f44131cfe4a216..06bb082b4110b531209d55321e4aa9e4f4763b15 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -79,10 +79,10 @@ let rec pp t l =
     | C.Var (uri,exp_named_subst) ->
        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
-       "?" ^ (string_of_int n) (* ^ "[" ^ 
+       "?" ^ (string_of_int n) ^ "[" ^ 
         String.concat " ; "
          (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-        "]" *)
+        "]"
     | C.Sort s ->
        (match s with
            C.Prop  -> "Prop"
@@ -95,14 +95,14 @@ let rec pp t l =
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
-          C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
-        | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
+          C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+        | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
        )
     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
     | C.LetIn (b,s,t) ->
-       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -313,11 +313,6 @@ let is_prefix prefix string =
   else None
 
 let remove_prefix prefix (last,string) =
-  if prefix="append" then
-    begin 
-      prerr_endline last;
-      prerr_endline string;
-    end;
   if string = "" then (last,string)
   else 
     match is_prefix prefix string with
@@ -357,7 +352,7 @@ let rec check_rec ctx string_name =
     | Cic.Implicit _ -> string_name
     | Cic.Cast (te,ty) -> check_rec ctx string_name te
     | Cic.Prod (name,so,dest) -> 
-       let _l_string_name = check_rec ctx string_name so in
+       let l_string_name = check_rec ctx string_name so in
        check_rec (name::ctx) string_name dest
     | Cic.Lambda (name,so,dest) -> 
         let string_name =
@@ -390,11 +385,11 @@ let rec check_rec ctx string_name =
          | _ -> assert false) in
        remove_prefix name string_name  
     | Cic.MutCase (_,_,_,te,pl) ->
-       let _strig_name = remove_prefix "match" string_name in
+       let strig_name = remove_prefix "match" string_name in
        let string_name = check_rec ctx string_name te in
         List.fold_right (fun t s -> check_rec ctx s t) pl string_name
     | Cic.Fix (_,fl) ->
-        let _strig_name = remove_prefix "fix" string_name in
+        let strig_name = remove_prefix "fix" string_name in
         let names = List.map (fun (name,_,_,_) -> name) fl in
         let onames =
           List.rev (List.map (function name -> Cic.Name name) names)
@@ -402,7 +397,7 @@ let rec check_rec ctx string_name =
         List.fold_right 
          (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
     | Cic.CoFix (_,fl) ->
-       let _strig_name = remove_prefix "cofix" string_name in
+       let strig_name = remove_prefix "cofix" string_name in
         let names = List.map (fun (name,_,_) -> name) fl in
         let onames =
           List.rev (List.map (function name -> Cic.Name name) names)
@@ -461,8 +456,6 @@ let rec check_names ctx hyp_names conclusion_name t =
        hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
 
 let check name term =
-(*  prerr_endline name;
-  prerr_endline (ppterm term); *)
   let names = Str.split (Str.regexp_string "_to_") name in
   let hyp_names,conclusion_name =
     match List.rev names with