new problem:

[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 954134584b69db831d0d060cc0ed2bd301b4bdb0..feca7c3cfe07951bfd32d42ff29e74f0391e976f 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -80,8 +80,10 @@ let rec pp t l =
        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.concat " ; "
          (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+*)
         "]"
     | C.Sort s ->
        (match s with
@@ -119,7 +121,8 @@ let rec pp t l =
               name ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
         with
-         _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+           Sys.Break as exn -> raise exn
+         | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
@@ -130,7 +133,8 @@ let rec pp t l =
                id ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
         with
-         _ ->
+           Sys.Break as exn -> raise exn
+         | _ ->
           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
            string_of_int n2
        )
@@ -311,11 +315,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
@@ -459,8 +458,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