diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /plugins | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'plugins')
49 files changed, 244 insertions, 178 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index d0f81dad..1c021eee 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -404,7 +404,8 @@ let rec canonize_name c = let build_subst uf subst = Array.map (fun i -> try term uf i - with _ -> anomaly "incomplete matching") subst + with e when Errors.noncritical e -> + anomaly "incomplete matching") subst let rec inst_pattern subst = function PVar i -> @@ -730,9 +731,7 @@ let __eps__ = id_of_string "_eps_" let new_state_var typ state = let id = pf_get_new_id __eps__ state.gls in let {it=gl ; sigma=sigma} = state.gls in - let new_hyps = - Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in - let gls = Goal.V82.new_goal_with sigma gl new_hyps in + let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in state.gls<- gls; id diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 95ff4d34..764e36b0 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -129,7 +129,9 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= - try destApp (whd_delta env term) with _ -> raise Not_found in + try destApp (whd_delta env term) + with e when Errors.noncritical e -> raise Not_found + in if eq_constr f (Lazy.force _eq) && (Array.length args)=3 then let patt1,rels1 = pattern_of_constr env sigma args.(1) diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 730051c1..da88d48d 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -75,9 +75,9 @@ let mode_of_pftreestate pts = Mode_proof let get_current_mode () = - try + try mode_of_pftreestate (Pfedit.get_pftreestate ()) - with _ -> Mode_none + with e when Errors.noncritical e -> Mode_none let check_not_proof_mode str = if get_current_mode () = Mode_proof then diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 72caeaed..ab161b35 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -381,7 +381,7 @@ let find_subsubgoal c ctyp skip submetas gls = se.se_meta submetas se.se_meta_list} else dfs (pred n) - with _ -> + with e when Errors.noncritical e -> begin enstack_subsubgoals env se stack gls; dfs n @@ -519,7 +519,10 @@ let decompose_eq id gls = let instr_rew _thus rew_side cut gls0 = let last_id = - try get_last (pf_env gls0) with _ -> error "No previous equality." in + try get_last (pf_env gls0) + with e when Errors.noncritical e -> + error "No previous equality." + in let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = match cut.cut_by with @@ -849,7 +852,7 @@ let build_per_info etype casee gls = let ind = try destInd hd - with _ -> + with e when Errors.noncritical e -> error "Case analysis must be done on an inductive object." in let mind,oind = Global.lookup_inductive ind in let nparams,index = diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 6aa47eff..b7ee3c1a 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -397,8 +397,10 @@ let mono_filename f = in let id = if lang () <> Haskell then default_id - else try id_of_string (Filename.basename f) - with _ -> error "Extraction: provided filename is not a valid identifier" + else + try id_of_string (Filename.basename f) + with e when Errors.noncritical e -> + error "Extraction: provided filename is not a valid identifier" in Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id @@ -473,8 +475,8 @@ let print_structure_to_file (fn,si,mo) dry struc = msg_with ft (d.preamble mo opened unsafe_needs); msg_with ft (d.pp_struct struc); Option.iter close_out cout; - with e -> - Option.iter close_out cout; raise e + with reraise -> + Option.iter close_out cout; raise reraise end; if not dry then Option.iter info_file fn; (* Now, let's print the signature *) @@ -487,8 +489,8 @@ let print_structure_to_file (fn,si,mo) dry struc = msg_with ft (d.sig_preamble mo opened unsafe_needs); msg_with ft (d.pp_sig (signature_of_structure struc)); close_out cout; - with e -> - close_out cout; raise e + with reraise -> + close_out cout; raise reraise end; info_file si) (if dry then None else si); @@ -527,7 +529,9 @@ let rec locate_ref = function | r::l -> let q = snd (qualid_of_reference r) in let mpo = try Some (Nametab.locate_module q) with Not_found -> None - and ro = try Some (Smartlocate.global_with_alias r) with _ -> None + and ro = + try Some (Smartlocate.global_with_alias r) + with e when Errors.noncritical e -> None in match mpo, ro with | None, None -> Nametab.error_global_not_found q diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0a17453c..e5357336 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -149,7 +149,7 @@ let rec handle_exn r n fn_name = function (fun i -> assert ((0 < i) && (i <= n)); MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i))) - with _ -> MLexn s) + with e when Errors.noncritical e -> MLexn s) | a -> ast_map (handle_exn r n fn_name) a (*S Management of type variable contexts. *) @@ -683,7 +683,7 @@ and extract_cst_app env mle mlt kn args = let l,l' = list_chop (projection_arity (ConstRef kn)) mla in if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla - with _ -> mla + with e when Errors.noncritical e -> mla in (* For strict languages, purely logical signatures with at least one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 6c78b533..b6fc5ac8 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -81,7 +81,9 @@ let kn_sig = let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false - | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) + | Tvar i -> + (try pr_id (List.nth vl (pred i)) + with e when Errors.noncritical e -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r | Tglob (IndRef(kn,0),l) when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" -> diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a38b303f..d0bf387a 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -879,7 +879,7 @@ let is_program_branch = function (try ignore (int_of_string (String.sub s n (String.length s - n))); String.sub s 0 n = br - with _ -> false) + with e when Errors.noncritical e -> false) | Tmp _ | Dummy -> false let expand_linear_let o id e = @@ -1312,7 +1312,7 @@ let inline_test r t = let c = match r with ConstRef c -> c | _ -> assert false in let has_body = try constant_has_body (Global.lookup_constant c) - with _ -> false + with e when Errors.noncritical e -> false in has_body && (let t1 = eta_red t in diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 289b2a1d..4e8d8145 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -119,7 +119,8 @@ let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) - with _ -> (str "'a" ++ int i)) + with e when Errors.noncritical e -> + (str "'a" ++ int i)) | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r @@ -188,7 +189,7 @@ let rec pp_expr par env args = let args = list_skipn (projection_arity r) args in let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) - with _ -> apply (pp_global Term r)) + with e when Errors.noncritical e -> apply (pp_global Term r)) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index e0a6e843..497ddf03 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -255,7 +255,7 @@ let safe_basename_of_global r = let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) - with _ -> string_of_id (safe_basename_of_global r) + with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r) let safe_pr_global r = str (string_of_global r) @@ -263,7 +263,7 @@ let safe_pr_global r = str (string_of_global r) let safe_pr_long_global r = try Printer.pr_global r - with _ -> match r with + with e when Errors.noncritical e -> match r with | ConstRef kn -> let mp,_,l = repr_con kn in str ((string_of_mp mp)^"."^(string_of_label l)) @@ -452,7 +452,7 @@ let my_bool_option name initval = (*s Extraction AccessOpaque *) -let access_opaque = my_bool_option "AccessOpaque" false +let access_opaque = my_bool_option "AccessOpaque" true (*s Extraction AutoInline *) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 9d3d8c99..29d41b81 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -85,7 +85,7 @@ let gen_ground_tac flag taco ids bases gl= extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in let result=ground_tac solver startseq gl in qflag:=backup;result - with e ->qflag:=backup;raise e + with reraise ->qflag:=backup;raise reraise (* special for compatibility with Intuition diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 68f112d6..4b07c609 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -129,7 +129,7 @@ let mk_open_instance id gl m t= | _-> anomaly "can't happen" in let ntt=try Pretyping.Default.understand evmap env (raux m rawt) - with _ -> + with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in decompose_lam_n_assum m ntt diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index 043c9e51..1574e21e 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -175,7 +175,7 @@ let unsolvable lie = raise (Failure "contradiction found")) |_->assert false) lr) - with _ -> ()); + with e when Errors.noncritical e -> ()); !res ;; diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index cdd10d70..e0e4f7d6 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -40,7 +40,7 @@ type flin = {fhom: rational Constrhash.t; let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};; -let flin_coef f x = try (Constrhash.find f.fhom x) with _-> r0;; +let flin_coef f x = try (Constrhash.find f.fhom x) with Not_found -> r0;; let flin_add f x c = let cx = flin_coef f x in @@ -141,10 +141,12 @@ let rec flin_of_constr c = (try (let a=(rational_of_constr args.(0)) in try (let b = (rational_of_constr args.(1)) in (flin_add_cste (flin_zero()) (rmult a b))) - with _-> (flin_add (flin_zero()) + with e when Errors.noncritical e -> + (flin_add (flin_zero()) args.(1) a)) - with _-> (flin_add (flin_zero()) + with e when Errors.noncritical e -> + (flin_add (flin_zero()) args.(0) (rational_of_constr args.(1)))) | "Rinv"-> @@ -154,7 +156,8 @@ let rec flin_of_constr c = (let b=(rational_of_constr args.(1)) in try (let a = (rational_of_constr args.(0)) in (flin_add_cste (flin_zero()) (rdiv a b))) - with _-> (flin_add (flin_zero()) + with e when Errors.noncritical e -> + (flin_add (flin_zero()) args.(0) (rinv b))) |_->assert false) @@ -164,7 +167,8 @@ let rec flin_of_constr c = |"R0" -> flin_zero () |_-> assert false) |_-> assert false) - with _ -> flin_add (flin_zero()) + with e when Errors.noncritical e -> + flin_add (flin_zero()) c r1 ;; @@ -494,13 +498,13 @@ let rec fourier gl= |_->assert false) |_->assert false in tac gl) - with _ -> + with e when Errors.noncritical e -> (* les hypothèses *) let hyps = List.map (fun (h,t)-> (mkVar h,t)) (list_of_sign (pf_hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) - with _ -> ()) + with e when Errors.noncritical e -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) if !lineq=[] then Util.error "No inequalities"; diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 33d77568..48205019 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -33,9 +33,12 @@ let observennl strm = let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v - with e -> - let e = Cerrors.process_vernac_interp_error e in - let goal = begin try (Printer.pr_goal g) with _ -> assert false end in + with reraise -> + let e = Cerrors.process_vernac_interp_error reraise in + let goal = + try (Printer.pr_goal g) + with e when Errors.noncritical e -> assert false + in msgnl (str "observation "++ s++str " raised exception " ++ Errors.print e ++ str " on goal " ++ goal ); raise e;; @@ -119,7 +122,7 @@ let is_trivial_eq t = eq_constr t1 t2 && eq_constr a1 a2 | _ -> false end - with _ -> false + with e when Errors.noncritical e -> false in (* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *) res @@ -145,7 +148,7 @@ let is_incompatible_eq t = (eq_constr u1 u2 && incompatible_constructor_terms t1 t2) | _ -> false - with _ -> false + with e when Errors.noncritical e -> false in if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t); res @@ -232,7 +235,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = then (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0)) else nochange "not an equality" - with _ -> nochange "not an equality" + with e when Errors.noncritical e -> nochange "not an equality" in if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs"; let rec compute_substitution sub t1 t2 = @@ -608,7 +611,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let my_orelse tac1 tac2 g = try tac1 g - with e -> + with e when Errors.noncritical e -> (* observe (str "using snd tac since : " ++ Errors.print e); *) tac2 g @@ -1212,7 +1215,11 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let ctxt,pte_app = (decompose_prod_assum (pf_concl gl)) in let pte,pte_args = (decompose_app pte_app) in try - let pte = try destVar pte with _ -> anomaly "Property is not a variable" in + let pte = + try destVar pte + with e when Errors.noncritical e -> + anomaly "Property is not a variable" + in let fix_info = Idmap.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in tclTHENSEQ diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 00e966fb..04fcc8d4 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -302,11 +302,8 @@ let defined () = "defined" ((try str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl () - with _ -> mt () + with e when Errors.noncritical e -> mt () ) ++msg) - | e -> raise e - - let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) @@ -401,7 +398,7 @@ let generate_functional_principle Don't forget to close the goal if an error is raised !!!! *) save false new_princ_name entry g_kind hook - with e -> + with e when Errors.noncritical e -> begin begin try @@ -413,7 +410,7 @@ let generate_functional_principle then Pfedit.delete_current_proof () else () else () - with _ -> () + with e when Errors.noncritical e -> () end; raise (Defining_principle e) end @@ -554,7 +551,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition 0 (prove_princ_for_struct false 0 (Array.of_list funs)) (fun _ _ _ -> ()) - with e -> + with e when Errors.noncritical e -> begin begin try @@ -566,7 +563,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition then Pfedit.delete_current_proof () else () else () - with _ -> () + with e when Errors.noncritical e -> () end; raise (Defining_principle e) end diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 85d79214..6b6e4838 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -208,14 +208,14 @@ VERNAC COMMAND EXTEND NewFunctionalScheme try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> Util.error ("Cannot generate induction principle(s)") - | e -> + | e when Errors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end | _ -> assert false (* we can only have non empty list *) end - | e -> + | e when Errors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 43b08840..b9e0e62a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -948,7 +948,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue + try Pretyping.Default.understand Evd.empty env t + with e when Errors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in let _keep_eq = @@ -1247,7 +1248,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b l := param::!l ) rels_params.(0) - with _ -> + with e when Errors.noncritical e -> () in List.rev !l @@ -1453,7 +1454,7 @@ let do_build_inductive in observe (msg); raise e - | e -> + | reraise -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = @@ -1464,16 +1465,16 @@ let do_build_inductive str "while trying to define"++ spc () ++ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ - Errors.print e + Errors.print reraise in observe msg; - raise e + raise reraise let build_inductive funnames funsargs returned_types rtl = try do_build_inductive funnames funsargs returned_types rtl - with e -> raise (Building_graph e) + with e when Errors.noncritical e -> raise (Building_graph e) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index cdd0eaf7..6cc932b1 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -534,7 +534,8 @@ let rec are_unifiable_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "are_unifiable_aux" + with e when Errors.noncritical e -> + anomaly "are_unifiable_aux" in are_unifiable_aux eqs' @@ -556,7 +557,8 @@ let rec eq_cases_pattern_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "eq_cases_pattern_aux" + with e when Errors.noncritical e -> + anomaly "eq_cases_pattern_aux" in eq_cases_pattern_aux eqs' | _ -> raise NotUnifiable diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8caeca57..d2c065a0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -82,7 +82,7 @@ let functional_induction with_clean c princl pat = List.fold_right (fun a acc -> try Idset.add (destVar a) acc - with _ -> acc + with e when Errors.noncritical e -> acc ) args Idset.empty @@ -166,8 +166,8 @@ let build_newrecursive sigma rec_sign rec_impls def ) lnameargsardef - with e -> - States.unfreeze fs; raise e in + with reraise -> + States.unfreeze fs; raise reraise in States.unfreeze fs; def in recdef,rec_impls @@ -251,12 +251,12 @@ let derive_inversion fix_names = (fun id -> destInd (Constrintern.global_reference (mk_rel_id id))) fix_names ) - with e -> + with e when Errors.noncritical e -> let e' = Cerrors.process_vernac_interp_error e in msg_warning (str "Cannot build inversion information" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) - with _ -> () + with e when Errors.noncritical e -> () let warning_error names e = let e = Cerrors.process_vernac_interp_error e in @@ -346,7 +346,7 @@ let generate_principle on_error Array.iter (add_Function is_general) funs_kn; () end - with e -> + with e when Errors.noncritical e -> on_error names e let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = @@ -413,7 +413,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); derive_inversion [fname] - with e -> + with e when Errors.noncritical e -> (* No proof done *) () in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index dd475315..827191b1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -55,7 +55,6 @@ let locate_with_msg msg f x = f x with | Not_found -> raise (Util.UserError("", msg)) - | e -> raise e let filter_map filter f = @@ -123,7 +122,7 @@ let def_of_const t = (try (match Declarations.body_of_constant (Global.lookup_constant sp) with | Some c -> Declarations.force c | _ -> assert false) - with _ -> assert false) + with e when Errors.noncritical e -> assert false) |_ -> assert false let coq_constant s = @@ -215,13 +214,13 @@ let with_full_print f a = Dumpglob.continue (); res with - | e -> + | reraise -> Impargs.make_implicit_args old_implicit_args; Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Dumpglob.continue (); - raise e + raise reraise @@ -350,7 +349,8 @@ open Term let pr_info f_info = str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ - (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++ + (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) + with e when Errors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++ str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++ str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++ @@ -502,22 +502,22 @@ exception ToShow of exn let init_constant dir s = try Coqlib.gen_constant "Function" dir s - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) let jmeq () = try (Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; init_constant ["Logic";"JMeq"] "JMeq") - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) let jmeq_rec () = try Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; init_constant ["Logic";"JMeq"] "JMeq_rec" - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; init_constant ["Logic";"JMeq"] "JMeq_refl" - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 55451a9f..7b5dd763 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -59,14 +59,17 @@ let observennl strm = let do_observe_tac s tac g = - let goal = begin try (Printer.pr_goal g) with _ -> assert false end in + let goal = + try Printer.pr_goal g + with e when Errors.noncritical e -> assert false + in try let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v - with e -> - let e' = Cerrors.process_vernac_interp_error e in + with reraise -> + let e' = Cerrors.process_vernac_interp_error reraise in msgnl (str "observation "++ s++str " raised exception " ++ Errors.print e' ++ str " on goal " ++ goal ); - raise e;; + raise reraise;; let observe_tac s tac g = @@ -568,7 +571,7 @@ let rec reflexivity_with_destruct_cases g = observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] | _ -> reflexivity - with _ -> reflexivity + with e when Errors.noncritical e -> reflexivity in let eq_ind = Coqlib.build_coq_eq () in let discr_inject = @@ -862,11 +865,11 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g update_Function {finfo with completeness_lemma = Some lem_cst} ) funs; - with e -> + with reraise -> (* In case of problem, we reset all the lemmas *) Pfedit.delete_all_proofs (); States.unfreeze previous_state; - raise e + raise reraise diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 6ee2f352..bd1a1710 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -70,7 +70,7 @@ let ident_global_exist id = let ans = CRef (Libnames.Ident (dummy_loc,id)) in let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in true - with _ -> false + with e when Errors.noncritical e -> false (** [next_ident_fresh id] returns a fresh identifier (ie not linked in global env) with base [id]. *) @@ -793,10 +793,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let params1 = try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) - with _ -> [] in + with e when Errors.noncritical e -> [] in let params2 = try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) - with _ -> [] in + with e when Errors.noncritical e -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 892c1a77..9853fd73 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -94,11 +94,11 @@ let do_observe_tac s tac g = let v = tac g in ignore(Stack.pop debug_queue); v - with e -> + with reraise -> if not (Stack.is_empty debug_queue) then - print_debug_queue true e; - raise e + print_debug_queue true reraise; + raise reraise let observe_tac s tac g = if Tacinterp.get_debug () <> Tactic_debug.DebugOff @@ -140,7 +140,7 @@ let def_of_const t = (try (match body_of_constant (Global.lookup_constant sp) with | Some c -> Declarations.force c | _ -> assert false) - with _ -> + with e when Errors.noncritical e -> anomaly ("Cannot find definition of constant "^ (string_of_id (id_of_label (con_label sp)))) ) @@ -380,7 +380,11 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool) (fun g1 -> let ty_teq = pf_type_of g1 (mkVar teq) in let teq_lhs,teq_rhs = - let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in + let _,args = + try destApp ty_teq + with e when Errors.noncritical e -> + Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false + in args.(1),args.(2) in cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1 @@ -701,12 +705,17 @@ let proveterminate nb_arg rec_arg_id is_mes acc_inv (hrec:identifier) (match find_call_occs nb_arg 0 f_constr expr with _,[] -> (try observe_tac "base_leaf" (base_leaf func eqs expr) - with e -> (msgerrnl (str "failure in base case");raise e )) + with reraise -> + (msgerrnl (str "failure in base case");raise reraise )) | _, _::_ -> observe_tac "rec_leaf" (rec_leaf is_mes acc_inv hrec func eqs expr)) in v - with e -> begin msgerrnl(str "failure in proveterminate"); raise e end + with reraise -> + begin + msgerrnl(str "failure in proveterminate"); + raise reraise + end in proveterminate @@ -931,7 +940,7 @@ let is_rec_res id = let id_name = string_of_id id in try String.sub id_name 0 (String.length rec_res_name) = rec_res_name - with _ -> false + with e when Errors.noncritical e -> false let clear_goals = let rec clear_goal t = @@ -969,7 +978,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ | Some s -> s | None -> try (add_suffix current_proof_name "_subproof") - with _ -> anomaly "open_new_goal with an unamed theorem" + with e when Errors.noncritical e -> + anomaly "open_new_goal with an unamed theorem" in let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in @@ -1439,7 +1449,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let stop = ref false in begin try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) - with e -> + with e when Errors.noncritical e -> begin if Tacinterp.get_debug () <> Tactic_debug.DebugOff then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e) @@ -1474,9 +1484,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num using_lemmas (List.length res_vars) hook - with e -> + with reraise -> begin - (try ignore (Backtrack.backto previous_label) with _ -> ()); + (try ignore (Backtrack.backto previous_label) + with e when Errors.noncritical e -> ()); (* anomaly "Cannot create termination Lemma" *) - raise e + raise reraise end diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 25579a87..a5b0da9c 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -331,7 +331,7 @@ let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = | Inr _ -> None | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) (* should not use rats_to_ints *) - with x -> + with x when Errors.noncritical x -> if debug then (Printf.printf "raw certificate %s" (Printexc.to_string x); flush stdout) ; @@ -377,8 +377,9 @@ let linear_prover n_spec l = let linear_prover n_spec l = - try linear_prover n_spec l with - x -> (print_string (Printexc.to_string x); None) + try linear_prover n_spec l + with x when x <> Sys.Break -> + (print_string (Printexc.to_string x); None) let linear_prover_with_cert spec l = match linear_prover spec l with diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 2020447f..ff08aeb3 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -937,7 +937,8 @@ struct let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in (power , env) - with _ -> (* if the exponent is a variable *) + with e when e <> Sys.Break -> + (* if the exponent is a variable *) let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) end | Ukn s -> @@ -1112,8 +1113,12 @@ struct let parse_formula parse_atom env tg term = - let parse_atom env tg t = try let (at,env) = parse_atom env t in - (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in + let parse_atom env tg t = + try + let (at,env) = parse_atom env t in + (A(at,tg,t), env,Tag.next tg) + with e when e <> Sys.Break -> (X(t),env,tg) + in let rec xparse_formula env tg term = match kind_of_term term with @@ -1189,7 +1194,8 @@ let same_proof sg cl1 cl2 = let rec xsame_proof sg = match sg with | [] -> true - | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false) + | n::sg -> + (try List.nth cl1 n = List.nth cl2 n with e when e <> Sys.Break -> false) && (xsame_proof sg ) in xsame_proof sg @@ -1253,7 +1259,7 @@ let btree_of_array typ a = let btree_of_array typ a = try btree_of_array typ a - with x -> + with x when x <> Sys.Break -> failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x)) let dump_varmap typ env = @@ -1322,7 +1328,7 @@ let rec parse_hyps parse_arith env tg hyps = try let (c,env,tg) = parse_formula parse_arith env tg t in ((i,c)::lhyps, env,tg) - with _ -> (lhyps,env,tg) + with e when e <> Sys.Break -> (lhyps,env,tg) (*(if debug then Printf.printf "parse_arith : %s\n" x);*) @@ -1466,7 +1472,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = (pp_ml_list prover.pp_f) (List.map fst new_cl) ; flush stdout end ; *) - let res = try prover.compact prf remap with x -> + let res = try prover.compact prf remap with x when x <> Sys.Break -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) match prover.prover (List.map fst new_cl) with @@ -2031,13 +2037,13 @@ let xlia gl = try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_Z ] gl - with z -> (*Printexc.print_backtrace stdout ;*) raise z + with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let xnlia gl = try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ nlinear_Z ] gl - with z -> (*Printexc.print_backtrace stdout ;*) raise z + with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index dfda5984..0f26575c 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -150,7 +150,7 @@ let real_nonlinear_prover d l = S (Some proof) with | Sos_lib.TooDeep -> S None - | x -> F (Printexc.to_string x) + | x when x <> Sys.Break -> F (Printexc.to_string x) (* This is somewhat buggy, over Z, strict inequality vanish... *) let pure_sos l = @@ -174,7 +174,7 @@ let pure_sos l = S (Some proof) with (* | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *) - | x -> (* May be that could be refined *) S None + | x when x <> Sys.Break -> (* May be that could be refined *) S None @@ -203,7 +203,7 @@ let main () = Marshal.to_channel chan (cert:csdp_certificate) [] ; flush chan ; exit 0 - with x -> (Printf.fprintf chan "error %s" (Printexc.to_string x) ; exit 1) + with any -> (Printf.fprintf chan "error %s" (Printexc.to_string any) ; exit 1) ;; diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index d9201722..6effa4c4 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -728,7 +728,8 @@ struct try Some (bound_of_variable IMap.empty fresh s.sys) with - x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None + x when x <> Sys.Break -> + Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None let find_point cstrs = diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index ccbf0406..3129e54d 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -29,10 +29,10 @@ let finally f rst = try let res = f () in rst () ; res - with x -> + with reraise -> (try rst () - with _ -> raise x - ); raise x + with any -> raise reraise + ); raise reraise let map_option f x = match x with @@ -431,14 +431,16 @@ let command exe_path args vl = | Unix.WEXITED 0 -> let inch = Unix.in_channel_of_descr stdout_read in begin try Marshal.from_channel inch - with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) + with x when x <> Sys.Break -> + failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) end | Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) | Unix.WSTOPPED i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) (* Cleanup *) (fun () -> - List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write]) + List.iter (fun x -> try Unix.close x with e when e <> Sys.Break -> ()) + [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write]) (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index cb7a9280..6d1a2927 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -82,10 +82,10 @@ let finally f rst = try let res = f () in rst () ; res - with x -> + with reraise -> (try rst () - with _ -> raise x - ); raise x + with any -> raise reraise + ); raise reraise let read_key_elem inch = @@ -93,7 +93,7 @@ let read_key_elem inch = Some (Marshal.from_channel inch) with | End_of_file -> None - | _ -> raise InvalidTableFormat + | e when e <> Sys.Break -> raise InvalidTableFormat (** In win32, it seems that we should unlock the exact zone that has been locked, and not the whole file *) @@ -151,7 +151,7 @@ let open_in f = Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl; flush outch ; - with _ -> () ) + with e when e <> Sys.Break -> () ) ; unlock out ; { outch = outch ; diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 996dbadd..68fb2626 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -237,7 +237,8 @@ open Format let getvar lv i = try (nth lv i) - with _ -> (fold_left (fun r x -> r^" "^x) "lv= " lv) + with e when Errors.noncritical e -> + (fold_left (fun r x -> r^" "^x) "lv= " lv) ^" i="^(string_of_int i) let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef @@ -590,7 +591,7 @@ let coefpoldep = Hashtbl.create 51 (* coef of q in p = sum_i c_i*q_i *) let coefpoldep_find p q = try (Hashtbl.find coefpoldep (p.num,q.num)) - with _ -> [] + with Not_found -> [] let coefpoldep_remove p q = Hashtbl.remove coefpoldep (p.num,q.num) diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 0eea961d..fdc8e865 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -173,7 +173,7 @@ let rec equal p q = then failwith "raté") p1; true) - with _ -> false) + with e when Errors.noncritical e -> false) | (_,_) -> false (* normalize polynomial: remove head zeros, coefficients are normalized @@ -524,7 +524,7 @@ let div_pol_rat p q= q x in (* degueulasse, mais c 'est pour enlever un warning *) if s==s then true else true) - with _ -> false + with e when Errors.noncritical e -> false (*********************************************************************** 5. Pseudo-division and gcd with subresultants. diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index c16bd425..17c8654b 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -33,10 +33,11 @@ let set_of_list_eq eq l = let memos s memoire nf f x = try (let v = Hashtbl.find memoire (nf x) in pr s;v) - with _ -> (pr "#"; - let v = f x in - Hashtbl.add memoire (nf x) v; - v) + with e when Errors.noncritical e -> + (pr "#"; + let v = f x in + Hashtbl.add memoire (nf x) v; + v) (********************************************************************** @@ -64,7 +65,7 @@ let facteurs_liste div constant lp = if not (constant r) then l1:=r::(!l1) else p_dans_lmin:=true) - with _ -> ()) + with e when Errors.noncritical e -> ()) lmin; if !p_dans_lmin then factor lmin lp1 @@ -75,7 +76,8 @@ let facteurs_liste div constant lp = List.iter (fun q -> try (let r = div q p in if not (constant r) then l1:=r::(!l1)) - with _ -> lmin1:=q::(!lmin1)) + with e when Errors.noncritical e -> + lmin1:=q::(!lmin1)) lmin; factor (List.rev (p::(!lmin1))) !l1) (* au moins un q de lmin divise p non trivialement *) @@ -105,7 +107,7 @@ let factorise_tableau div zero c f l1 = li:=j::(!li); r:=rr; done) - with _ -> ()) + with e when Errors.noncritical e -> ()) l1; res.(i)<-(!r,!li)) f; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 028ef95d..ffa99fc7 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -885,7 +885,7 @@ let rec transform p t = try let v,th,_ = find_constr t' in [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - with _ -> + with e when Errors.noncritical e -> let v = new_identifier_var () and th = new_identifier () in hide_constr t' v th isnat; @@ -924,7 +924,8 @@ let rec transform p t = | _ -> default false t end | Kapp((Zpos|Zneg|Z0),_) -> - (try ([],Oz(recognize_number t)) with _ -> default false t) + (try ([],Oz(recognize_number t)) + with e when Errors.noncritical e -> default false t) | Kvar s -> [],Oatom s | Kapp(Zopp,[t]) -> let tac,t' = transform (P_APP 1 :: p) t in diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index f0ca3bb9..216a719d 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -221,7 +221,10 @@ let compute_rhs bodyi index_of_f = (*s Now the function [compute_ivs] itself *) let compute_ivs gl f cs = - let cst = try destConst f with _ -> i_can't_do_that () in + let cst = + try destConst f + with e when Errors.noncritical e -> i_can't_do_that () + in let body = Environ.constant_value (Global.env()) cst in match decomp_term body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index ae73069d..7b0d96bb 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -292,7 +292,8 @@ let unbox = function (* Protects the convertibility test against undue exceptions when using it with untyped terms *) -let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false +let safe_pf_conv_x gl c1 c2 = + try pf_conv_x gl c1 c2 with e when Errors.noncritical e -> false (* Add a Ring or a Semi-Ring to the database after a type verification *) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index e810e15c..fb45e816 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -335,7 +335,7 @@ let parse_term t = | Kapp("Z.succ",[t]) -> Tsucc t | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (try Tnum (recognize t) with _ -> Tother) + (try Tnum (recognize t) with e when Errors.noncritical e -> Tother) | _ -> Tother with e when Logic.catchable_exception e -> Tother @@ -357,6 +357,6 @@ let is_scalar t = | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true | _ -> false in - try aux t with _ -> false + try aux t with e when Errors.noncritical e -> false end diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 4a6d462e..e57230cb 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -225,7 +225,8 @@ let add_reified_atom t env = env.terms <- env.terms @ [t]; i let get_reified_atom env = - try List.nth env.terms with _ -> failwith "get_reified_atom" + try List.nth env.terms + with e when Errors.noncritical e -> failwith "get_reified_atom" (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) @@ -235,7 +236,9 @@ let add_prop env t = let i = List.length env.props in env.props <- env.props @ [t]; i (* accès a une proposition *) -let get_prop v env = try List.nth v env with _ -> failwith "get_prop" +let get_prop v env = + try List.nth v env + with e when Errors.noncritical e -> failwith "get_prop" (* \subsection{Gestion du nommage des équations} *) (* Ajout d'une equation dans l'environnement de reification *) @@ -247,7 +250,8 @@ let add_equation env e = (* accès a une equation *) let get_equation env id = try Hashtbl.find env.equations id - with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e + with Not_found as e -> + Printf.printf "Omega Equation %d non trouvée\n" id; raise e (* Affichage des termes réifiés *) let rec oprint ch = function @@ -349,7 +353,8 @@ let rec reified_of_formula env = function app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |] let reified_of_formula env f = - begin try reified_of_formula env f with e -> oprint stderr f; raise e end + try reified_of_formula env f + with reraise -> oprint stderr f; raise reraise let rec reified_of_proposition env = function Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) -> @@ -380,8 +385,8 @@ let rec reified_of_proposition env = function | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |] let reified_of_proposition env f = - begin try reified_of_proposition env f - with e -> pprint stderr f; raise e end + try reified_of_proposition env f + with reraise -> pprint stderr f; raise reraise (* \subsection{Omega vers COQ réifié} *) @@ -397,11 +402,11 @@ let reified_of_omega env body constant = List.fold_right mk_coeff body coeff_constant let reified_of_omega env body c = - begin try + try reified_of_omega env body c - with e -> - display_eq display_omega_var (body,c); raise e - end + with reraise -> + display_eq display_omega_var (body,c); raise reraise + (* \section{Opérations sur les équations} Ces fonctions préparent les traces utilisées par la tactique réfléchie @@ -1000,10 +1005,11 @@ let rec solve_with_constraints all_solutions path = let weighted = filter_compatible_systems path all_solutions in let (winner_sol,winner_deps) = try select_smaller weighted - with e -> + with reraise -> Printf.printf "%d - %d\n" (List.length weighted) (List.length all_solutions); - List.iter display_depend path; raise e in + List.iter display_depend path; raise reraise + in build_tree winner_sol (List.rev path) winner_deps let find_path {o_hyp=id;o_path=p} env = diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 956ccf09..6e7a8d32 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -90,7 +90,8 @@ VERNAC COMMAND EXTEND Subtac let try_catch_exn f e = try f e - with exn -> errorlabstrm "Program" (Errors.print exn) + with exn when Errors.noncritical exn -> + errorlabstrm "Program" (Errors.print exn) let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 281e981b..ad248bfb 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -221,6 +221,6 @@ let subtac (loc, command) = | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | Loc.Exc_located (loc, e') as e) -> raise e - | e -> + | reraise -> (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *) - raise e + raise reraise diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 221b57ee..0b1ed9bb 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -342,7 +342,7 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c = let pred = predicate 0 c in let env' = push_rel_context (context_of_arsign arsign) env in ignore(Typing.sort_of env' evm pred); pred - with _ -> lift nar c + with e when Errors.noncritical e -> lift nar c module Cases_F(Coercion : Coercion.S) : S = struct @@ -1465,7 +1465,8 @@ let extract_arity_signatures env0 tomatchl tmsign = | None -> list_tabulate (fun _ -> Anonymous) nrealargs in let arsign = fst (get_arity env0 indf) in (na,None,build_dependent_inductive env0 indf) - ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in + ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign + with e when Errors.noncritical e -> assert false) in let rec buildrec = function | [],[] -> [] | (_,tm)::ltm, x::tmsign -> diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 168a799d..0c03fb4c 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -356,7 +356,7 @@ module Coercion = struct jres), jres.uj_type) (hj,typ_cl) p) - with _ -> anomaly "apply_coercion" + with e when Errors.noncritical e -> anomaly "apply_coercion" let inh_app_fun env isevars j = let isevars = ref isevars in @@ -506,5 +506,5 @@ module Coercion = struct with NoSubtacCoercion -> error_cannot_coerce env' isevars (t, t')) else isevars - with _ -> isevars + with e when Errors.noncritical e -> isevars end diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 14a09032..537a8301 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -248,7 +248,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = | [(_, None, t); (_, None, u)], Sort (Prop Null) when Reductionops.is_conv env !isevars t u -> t | _, _ -> error () - with _ -> error () + with e when Errors.noncritical e -> error () in let measure = interp_casted_constr isevars binders_env measure relargty in let wf_rel, wf_rel_fun, measure_fn = @@ -440,7 +440,7 @@ let interp_recursive fixkind l = let sort = Retyping.get_type_of env !evdref t in let fixprot = try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|]) - with e -> t + with e when Errors.noncritical e -> t in (id,None,fixprot) :: env') [] fixnames fixtypes diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index dfcc8526..d8f46098 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -121,7 +121,7 @@ let obl_substitution expand obls deps = let xobl = obls.(x) in let oblb = try get_obligation_body expand xobl - with _ -> assert(false) + with e when Errors.noncritical e -> assert(false) in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) deps [] @@ -498,7 +498,8 @@ let rec solve_obligation prg num tac = let obls = Array.copy obls in let _ = obls.(num) <- obl in let res = try update_obls prg obls (pred rem) - with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e)) + with e when Errors.noncritical e -> + pperror (Errors.print (Cerrors.process_vernac_interp_error e)) in match res with | Remain n when n > 0 -> @@ -552,7 +553,7 @@ and solve_obligation_by_tac prg obls i tac = | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) | Util.Anomaly _ as e -> raise e - | e -> false + | e when Errors.noncritical e -> false and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 95e756ab..f0579711 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -302,7 +302,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix with e -> Loc.raise loc e); + (try check_cofix env cofix + with e when Errors.noncritical e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon @@ -601,7 +602,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct ~split:true ~fail:true env !evdref; evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref - with e -> if fail_evar then raise e else ()); + with e when Errors.noncritical e -> + if fail_evar then raise e else ()); evdref := consider_remaining_unif_problems env !evdref; let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index fbb44811..e32bb9e0 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -232,7 +232,7 @@ let build_dependent_sum l = let hyptype = substl names t in trace (spc () ++ str ("treating evar " ^ string_of_id n)); (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype) - with _ -> ()); + with e when Errors.noncritical e -> ()); let tac = assert_tac (Name n) hyptype in let conttac = (fun cont -> @@ -331,7 +331,7 @@ let destruct_ex ext ex = Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 -> let (dom, rng) = try (args.(0), args.(1)) - with _ -> assert(false) + with e when Errors.noncritical e -> assert(false) in let pi1 = (mk_ex_pi1 dom rng acc) in let rng_body = @@ -375,9 +375,9 @@ let solve_by_tac evi t = Inductiveops.control_only_guard (Global.env ()) const.Entries.const_entry_body; const.Entries.const_entry_body - with e -> + with reraise -> Pfedit.delete_current_proof(); - raise e + raise reraise (* let apply_tac t goal = t goal *) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index da0a65ff..a14eda60 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -349,7 +349,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids if computeinnertypes then try Acic.CicHash.find terms_to_types tt -with _ -> +with e when e <> Sys.Break -> (*CSC: Warning: it really happens, for example in Ring_theory!!! *) Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false else diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index a21a919a..c22c16f0 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -147,7 +147,8 @@ let double_type_of env sigma cstr expectedty subterms_to_types = (*CSC: universes. *) (try Typeops.judge_of_type u - with _ -> (* Successor of a non universe-variable universe anomaly *) + with e when e <> Sys.Break -> + (* Successor of a non universe-variable universe anomaly *) (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ; Typeops.judge_of_type (Termops.new_univ ()) ) diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 1037bbf0..867aac71 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -143,7 +143,7 @@ let rec join_dirs cwd = | he::tail -> (try Unix.mkdir cwd 0o775 - with _ -> () (* Let's ignore the errors on mkdir *) + with e when e <> Sys.Break -> () (* Let's ignore the errors on mkdir *) ) ; let newcwd = cwd ^ "/" ^ he in join_dirs newcwd tail |