X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicPp.ml;h=e44c6b5881be2f47d260c66c6ed91142416ffd7a;hb=b65592962c5614981b20154000779805c3620075;hp=954134584b69db831d0d060cc0ed2bd301b4bdb0;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml index 954134584..e44c6b588 100644 --- a/components/cic_proof_checking/cicPp.ml +++ b/components/cic_proof_checking/cicPp.ml @@ -119,7 +119,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 +131,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 +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 @@ -459,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