From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- CHANGES | 29 ++++++++++++ checker/check.ml | 6 +-- checker/checker.ml | 3 +- checker/mod_checking.ml | 7 ++- configure | 2 +- dev/base_include | 4 +- dev/top_printers.ml | 6 +-- ide/coqide.ml | 7 ++- ide/coqide_main.ml4 | 52 +++++++++------------ ide/gtk_parsing.ml | 1 + ide/ide_win32_stubs.c | 44 ++++++++--------- interp/constrextern.ml | 33 +++++++------ interp/constrextern.mli | 9 ++-- interp/constrintern.ml | 14 +++--- interp/implicit_quantifiers.ml | 4 +- interp/notation.ml | 2 +- kernel/csymtable.ml | 4 +- kernel/mod_subst.ml | 25 ++++++---- kernel/modops.ml | 2 +- kernel/modops.mli | 3 +- kernel/names.ml | 10 ++-- kernel/pre_env.ml | 2 +- kernel/safe_typing.ml | 5 +- kernel/subtyping.ml | 12 +++-- lib/envars.ml | 19 ++++---- lib/errors.ml | 13 +++++- lib/errors.mli | 8 ++++ lib/flags.ml | 4 +- lib/hashtbl_alt.ml | 2 +- lib/pp.ml4 | 2 +- lib/profile.ml | 30 ++++++------ lib/store.ml | 2 +- lib/system.ml | 24 ++++++---- lib/system.mli | 2 +- lib/xml_parser.ml | 6 +-- library/declaremods.ml | 4 +- library/heads.ml | 2 +- library/impargs.ml | 4 +- library/library.ml | 17 +++---- myocamlbuild.ml | 15 +++--- parsing/argextend.ml4 | 2 +- parsing/egrammar.ml | 2 +- parsing/g_tactic.ml4 | 2 +- parsing/g_xml.ml4 | 3 +- parsing/prettyp.ml | 8 ++-- parsing/printer.ml | 65 ++++++++++++++++++++++++-- parsing/printer.mli | 11 +++++ parsing/printmod.ml | 59 +++++++++++++++-------- parsing/tacextend.ml4 | 4 +- parsing/vernacextend.ml4 | 4 +- plugins/cc/ccalgo.ml | 7 ++- plugins/cc/cctac.ml | 4 +- plugins/decl_mode/decl_mode.ml | 4 +- plugins/decl_mode/decl_proof_instr.ml | 9 ++-- plugins/extraction/extract_env.ml | 18 ++++--- plugins/extraction/extraction.ml | 4 +- plugins/extraction/haskell.ml | 4 +- plugins/extraction/mlutil.ml | 4 +- plugins/extraction/ocaml.ml | 5 +- plugins/extraction/table.ml | 6 +-- plugins/firstorder/g_ground.ml4 | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/fourier/fourier.ml | 2 +- plugins/fourier/fourierR.ml | 18 ++++--- plugins/funind/functional_principles_proofs.ml | 23 +++++---- plugins/funind/functional_principles_types.ml | 13 ++---- plugins/funind/g_indfun.ml4 | 4 +- plugins/funind/glob_term_to_relation.ml | 13 +++--- plugins/funind/glob_termops.ml | 6 ++- plugins/funind/indfun.ml | 14 +++--- plugins/funind/indfun_common.ml | 18 +++---- plugins/funind/invfun.ml | 17 ++++--- plugins/funind/merge.ml | 6 +-- plugins/funind/recdef.ml | 37 +++++++++------ plugins/micromega/certificate.ml | 7 +-- plugins/micromega/coq_micromega.ml | 24 ++++++---- plugins/micromega/csdpcert.ml | 6 +-- plugins/micromega/mfourier.ml | 3 +- plugins/micromega/mutils.ml | 12 +++-- plugins/micromega/persistent_cache.ml | 10 ++-- plugins/nsatz/ideal.ml | 5 +- plugins/nsatz/polynom.ml | 4 +- plugins/nsatz/utile.ml | 16 ++++--- plugins/omega/coq_omega.ml | 5 +- plugins/quote/quote.ml | 5 +- plugins/ring/ring.ml | 3 +- plugins/romega/const_omega.ml | 4 +- plugins/romega/refl_omega.ml | 30 +++++++----- plugins/subtac/g_subtac.ml4 | 3 +- plugins/subtac/subtac.ml | 4 +- plugins/subtac/subtac_cases.ml | 5 +- plugins/subtac/subtac_coercion.ml | 4 +- plugins/subtac/subtac_command.ml | 4 +- plugins/subtac/subtac_obligations.ml | 7 +-- plugins/subtac/subtac_pretyping_F.ml | 6 ++- plugins/subtac/subtac_utils.ml | 8 ++-- plugins/xml/cic2acic.ml | 2 +- plugins/xml/doubleTypeInference.ml | 3 +- plugins/xml/xmlcommand.ml | 2 +- pretyping/coercion.ml | 2 +- pretyping/detyping.ml | 6 +-- pretyping/evarconv.ml | 8 ++-- pretyping/evarutil.ml | 27 +++++++---- pretyping/evarutil.mli | 1 + pretyping/evd.ml | 5 +- pretyping/evd.mli | 1 + pretyping/inductiveops.ml | 1 + pretyping/pretyping.ml | 11 +++-- pretyping/recordops.ml | 8 ++-- pretyping/reductionops.ml | 10 +++- pretyping/retyping.ml | 12 ++--- pretyping/tacred.ml | 10 ++-- pretyping/typeclasses.ml | 10 ++-- pretyping/unification.ml | 13 ++++-- pretyping/vnorm.ml | 24 +++++++--- proofs/evar_refiner.ml | 2 +- proofs/goal.ml | 16 +++++-- proofs/goal.mli | 2 +- proofs/logic.ml | 2 +- proofs/pfedit.ml | 6 +-- proofs/proof.ml | 10 ++-- proofs/proofview.ml | 10 ++-- proofs/refiner.ml | 8 ++-- proofs/tactic_debug.ml | 8 ++-- scripts/coqmktop.ml | 13 +++--- tactics/auto.ml | 11 +++-- tactics/autorewrite.ml | 12 +++-- tactics/class_tactics.ml4 | 7 ++- tactics/eauto.ml4 | 3 +- tactics/equality.ml | 5 +- tactics/extratactics.ml4 | 2 +- tactics/hipattern.ml4 | 10 +++- tactics/inv.ml | 4 +- tactics/rewrite.ml4 | 25 ++++++---- tactics/tacinterp.ml | 64 +++++++++++++------------ tactics/tactics.ml | 15 ++++-- test-suite/bugs/closed/2955.v | 52 +++++++++++++++++++++ test-suite/bugs/closed/shouldsucceed/2629.v | 22 +++++++++ test-suite/bugs/closed/shouldsucceed/2668.v | 6 +++ test-suite/bugs/closed/shouldsucceed/2734.v | 15 ++++++ test-suite/bugs/closed/shouldsucceed/2750.v | 23 +++++++++ test-suite/bugs/closed/shouldsucceed/2928.v | 11 +++++ test-suite/bugs/closed/shouldsucceed/2983.v | 8 ++++ test-suite/bugs/closed/shouldsucceed/2995.v | 9 ++++ test-suite/bugs/closed/shouldsucceed/3000.v | 2 + test-suite/bugs/closed/shouldsucceed/3004.v | 7 +++ test-suite/bugs/closed/shouldsucceed/3008.v | 29 ++++++++++++ test-suite/output/inference.out | 4 ++ test-suite/output/inference.v | 12 +++++ test-suite/success/remember.v | 8 ++++ theories/Numbers/NatInt/NZOrder.v | 2 +- toplevel/auto_ind_decl.ml | 44 +++++++++-------- toplevel/autoinstance.ml | 3 +- toplevel/backtrack.ml | 4 +- toplevel/classes.ml | 11 +++-- toplevel/coqinit.ml | 4 +- toplevel/coqtop.ml | 9 ++-- toplevel/himsg.ml | 11 +++-- toplevel/ide_intf.ml | 6 +-- toplevel/ide_slave.ml | 11 +++-- toplevel/ind_tables.ml | 5 +- toplevel/indschemes.ml | 7 +-- toplevel/lemmas.ml | 27 +++++++---- toplevel/metasyntax.ml | 13 ++++-- toplevel/mltop.ml4 | 11 +++-- toplevel/search.ml | 2 +- toplevel/toplevel.ml | 12 ++--- toplevel/vernac.ml | 24 +++++----- toplevel/vernacentries.ml | 13 ++++-- toplevel/vernacinterp.ml | 4 +- 170 files changed, 1205 insertions(+), 632 deletions(-) create mode 100644 test-suite/bugs/closed/2955.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2629.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2668.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2734.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2750.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2928.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2983.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2995.v create mode 100644 test-suite/bugs/closed/shouldsucceed/3000.v create mode 100644 test-suite/bugs/closed/shouldsucceed/3004.v create mode 100644 test-suite/bugs/closed/shouldsucceed/3008.v diff --git a/CHANGES b/CHANGES index fa0cca0c..a696ad71 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,30 @@ +Changes from V8.4pl1 to V8.4pl2 +=============================== + +Bug fixes + +- Solved bugs : + #2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967 + #2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008 +- Partially fixed bugs : #2830 #2949 +- Coqtop should now react more reliably when receiving interrupt signals: + all the "try...with" constructs have been protected against undue + handling of the Sys.Break exception. + +Coqide + +- The Windows-specific code handling the interrupt button of Coqide + had to be reworked (cf. bug #2869). Now, in Win32 this button does + not target a specific coqtop client, but instead sends a Ctrl-C to + any process sharing its console with Coqide. To avoid awkward + effects, it is recommended to launch Coqide via its icon, its menu, + or in a dedicated console window. + +Extraction + +- The option Extraction AccessOpaque is now set by default, + restoring compatibility of older versions of Coq (cf bug #2952). + Changes from V8.4 to V8.4pl1 ============================ @@ -2438,3 +2465,5 @@ New user contributions - Correctness proof of Stalmarck tautology checker algorithm [Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis) + + LocalWords: recommended diff --git a/checker/check.ml b/checker/check.ml index 237eb079..fb0dc12a 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -290,9 +290,9 @@ let intern_from_file (dir, f) = let (md,table,digest) = try let ch = with_magic_number_check raw_intern_library f in - let (md:library_disk) = System.marshal_in ch in - let digest = System.marshal_in ch in - let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in + let (md:library_disk) = System.marshal_in f ch in + let digest = System.marshal_in f ch in + let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in close_in ch; if dir <> md.md_name then errorlabstrm "load_physical_library" diff --git a/checker/checker.ml b/checker/checker.ml index 945abde4..e5e20b1a 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -371,7 +371,8 @@ let run () = compile_files (); flush_all() with e -> - (Pp.ppnl(explain_exn e); + (flush_all(); + Pp.ppnl(explain_exn e); flush_all(); exit 1) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index e3431fec..dc3ed452 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -133,6 +133,11 @@ let lookup_modtype mp env = with Not_found -> failwith ("Unknown module type: "^string_of_mp mp) +let lookup_module mp env = + try Environ.lookup_module mp env + with Not_found -> + failwith ("Unknown module: "^string_of_mp mp) + let rec check_with env mtb with_decl mp= match with_decl with | With_definition_body (idl,c) -> @@ -199,7 +204,7 @@ and check_with_mod env mtb (idl,mp1) mp = SFBmodule msb -> msb | _ -> error_not_a_module l in - let (_:module_body) = (lookup_module mp1 env) in () + let (_:module_body) = (Environ.lookup_module mp1 env) in () else let old = match spec with SFBmodule msb -> msb diff --git a/configure b/configure index 589cba6e..f7bdf154 100755 --- a/configure +++ b/configure @@ -6,7 +6,7 @@ # ################################## -VERSION=8.4pl1 +VERSION=8.4pl2 VOMAGIC=08400 STATEMAGIC=58400 DATE=`LC_ALL=C LANG=C date +"%B %Y"` diff --git a/dev/base_include b/dev/base_include index ad2a3aec..9a788b7b 100644 --- a/dev/base_include +++ b/dev/base_include @@ -200,8 +200,8 @@ let pf_e gl s = (* Set usual printing since the global env is available from the tracer *) let _ = Constrextern.in_debugger := false -let _ = Constrextern.set_debug_global_reference_printer - (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; +let _ = Constrextern.set_extern_reference + (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; open Toplevel let go = loop diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0038e78a..c55c4377 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -459,7 +459,7 @@ let encode_path loc prefix mpdir suffix id = Qualid (loc, make_qualid (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id) -let raw_string_of_ref loc = function +let raw_string_of_ref loc _ = function | ConstRef cst -> let (mp,dir,id) = repr_con cst in encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id) @@ -475,7 +475,7 @@ let raw_string_of_ref loc = function | VarRef id -> encode_path loc "SECVAR" None [] id -let short_string_of_ref loc = function +let short_string_of_ref loc _ = function | VarRef id -> Ident (loc,id) | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst))) | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn))) @@ -491,5 +491,5 @@ let short_string_of_ref loc = function pretty-printer should not make calls to the global env since ocamldebug runs in a different process and does not have the proper env at hand *) let _ = Constrextern.in_debugger := true -let _ = Constrextern.set_debug_global_reference_printer +let _ = Constrextern.set_extern_reference (if !rawdebug then raw_string_of_ref else short_string_of_ref) diff --git a/ide/coqide.ml b/ide/coqide.ml index 07de4daf..94be8318 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -212,6 +212,9 @@ let ignore_break () = try Sys.set_signal i (Sys.Signal_handle crash_save) with _ -> prerr_endline "Signal ignored (normal if Win32)") signals_to_crash; + (* We ignore the Ctrl-C, this is required for the Stop button to work, + since we will actually send Ctrl-C to all processes sharing + our console (including us) *) Sys.set_signal Sys.sigint Sys.Signal_ignore @@ -902,7 +905,7 @@ object(self) if stop#compare start > 0 && is_sentence_end stop#backward_char then Some (start,stop) else None - with Not_found -> None + with StartError -> None method complete_at_offset (offset:int) = prerr_endline ("Completion at offset : " ^ string_of_int offset); @@ -2449,7 +2452,7 @@ let main files = try configure ~apply:update_notebook_pos () with _ -> flash_info "Cannot save preferences" end; - reset_revert_timer ()) ~accel:"," ~stock:`PREFERENCES; + reset_revert_timer ()) ~accel:"comma" ~stock:`PREFERENCES; (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ]; GAction.add_actions view_actions [ GAction.add_action "View" ~label:"_View"; diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index ebcecc17..aaede465 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -38,6 +38,11 @@ let catch_gtk_messages () = let () = catch_gtk_messages () +(* We anticipate a bit the argument parsing and look for -debug *) + +let early_set_debug () = + Ideutils.debug := List.mem "-debug" (Array.to_list Sys.argv) + (* On win32, we add the directory of coqide to the PATH at launch-time (this used to be done in a .bat script). *) @@ -46,47 +51,32 @@ let set_win32_path () = (Filename.dirname Sys.executable_name ^ ";" ^ (try Sys.getenv "PATH" with _ -> "")) -(* On win32, since coqide is now console-free, we re-route stdout/stderr - to avoid Sys_error if someone writes to them. We write to a pipe which - is never read (by default) or to a temp log file (when in debug mode). -*) - -let reroute_stdout_stderr () = - (* We anticipate a bit the argument parsing and look for -debug *) - let debug = List.mem "-debug" (Array.to_list Sys.argv) in - Ideutils.debug := debug; - let out_descr = - if debug then - let (name,chan) = Filename.open_temp_file "coqide_" ".log" in - Coqide.logfile := Some name; - Unix.descr_of_out_channel chan - else - snd (Unix.pipe ()) - in +(* On win32, in debug mode we duplicate stdout/stderr in a log file. *) + +let log_stdout_stderr () = + let (name,chan) = Filename.open_temp_file "coqide_" ".log" in + Coqide.logfile := Some name; + let out_descr = Unix.descr_of_out_channel chan in Unix.set_close_on_exec out_descr; Unix.dup2 out_descr Unix.stdout; Unix.dup2 out_descr Unix.stderr (* We also provide specific kill and interrupt functions. *) -(* Since [win32_interrupt] involves some hack about the process console, - only one should run at the same time, we simply skip execution of - [win32_interrupt] if another instance is already running *) - -let ctrl_c_mtx = Mutex.create () - -let ctrl_c_protect f i = - if not (Mutex.try_lock ctrl_c_mtx) then () - else try f i; Mutex.unlock ctrl_c_mtx with _ -> Mutex.unlock ctrl_c_mtx - IFDEF WIN32 THEN external win32_kill : int -> unit = "win32_kill" -external win32_interrupt : int -> unit = "win32_interrupt" +external win32_interrupt_all : unit -> unit = "win32_interrupt_all" +external win32_hide_console : unit -> unit = "win32_hide_console" + let () = - Coq.killer := win32_kill; - Coq.interrupter := ctrl_c_protect win32_interrupt; set_win32_path (); - reroute_stdout_stderr () + Coq.killer := win32_kill; + Coq.interrupter := (fun pid -> win32_interrupt_all ()); + early_set_debug (); + if !Ideutils.debug then + log_stdout_stderr () + else + win32_hide_console () END IFDEF QUARTZ THEN diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index 67f7e649..47096e6f 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ideutils let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0) let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0) diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c index c09bf37d..c170b1a9 100644 --- a/ide/ide_win32_stubs.c +++ b/ide/ide_win32_stubs.c @@ -19,31 +19,33 @@ CAMLprim value win32_kill(value pseudopid) { CAMLreturn(Val_unit); } - /* Win32 emulation of a kill -2 (SIGINT) */ -/* This code rely of the fact that coqide is now without initial console. - Otherwise, no console creation in win32unix/createprocess.c, hence - the same console for coqide and all coqtop, and everybody will be - signaled at the same time by the code below. */ +/* For simplicity, we signal all processes sharing a console with coqide. + This shouldn't be an issue since currently at most one coqtop is busy + at a given time. Earlier, we tried to be more precise via + FreeConsole and AttachConsole before generating the Ctrl-C, but + that wasn't working so well (see #2869). + This code rely now on the fact that coqide is a console app, + and that coqide itself ignores Ctrl-C. +*/ + +CAMLprim value win32_interrupt_all(value unit) { + CAMLparam1(unit); + GenerateConsoleCtrlEvent(CTRL_C_EVENT,0); + CAMLreturn(Val_unit); +} -/* Moreover, AttachConsole exists only since WinXP, and GetProcessId - since WinXP SP1. For avoiding the GetProcessId, we could adapt code - from win32unix/createprocess.c to make it return both the pid and the - handle. For avoiding the AttachConsole, I don't know, maybe having - an intermediate process between coqide and coqtop ? */ +/* Get rid of the nasty console window (only if we created it) */ -CAMLprim value win32_interrupt(value pseudopid) { - CAMLparam1(pseudopid); - HANDLE h; +CAMLprim value win32_hide_console (value unit) { + CAMLparam1(unit); DWORD pid; - FreeConsole(); /* Normally unnecessary, just to be sure... */ - h = (HANDLE)(Long_val(pseudopid)); - pid = GetProcessId(h); - AttachConsole(pid); - /* We want to survive the Ctrl-C that will also concerns us */ - SetConsoleCtrlHandler(NULL,TRUE); /* NULL + TRUE means ignore */ - GenerateConsoleCtrlEvent(CTRL_C_EVENT,0); /* signal our co-console */ - FreeConsole(); + HWND hw = GetConsoleWindow(); + if (hw != NULL) { + GetWindowThreadProcessId(hw, &pid); + if (pid == GetCurrentProcessId()) + ShowWindow(hw, SW_HIDE); + } CAMLreturn(Val_unit); } diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 20b9c2a3..ee529fe0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -137,20 +137,21 @@ let insert_pat_alias loc p = function let extern_evar loc n l = if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None) -let debug_global_reference_printer = - ref (fun _ -> failwith "Cannot print a global reference") +(** We allow customization of the global_reference printer. + For instance, in the debugger the tables of global references + may be inaccurate *) -let in_debugger = ref false +let default_extern_reference loc vars r = + Qualid (loc,shortest_qualid_of_global vars r) -let set_debug_global_reference_printer f = - debug_global_reference_printer := f +let my_extern_reference = ref default_extern_reference -let extern_reference loc vars r = - if !in_debugger then - (* Debugger does not have the tables of global reference at hand *) - !debug_global_reference_printer loc r - else - Qualid (loc,shortest_qualid_of_global vars r) +let set_extern_reference f = my_extern_reference := f +let get_extern_reference () = !my_extern_reference + +let extern_reference loc vars l = !my_extern_reference loc vars l + +let in_debugger = ref false (************************************************************************) @@ -303,10 +304,10 @@ let make_notation_gen loc ntn mknot mkprim destprim l = match decompose_notation_key ntn, l with | [Terminal "-"; Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x))) - with _ -> mknot (loc,ntn,[])) + with e when Errors.noncritical e -> mknot (loc,ntn,[])) | [Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.of_string x)) - with _ -> mknot (loc,ntn,[])) + with e when Errors.noncritical e -> mknot (loc,ntn,[])) | _ -> mknot (loc,ntn,l) @@ -816,12 +817,14 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function match f with | GRef (_,ref) -> let subscopes = - try list_skipn n (find_arguments_scope ref) with _ -> [] in + try list_skipn n (find_arguments_scope ref) + with e when Errors.noncritical e -> [] in let impls = let impls = select_impargs_size (List.length args) (implicits_of_global ref) in - try list_skipn n impls with _ -> [] in + try list_skipn n impls + with e when Errors.noncritical e -> [] in subscopes,impls | _ -> [], [] in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 1a1560e5..55fababd 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -50,9 +50,12 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -(** Debug printing options *) -val set_debug_global_reference_printer : - (loc -> global_reference -> reference) -> unit +(** Customization of the global_reference printer *) +val set_extern_reference : + (loc -> Idset.t -> global_reference -> reference) -> unit +val get_extern_reference : + unit -> (loc -> Idset.t -> global_reference -> reference) + val in_debugger : bool ref (** This governs printing of implicit arguments. If [with_implicits] is diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 81e4501a..e806686a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -650,7 +650,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; GRef (loc, ref), impls, scopes, [] - with _ -> + with e when Errors.noncritical e -> (* [id] a goal variable *) GVar (loc,id), [], [], [] @@ -716,7 +716,7 @@ let intern_applied_reference intern env namedctx lvar args = function try let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in find_appl_head_data r, args2 - with e -> + with e when Errors.noncritical e -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (GVar (loc,id), [], [], []),args @@ -969,15 +969,15 @@ let sort_fields mode loc l completer = | [] -> anomaly "Number of projections mismatch" | (_, regular)::tm -> let boolean = not regular in - if ConstRef name = global_reference_of_reference refer - then + (match global_reference_of_reference refer with + | ConstRef name' when eq_constant name name' -> if boolean && mode then user_err_loc (loc, "", str"No local fields allowed in a record construction.") else build_patt b tm (i + 1) (i, snd acc) (* we found it *) - else + | _ -> build_patt b tm (if boolean&&mode then i else i + 1) (if boolean && mode then acc - else fst acc, (i, ConstRef name) :: snd acc)) + else fst acc, (i, ConstRef name) :: snd acc))) | None :: b-> (* we don't want anonymous fields *) if mode then user_err_loc (loc, "", str "This record contains anonymous fields.") @@ -1009,7 +1009,7 @@ let sort_fields mode loc l completer = (loc, "", str "This record contains fields of different records.") | (i, a) :: b-> - if glob_refer = a + if eq_gr glob_refer a then (i,List.rev_append acc l) else add_patt b ((i,a)::acc) in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 9950178c..2c000258 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -88,8 +88,8 @@ let is_freevar ids env x = if Idset.mem x ids then false else try ignore(Environ.lookup_named x env) ; false - with _ -> not (is_global x) - with _ -> true + with e when Errors.noncritical e -> not (is_global x) + with e when Errors.noncritical e -> true (* Auxiliary functions for the inference of implicitly quantified variables. *) diff --git a/interp/notation.ml b/interp/notation.ml index e3fb5d5e..03fa23a3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -838,4 +838,4 @@ let _ = let with_notation_protection f x = let fs = freeze () in try let a = f x in unfreeze fs; a - with e -> unfreeze fs; raise e + with reraise -> unfreeze fs; raise reraise diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 8d09cbd7..9c9f6a57 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -190,7 +190,9 @@ and eval_to_patch env (buff,pl,fv) = and val_of_constr env c = let (_,fun_code,_ as ccfv) = try compile env c - with e -> print_string "can not compile \n";Format.print_flush();raise e in + with reraise -> + print_string "can not compile \n";Format.print_flush();raise reraise + in eval_to_patch env (to_memory ccfv) let set_transparent_const kn = diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 15a48e1c..9aeaf110 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -83,13 +83,14 @@ let string_of_hint = function | Equiv kn -> string_of_kn kn let debug_string_of_delta resolve = - let kn_to_string kn hint s = - s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint) + let kn_to_string kn hint l = + (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l in - let mp_to_string mp mp' s = - s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp') + let mp_to_string mp mp' l = + (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l in - Deltamap.fold mp_to_string kn_to_string resolve "" + let l = Deltamap.fold mp_to_string kn_to_string resolve [] in + String.concat ", " (List.rev l) let list_contents sub = let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in @@ -173,7 +174,7 @@ let solve_delta_kn resolve kn = let kn_of_delta resolve kn = try solve_delta_kn resolve kn - with _ -> kn + with e when Errors.noncritical e -> kn let constant_of_delta_kn resolve kn = constant_of_kn_equiv kn (kn_of_delta resolve kn) @@ -182,7 +183,7 @@ let gen_of_delta resolve x kn fix_can = try let new_kn = solve_delta_kn resolve kn in if kn == new_kn then x else fix_can new_kn - with _ -> x + with e when Errors.noncritical e -> x let constant_of_delta resolve con = let kn = user_con con in @@ -223,8 +224,10 @@ let constant_of_delta_with_inline resolve con = let kn1,kn2 = canonical_con con,user_con con in try find_inline_of_delta kn2 resolve with Not_found -> - try find_inline_of_delta kn1 resolve - with Not_found -> None + if kn1 == kn2 then None + else + try find_inline_of_delta kn1 resolve + with Not_found -> None let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = @@ -272,7 +275,9 @@ type sideconstantsubst = | Canonical let gen_subst_mp f sub mp1 mp2 = - match subst_mp0 sub mp1, subst_mp0 sub mp2 with + let o1 = subst_mp0 sub mp1 in + let o2 = if mp1 == mp2 then o1 else subst_mp0 sub mp2 in + match o1, o2 with | None, None -> raise No_subst | Some (mp',resolve), None -> User, (f mp' mp2), resolve | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve diff --git a/kernel/modops.ml b/kernel/modops.ml index af32288c..a81f868e 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -33,7 +33,7 @@ type signature_mismatch_error = | NotConvertibleInductiveField of identifier | NotConvertibleConstructorField of identifier | NotConvertibleBodyField - | NotConvertibleTypeField + | NotConvertibleTypeField of env * types * types | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool diff --git a/kernel/modops.mli b/kernel/modops.mli index d03d61bd..daea3258 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -9,6 +9,7 @@ open Util open Names open Univ +open Term open Environ open Declarations open Entries @@ -60,7 +61,7 @@ type signature_mismatch_error = | NotConvertibleInductiveField of identifier | NotConvertibleConstructorField of identifier | NotConvertibleBodyField - | NotConvertibleTypeField + | NotConvertibleTypeField of env * types * types | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool diff --git a/kernel/names.ml b/kernel/names.ml index 17bda124..8c228404 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -205,7 +205,9 @@ type constant = kernel_name*kernel_name let constant_of_kn kn = (kn,kn) let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) let make_con mp dir l = constant_of_kn (mp,dir,l) -let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) +let make_con_equiv mp1 mp2 dir l = + if mp1 == mp2 then make_con mp1 dir l + else ((mp1,dir,l),(mp2,dir,l)) let canonical_con con = snd con let user_con con = fst con let repr_con con = fst con @@ -263,8 +265,10 @@ let constr_modpath c = ind_modpath (fst c) let mind_of_kn kn = (kn,kn) let mind_of_kn_equiv kn1 kn2 = (kn1,kn2) -let make_mind mp dir l = ((mp,dir,l),(mp,dir,l)) -let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) +let make_mind mp dir l = mind_of_kn (mp,dir,l) +let make_mind_equiv mp1 mp2 dir l = + if mp1 == mp2 then make_mind mp1 dir l + else ((mp1,dir,l),(mp2,dir,l)) let canonical_mind mind = snd mind let user_mind mind = fst mind let repr_mind mind = fst mind diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 6c08c34c..f0a3292c 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -90,7 +90,7 @@ let push_rel d env = let lookup_rel_val n env = try List.nth env.env_rel_val (n - 1) - with _ -> raise Not_found + with e when Errors.noncritical e -> raise Not_found let env_of_rel n env = { env with diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 1d606782..ec891e13 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -477,7 +477,7 @@ let end_module l restype senv = in let str = match sign with | SEBstruct(str_l) -> str_l - | _ -> error ("You cannot Include a high-order structure.") + | _ -> error ("You cannot Include a higher-order structure.") in let senv = update_resolver (add_delta_resolver resolver) senv in @@ -873,7 +873,8 @@ end = struct let k = key_of_lazy_constr k in let access key = try (Lazy.force table).(key) - with _ -> error "Error while retrieving an opaque body" + with e when Errors.noncritical e -> + error "Error while retrieving an opaque body" in match load_proof with | Flags.Force -> diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e2c5f48c..c809572a 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -219,6 +219,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = + let err = NotConvertibleTypeField (env, t1, t2) in + (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion algorithm is not ready to handle. Anyway, generated types of @@ -257,12 +259,12 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = (the user has to use an explicit type in the interface *) error NoTypeConstraintExpected with NotArity -> - error NotConvertibleTypeField end + error err end | _ -> t1,t2 else (t1,t2) in - check_conv NotConvertibleTypeField cst conv_leq env t1 t2 + check_conv err cst conv_leq env t1 t2 in match info1 with @@ -301,7 +303,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if constant_has_body cb2 then error DefinitionFieldExpected; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2 + let error = NotConvertibleTypeField (env, arity1, typ2) in + check_conv error cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ @@ -312,7 +315,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if constant_has_body cb2 then error DefinitionFieldExpected; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv NotConvertibleTypeField cst conv env ty1 ty2 + let error = NotConvertibleTypeField (env, ty1, ty2) in + check_conv error cst conv env ty1 ty2 let rec check_modules cst env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in diff --git a/lib/envars.ml b/lib/envars.ml index 4ec68a27..c672d30c 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -23,6 +23,8 @@ let _ = if Coq_config.arch = "win32" then Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "") +let exe s = s ^ Coq_config.exec_extension + let reldir instdir testfile oth = let rpath = if Coq_config.local then [] else instdir in let out = List.fold_left Filename.concat coqroot rpath in @@ -87,19 +89,19 @@ let rec which l f = else which tl f let guess_camlbin () = - let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let path = Sys.getenv "PATH" in (* may raise Not_found *) let lpath = path_to_list path in - which lpath "ocamlc" + which lpath (exe "ocamlc") let guess_camlp4bin () = - let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let path = Sys.getenv "PATH" in (* may raise Not_found *) let lpath = path_to_list path in - which lpath Coq_config.camlp4 + which lpath (exe Coq_config.camlp4) let camlbin () = if !Flags.camlbin_spec then !Flags.camlbin else if !Flags.boot then Coq_config.camlbin else - try guess_camlbin () with _ -> Coq_config.camlbin + try guess_camlbin () with e when e <> Sys.Break -> Coq_config.camlbin let camllib () = if !Flags.boot @@ -113,9 +115,10 @@ let camllib () = let camlp4bin () = if !Flags.camlp4bin_spec then !Flags.camlp4bin else if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () with _ -> let cb = camlbin () in - if Sys.file_exists (Filename.concat cb Coq_config.camlp4) then cb - else Coq_config.camlp4bin + try guess_camlp4bin () with e when e <> Sys.Break -> + let cb = camlbin () in + if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb + else Coq_config.camlp4bin let camlp4lib () = if !Flags.boot diff --git a/lib/errors.ml b/lib/errors.ml index 3b5e6770..6affea23 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -28,7 +28,7 @@ let rec print_gen bottom stk e = try h e with | Unhandled -> print_gen bottom stk' e - | e' -> print_gen bottom stk' e' + | any -> print_gen bottom stk' any (** Only anomalies should reach the bottom of the handler stack. In usual situation, the [handle_stack] is treated as it if was always @@ -66,3 +66,14 @@ let _ = register_handler begin function | _ -> raise Unhandled end +(** Critical exceptions shouldn't be catched and ignored by mistake + by inner functions during a [vernacinterp]. They should be handled + only at the very end of interp, to be displayed to the user. *) + +(** NB: in the 8.4 branch, for maximal compatibility, anomalies + are considered non-critical *) + +let noncritical = function + | Sys.Break | Out_of_memory | Stack_overflow -> false + | _ -> true + diff --git a/lib/errors.mli b/lib/errors.mli index eb7fde8e..ae4d0b85 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -39,3 +39,11 @@ val print_no_report : exn -> Pp.std_ppcmds (** Same as [print], except that anomalies are not printed but re-raised (used for the Fail command) *) val print_no_anomaly : exn -> Pp.std_ppcmds + +(** Critical exceptions shouldn't be catched and ignored by mistake + by inner functions during a [vernacinterp]. They should be handled + only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user. + Typical example: [Sys.Break]. In the 8.4 branch, for maximal + compatibility, anomalies are not considered as critical... +*) +val noncritical : exn -> bool diff --git a/lib/flags.ml b/lib/flags.ml index 3474573e..32c68b25 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -9,12 +9,12 @@ let with_option o f x = let old = !o in o:=true; try let r = f x in o := old; r - with e -> o := old; raise e + with reraise -> o := old; raise reraise let without_option o f x = let old = !o in o:=false; try let r = f x in o := old; r - with e -> o := old; raise e + with reraise -> o := old; raise reraise let boot = ref false diff --git a/lib/hashtbl_alt.ml b/lib/hashtbl_alt.ml index 2780afe8..bb2252da 100644 --- a/lib/hashtbl_alt.ml +++ b/lib/hashtbl_alt.ml @@ -89,7 +89,7 @@ module Make (E : Hashtype) = match rest2 with | Empty -> add hash key; key | Cons (k3, h3, rest3) -> - if hash == h2 && E.equals key k3 then k3 + if hash == h3 && E.equals key k3 then k3 else find_rec hash key rest3 end diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 7777d091..569a028f 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -279,7 +279,7 @@ let pp_dirs ft = try Stream.iter pp_dir dirstream; com_brk ft with - | e -> Format.pp_print_flush ft () ; raise e + | reraise -> Format.pp_print_flush ft () ; raise reraise (* pretty print on stdout and stderr *) diff --git a/lib/profile.ml b/lib/profile.ml index 2472d75d..39e08721 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -260,7 +260,7 @@ let time_overhead_B_C () = let _dw = dummy_spent_alloc () in let _dt = get_time () in () - with _ -> assert false + with e when e <> Sys.Break -> assert false done; let after = get_time () in let beforeloop = get_time () in @@ -390,7 +390,7 @@ let profile1 e f a = (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r - with exn -> + with reraise -> let dw = spent_alloc () in let dt = get_time () - t in e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; @@ -403,7 +403,7 @@ let profile1 e f a = if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); - raise exn + raise reraise let profile2 e f a b = let dw = spent_alloc () in @@ -432,7 +432,7 @@ let profile2 e f a b = (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r - with exn -> + with reraise -> let dw = spent_alloc () in let dt = get_time () - t in e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; @@ -445,7 +445,7 @@ let profile2 e f a b = if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); - raise exn + raise reraise let profile3 e f a b c = let dw = spent_alloc () in @@ -474,7 +474,7 @@ let profile3 e f a b c = (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r - with exn -> + with reraise -> let dw = spent_alloc () in let dt = get_time () - t in e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; @@ -487,7 +487,7 @@ let profile3 e f a b c = if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); - raise exn + raise reraise let profile4 e f a b c d = let dw = spent_alloc () in @@ -516,7 +516,7 @@ let profile4 e f a b c d = (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r - with exn -> + with reraise -> let dw = spent_alloc () in let dt = get_time () - t in e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; @@ -529,7 +529,7 @@ let profile4 e f a b c d = if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); - raise exn + raise reraise let profile5 e f a b c d g = let dw = spent_alloc () in @@ -558,7 +558,7 @@ let profile5 e f a b c d g = (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r - with exn -> + with reraise -> let dw = spent_alloc () in let dt = get_time () - t in e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; @@ -571,7 +571,7 @@ let profile5 e f a b c d g = if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); - raise exn + raise reraise let profile6 e f a b c d g h = let dw = spent_alloc () in @@ -600,7 +600,7 @@ let profile6 e f a b c d g h = (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r - with exn -> + with reraise -> let dw = spent_alloc () in let dt = get_time () - t in e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; @@ -613,7 +613,7 @@ let profile6 e f a b c d g h = if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); - raise exn + raise reraise let profile7 e f a b c d g h i = let dw = spent_alloc () in @@ -642,7 +642,7 @@ let profile7 e f a b c d g h i = (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r - with exn -> + with reraise -> let dw = spent_alloc () in let dt = get_time () - t in e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; @@ -655,7 +655,7 @@ let profile7 e f a b c d g h i = if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); - raise exn + raise reraise (* Some utilities to compute the logical and physical sizes and depth of ML objects *) diff --git a/lib/store.ml b/lib/store.ml index bc1b335f..28eb65c8 100644 --- a/lib/store.ml +++ b/lib/store.ml @@ -53,7 +53,7 @@ let field () = in let get s = try Some (Obj.obj (Util.Intmap.find fid s)) - with _ -> None + with Not_found -> None in let remove s = Util.Intmap.remove fid s diff --git a/lib/system.ml b/lib/system.ml index a99c29f2..ae637708 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -140,7 +140,8 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames let ok_dirname f = f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) && - try ignore (check_ident f); true with _ -> false + try ignore (check_ident f); true + with e when e <> Sys.Break -> false let all_subdirs ~unix_path:root = let l = ref [] in @@ -223,17 +224,22 @@ let file_readable_p name = try access name [R_OK];true with Unix_error (_, _, _) -> false let open_trapping_failure name = - try open_out_bin name with _ -> error ("Can't open " ^ name) + try open_out_bin name + with e when e <> Sys.Break -> error ("Can't open " ^ name) let try_remove filename = try Sys.remove filename - with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++ - str filename ++ str" which is corrupted!" ) + with e when e <> Sys.Break -> + msgnl (str"Warning: " ++ str"Could not remove file " ++ + str filename ++ str" which is corrupted!" ) let marshal_out ch v = Marshal.to_channel ch v [] -let marshal_in ch = +let marshal_in filename ch = try Marshal.from_channel ch - with End_of_file -> error "corrupted file: reached end of file" + with + | End_of_file -> error "corrupted file: reached end of file" + | Failure _ (* e.g. "truncated object" *) -> + error (filename ^ " is corrupted, try to rebuild it.") exception Bad_magic_number of string @@ -259,14 +265,14 @@ let extern_intern ?(warn=true) magic suffix = try marshal_out channel val_0; close_out channel - with e -> - begin try_remove filename; raise e end + with reraise -> + begin try_remove filename; raise reraise end with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in let channel = raw_intern filename in - let v = marshal_in channel in + let v = marshal_in filename channel in close_in channel; v with Sys_error s -> diff --git a/lib/system.mli b/lib/system.mli index 4a79b874..d8420e7d 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -47,7 +47,7 @@ val find_file_in_path : when the check fails, with the full file name. *) val marshal_out : out_channel -> 'a -> unit -val marshal_in : in_channel -> 'a +val marshal_in : string -> in_channel -> 'a exception Bad_magic_number of string diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml index 19bab4f6..600796f7 100644 --- a/lib/xml_parser.ml +++ b/lib/xml_parser.ml @@ -175,7 +175,7 @@ let do_parse xparser source = if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected); Xml_lexer.close source; x - with e -> + with e when e <> Sys.Break -> Xml_lexer.close source; raise (!xml_error (error_of_exn stk e) source) @@ -190,9 +190,9 @@ let parse p = function close_in ch; x with - e -> + reraise -> close_in ch; - raise e + raise reraise let error_msg = function diff --git a/library/declaremods.ml b/library/declaremods.ml index 80da9e73..db7b8915 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -990,9 +990,9 @@ let declare_include_ interp_struct me_asts = let protect_summaries f = let fs = Summary.freeze_summaries () in try f fs - with e -> + with reraise -> (* Something wrong: undo the whole process *) - Summary.unfreeze_summaries fs; raise e + Summary.unfreeze_summaries fs; raise reraise let declare_include interp_struct me_asts = protect_summaries diff --git a/library/heads.ml b/library/heads.ml index b860dc2a..c33ea9b1 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -88,7 +88,7 @@ let kind_of_head env t = | Sort _ | Ind _ | Prod _ -> RigidHead RigidType | Cast (c,_,_) -> aux k l c b | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b - | Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b + | Lambda (_,_,c) -> aux k (List.tl l) (subst1 (List.hd l) c) b | LetIn _ -> assert false | Meta _ | Evar _ -> NotImmediatelyComputableHead | App (c,al) -> aux k (Array.to_list al @ l) c b diff --git a/library/impargs.ml b/library/impargs.ml index c79edb99..930b8f09 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -74,9 +74,9 @@ let with_implicits flags f x = let rslt = f x in implicit_args := oflags; rslt - with e -> begin + with reraise -> begin implicit_args := oflags; - raise e + raise reraise end let set_maximality imps b = diff --git a/library/library.ml b/library/library.ml index 30e7b675..c857fc86 100644 --- a/library/library.ml +++ b/library/library.ml @@ -368,14 +368,14 @@ let explain_locate_library_error qid = function let try_locate_absolute_library dir = try locate_absolute_library dir - with e -> + with e when Errors.noncritical e -> explain_locate_library_error (qualid_of_dirpath dir) e let try_locate_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in dir,f - with e -> + with e when Errors.noncritical e -> explain_locate_library_error qid e @@ -398,20 +398,20 @@ let fetch_opaque_table (f,pos,digest) = try let ch = System.with_magic_number_check raw_intern_library f in seek_in ch pos; - if System.marshal_in ch <> digest then failwith "File changed!"; - let table = (System.marshal_in ch : LightenLibrary.table) in + if System.marshal_in f ch <> digest then failwith "File changed!"; + let table = (System.marshal_in f ch : LightenLibrary.table) in close_in ch; table - with _ -> + with e when Errors.noncritical e -> error ("The file "^f^" is inaccessible or has changed,\n" ^ "cannot load some opaque constant bodies in it.\n") let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in - let lmd = System.marshal_in ch in + let lmd = System.marshal_in f ch in let pos = pos_in ch in - let digest = System.marshal_in ch in + let digest = System.marshal_in f ch in let table = lazy (fetch_opaque_table (f,pos,digest)) in register_library_filename lmd.md_name f; let library = mk_library lmd table digest in @@ -655,7 +655,8 @@ let save_library_to dir f = System.marshal_out ch di; System.marshal_out ch table; close_out ch - with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e + with reraise -> + warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise (************************************************************************) (*s Display the memory use of a library. *) diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 184985b5..7a214bcd 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -393,14 +393,17 @@ let extra_rules () = begin Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc; A "--output-format";A "coff";A "--output"; Px o])); -(** The windows version of Coqide is now a console-free win32 app, - which moreover contains the Coq icon. If necessary, the mkwinapp - tool can be used later to restore or suppress the console of Coqide. *) +(** Embed the Coq icon inside the windows version of Coqide *) if w32 then dep ["link"; "ocaml"; "program"; "ide"] [w32ico]; - - if w32 then flag ["link"; "ocaml"; "program"; "ide"] - (S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]); + if w32 then flag ["link"; "ocaml"; "program"; "ide"] (P w32ico); + +(** Ealier we tried to make Coqide a console-free win32 app, + but that was troublesome (unavailable stdout/stderr, issues + with the stop button,...). If somebody really want to try again, + the extra args to add are : + [A "-ccopt"; A "-link -Wl,-subsystem,windows"] + Other solution: use the mkwinapp tool. *) (** The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/". Let's tweak that... *) diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 1888ef17..214a6b98 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -146,7 +146,7 @@ let possibly_empty_subentries loc (prods,act) = (* an exception rather than returning a value; *) (* declares loc because some code can refer to it; *) (* ensures loc is used to avoid "unused variable" warning *) - (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>) + (true, <:expr< try Some $aux prods$ with [ e when Errors.noncritical e -> None ] >>) else (* Static optimisation *) (false, aux prods) diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index c68ba137..12359776 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -365,4 +365,4 @@ let _ = let with_grammar_rule_protection f x = let fs = freeze () in try let a = f x in unfreeze fs; a - with e -> unfreeze fs; raise e + with reraise -> unfreeze fs; raise reraise diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d265729a..1609e541 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -126,7 +126,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = let induction_arg_of_constr (c,lbind as clbind) = if lbind = NoBindings then try ElimOnIdent (constr_loc c,snd(coerce_to_id c)) - with _ -> ElimOnConstr clbind + with e when Errors.noncritical e -> ElimOnConstr clbind else ElimOnConstr clbind let mkTacCase with_evar = function diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 9dd0e369..869674f4 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -104,7 +104,8 @@ let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) let get_xml_inductive_kn al = inductive_of_cdata (* uriType apparent synonym of uri *) - (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al) + (try get_xml_attr "uri" al + with e when Errors.noncritical e -> get_xml_attr "uriType" al) let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index d3eb40d0..99e10908 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -273,7 +273,9 @@ let print_inductive_implicit_args = let print_inductive_renames = print_args_data_of_inductive_ids - (fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> []) + (fun r -> + try List.hd (Arguments_renaming.arguments_names r) + with e when Errors.noncritical e -> []) ((<>) Anonymous) print_renames_list @@ -737,7 +739,7 @@ let print_coercions () = let index_of_class cl = try fst (class_info cl) - with _ -> + with e when Errors.noncritical e -> errorlabstrm "index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") @@ -747,7 +749,7 @@ let print_path_between cls clt = let p = try lookup_path_between_class (i,j) - with _ -> + with e when Errors.noncritical e -> errorlabstrm "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") diff --git a/parsing/printer.ml b/parsing/printer.ml index 9f0cb00d..29ebe4fa 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -24,6 +24,7 @@ open Pfedit open Ppconstr open Constrextern open Tacexpr +open Declarations open Store.Field @@ -118,6 +119,63 @@ let pr_sort s = pr_glob_sort (extern_sort s) let _ = Termops.set_print_constr pr_lconstr_env + +(** Term printers resilient to [Nametab] errors *) + +(** When the nametab isn't up-to-date, the term printers above + could raise [Not_found] during [Nametab.shortest_qualid_of_global]. + In this case, we build here a fully-qualified name based upon + the kernel modpath and label of constants, and the idents in + the [mutual_inductive_body] for the inductives and constructors + (needs an environment for this). *) + +let id_of_global env = function + | ConstRef kn -> id_of_label (con_label kn) + | IndRef (kn,0) -> id_of_label (mind_label kn) + | IndRef (kn,i) -> + (Environ.lookup_mind kn env).mind_packets.(i).mind_typename + | ConstructRef ((kn,i),j) -> + (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1) + | VarRef v -> v + +let cons_dirpath id dp = make_dirpath (id :: repr_dirpath dp) + +let rec dirpath_of_mp = function + | MPfile sl -> sl + | MPbound uid -> make_dirpath [id_of_mbid uid] + | MPdot (mp,l) -> cons_dirpath (id_of_label l) (dirpath_of_mp mp) + +let dirpath_of_global = function + | ConstRef kn -> dirpath_of_mp (con_modpath kn) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + dirpath_of_mp (mind_modpath kn) + | VarRef _ -> empty_dirpath + +let qualid_of_global env r = + Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) + +let safe_gen f env c = + let orig_extern_ref = Constrextern.get_extern_reference () in + let extern_ref loc vars r = + try orig_extern_ref loc vars r + with e when Errors.noncritical e -> + Libnames.Qualid (loc, qualid_of_global env r) + in + Constrextern.set_extern_reference extern_ref; + try + let p = f env c in + Constrextern.set_extern_reference orig_extern_ref; + p + with e when Errors.noncritical e -> + Constrextern.set_extern_reference orig_extern_ref; + str "??" + +let safe_pr_lconstr_env = safe_gen pr_lconstr_env +let safe_pr_constr_env = safe_gen pr_constr_env +let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t +let safe_pr_constr t = safe_pr_constr_env (Global.env()) t + + (**********************************************************************) (* Global references *) @@ -389,7 +447,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = | None -> let exl = Evarutil.non_instantiated sigma in if exl = [] then - (str"No more subgoals." + (str"No more subgoals." ++ fnl () ++ emacs_print_dependent_evars sigma seeds) else let pei = pr_evars_int 1 exl in @@ -415,7 +473,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = v 0 ( int(List.length rest+1) ++ str" subgoals" ++ str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut () - ++ goals + ++ goals ++ fnl () ++ emacs_print_dependent_evars sigma seeds ) | g1::rest,a::l -> @@ -589,7 +647,7 @@ let pr_assumptionset env s = str (string_of_mp mp ^ "." ^ string_of_label lab) in let safe_pr_ltype typ = - try str " : " ++ pr_ltype typ with _ -> mt () + try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt () in let (vars,axioms,opaque) = ContextObjectMap.fold (fun t typ r -> @@ -647,7 +705,6 @@ let pr_instance_gmap insts = (** Inductive declarations *) -open Declarations open Termops open Reduction open Inductive diff --git a/parsing/printer.mli b/parsing/printer.mli index a034f0ed..3abe90e7 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -31,6 +31,17 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +(** Same, but resilient to [Nametab] errors. Prints fully-qualified + names when [shortest_qualid_of_global] has failed. Prints "??" + in case of remaining issues (such as reference not in env). *) + +val safe_pr_lconstr_env : env -> constr -> std_ppcmds +val safe_pr_lconstr : constr -> std_ppcmds + +val safe_pr_constr_env : env -> constr -> std_ppcmds +val safe_pr_constr : constr -> std_ppcmds + + val pr_open_constr_env : env -> open_constr -> std_ppcmds val pr_open_constr : open_constr -> std_ppcmds diff --git a/parsing/printmod.ml b/parsing/printmod.ml index b4a8fdfd..b46cf42d 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -68,12 +68,17 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn +(** Each time we have to print a non-globally visible structure, + we place its elements in a fake fresh namespace. *) + +let mk_fake_top = + let r = ref 0 in + fun () -> incr r; id_of_string ("FAKETOP"^(string_of_int !r)) + let nametab_register_dir mp = - let id = id_of_string "FAKETOP" in - let fp = Libnames.make_path empty_dirpath id in + let id = mk_fake_top () in let dir = make_dirpath [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath))); - fp + Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath))) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here @@ -81,9 +86,10 @@ let nametab_register_dir mp = the user names. This works nonetheless since we search now [Nametab.the_globrevtab] modulo user name. *) -let nametab_register_body mp fp (l,body) = +let nametab_register_body mp dir (l,body) = let push id ref = - Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref + Nametab.push (Nametab.Until (1+List.length (repr_dirpath dir))) + (make_path dir id) ref in match body with | SFBmodule _ -> () (* TODO *) @@ -99,6 +105,27 @@ let nametab_register_body mp fp (l,body) = mip.mind_consnames) mib.mind_packets +let nametab_register_module_body mp struc = + (* If [mp] is a globally visible module, we simply import it *) + try Declaremods.really_import_module mp + with Not_found -> + (* Otherwise we try to emulate an import by playing with nametab *) + nametab_register_dir mp; + List.iter (nametab_register_body mp empty_dirpath) struc + +let nametab_register_module_param mbid seb = + (* For algebraic seb, we use a Declaremods function that converts into mse *) + try Declaremods.process_module_seb_binding mbid seb + with e when Errors.noncritical e -> + (* Otherwise, for expanded structure, we try to play with the nametab *) + match seb with + | SEBstruct struc -> + let mp = MPbound mbid in + let dir = make_dirpath [id_of_mbid mbid] in + nametab_register_dir mp; + List.iter (nametab_register_body mp dir) struc + | _ -> () + let print_body is_impl env mp (l,body) = let name = str (string_of_label l) in hov 2 (match body with @@ -126,19 +153,11 @@ let print_body is_impl env mp (l,body) = try let env = Option.get env in Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib - with _ -> + with e when Errors.noncritical e -> (if mib.mind_finite then str "Inductive " else str "CoInductive") ++ name) let print_struct is_impl env mp struc = - begin - (* If [mp] is a globally visible module, we simply import it *) - try Declaremods.really_import_module mp - with _ -> - (* Otherwise we try to emulate an import by playing with nametab *) - let fp = nametab_register_dir mp in - List.iter (nametab_register_body mp fp) struc - end; prlist_with_sep spc (print_body is_impl env mp) struc let rec flatten_app mexpr l = match mexpr with @@ -156,7 +175,7 @@ let rec print_modtype env mp locals mty = let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ()); + nametab_register_module_param mbid seb1; hov 2 (str "Funsig" ++ spc () ++ str "(" ++ pr_id (id_of_mbid mbid) ++ str ":" ++ print_modtype env mp1 locals seb1 ++ @@ -164,6 +183,7 @@ let rec print_modtype env mp locals mty = | SEBstruct (sign) -> let env' = Option.map (Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in + nametab_register_module_body mp sign; hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++ brk (1,-2) ++ str "End") | SEBapply _ -> @@ -190,13 +210,14 @@ let rec print_modexpr env mp locals mexpr = match mexpr with (Modops.add_module (Modops.module_body_of_type mp' mty)) env in let typ = Option.default mty.typ_expr mty.typ_expr_alg in let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - (try Declaremods.process_module_seb_binding mbid typ with _ -> ()); + nametab_register_module_param mbid typ; hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ str ":" ++ print_modtype env mp' locals typ ++ str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr) | SEBstruct struc -> let env' = Option.map (Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in + nametab_register_module_body mp struc; hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++ brk (1,-2) ++ str "End") | SEBapply _ -> @@ -243,7 +264,7 @@ let print_module with_body mp = try if !short then raise ShortPrinting; print_module' (Some (Global.env ())) mp with_body me ++ fnl () - with _ -> + with e when Errors.noncritical e -> print_module' None mp with_body me ++ fnl () let print_modtype kn = @@ -254,5 +275,5 @@ let print_modtype kn = (try if !short then raise ShortPrinting; print_modtype' (Some (Global.env ())) kn mtb.typ_expr - with _ -> + with e when Errors.noncritical e -> print_modtype' None kn mtb.typ_expr)) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index dbc06856..77364180 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -188,11 +188,11 @@ let declare_tactic loc s cl = Tacexpr.TacExtend($default_loc$,$se$,l))) | None -> () ]) $atomic_tactics$ - with e -> + with [ e when Errors.noncritical e -> Pp.msg_warning (Stream.iapp (Pp.str ("Exception in tactic extend " ^ $se$ ^": ")) - (Errors.print e)); + (Errors.print e)) ]; Egrammar.extend_tactic_grammar $se$ $gl$; List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> ]) diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 4f39019f..bcdf7cff 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -55,11 +55,11 @@ let declare_command loc s nt cl = declare_str_items loc [ <:str_item< do { try Vernacinterp.vinterp_add $se$ $funcl$ - with e -> + with [ e when Errors.noncritical e -> Pp.msg_warning (Stream.iapp (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) - (Errors.print e)); + (Errors.print e)) ]; Egrammar.extend_vernac_command_grammar $se$ $nt$ $gl$ } >> ] 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 diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bdf94e0d..86f96c7c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -126,7 +126,7 @@ module Default = 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 evd j = let t = whd_betadeltaiota env evd j.uj_type in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a74e4cb4..0166b64c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -272,7 +272,7 @@ let is_nondep_branch c n = try let sign,ccl = decompose_lam_n_assum n c in noccur_between 1 (rel_context_length sign) ccl - with _ -> (* Not eta-expanded or not reduced *) + with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) false let extract_nondep_branches test c b n = @@ -386,7 +386,7 @@ let rec detype (isgoal:bool) avoid env t = | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id) - with _ -> + with e when Errors.noncritical e -> GVar (dl, id)) | Sort s -> GSort (dl,detype_sort s) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> @@ -492,7 +492,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl = let mat = build_tree Anonymous isgoal (avoid,env) ci bl in List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c)) mat - with _ -> + with e when Errors.noncritical e -> Array.to_list (array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 14f35941..0eed1949 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -454,7 +454,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) else Evd.set_leq_sort evd s1 s2 in (evd', true) with Univ.UniverseInconsistency _ -> (evd, false) - | _ -> (evd, false)) + | e when Errors.noncritical e -> (evd, false)) | Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> ise_and evd @@ -730,12 +730,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] - & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 -> + & List.for_all (fun a -> eq_constr a term2 or isEvar a) + (remove_instance_local_defs evd evk1 (Array.to_list args1)) -> (* The typical kind of constraint coming from pattern-matching return type inference *) choose_less_dependent_instance evk1 evd term2 args1 | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] - & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 -> + & List.for_all (fun a -> eq_constr a term1 or isEvar a) + (remove_instance_local_defs evd evk2 (Array.to_list args2)) -> (* The typical kind of constraint coming from pattern-matching return type inference *) choose_less_dependent_instance evk2 evd term1 args2 diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b0248a84..fc29ba6c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1194,10 +1194,9 @@ let filter_candidates evd evk filter candidates = let closure_of_filter evd evk filter = let evi = Evd.find_undefined evd evk in - let vars = collect_vars (evar_concl evi) in - let ids = List.map pi1 (evar_context evi) in - let test id b = b || Idset.mem id vars in - let newfilter = List.map2 test ids filter in + let vars = collect_vars (nf_evar evd (evar_concl evi)) in + let test (id,c,_) b = b || Idset.mem id vars || c <> None in + let newfilter = List.map2 test (evar_context evi) filter in if newfilter = evar_filter evi then None else Some newfilter let restrict_hyps evd evk filter candidates = @@ -1352,9 +1351,14 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect t in match kind_of_term f with | Construct (ind,_) -> - let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in - let params,_ = array_chop nparams args in - array_for_all (is_constrainable_in k g) params + let nparams = + (fst (Global.lookup_inductive ind)).Declarations.mind_nparams + in + if nparams > Array.length args + then true (* We don't try to be more clever *) + else + let params,_ = array_chop nparams args in + array_for_all (is_constrainable_in k g) params | Ind _ -> array_for_all (is_constrainable_in k g) args | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2 | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*) @@ -1442,7 +1446,7 @@ let check_evar_instance evd evk1 body conv_algo = (* FIXME: The body might be ill-typed when this is called from w_merge *) let ty = try Retyping.get_type_of evenv evd body - with _ -> error "Ill-typed evar instance" + with e when Errors.noncritical e -> error "Ill-typed evar instance" in let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in if b then evd else @@ -1492,7 +1496,10 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs = (filter_compatible_candidates conv_algo env evd evi args rhs) l in match l' with | [] -> error_cannot_unify env evd (mkEvar ev, rhs) - | [c,evd] -> Evd.define evk c evd + | [c,evd] -> + (* solve_candidates might have been called recursively in the mean *) + (* time and the evar been solved by the filtering process *) + if Evd.is_undefined evd evk then Evd.define evk c evd else evd | l when List.length l < List.length l' -> let candidates = List.map fst l in restrict_evar evd evk None (Some candidates) @@ -1643,7 +1650,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in t::l - with _ -> l in + with e when Errors.noncritical e -> l in (match candidates with | [x] -> x | _ -> diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 2b326fd1..591a008c 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -230,3 +230,4 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun -> evar_map +val remove_instance_local_defs : evar_map -> existential_key -> constr list -> constr list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 6d5c98ce..4d9eb897 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -67,9 +67,12 @@ let evar_hyps evi = evi.evar_hyps let evar_context evi = named_context_of_val evi.evar_hyps let evar_body evi = evi.evar_body let evar_filter evi = evi.evar_filter -let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps let evar_filtered_context evi = snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi)) +let evar_filtered_hyps evi = + List.fold_right push_named_context_val (evar_filtered_context evi) + empty_named_context_val +let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps let evar_env evi = List.fold_right push_named (evar_filtered_context evi) (reset_context (Global.env())) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 4813d3b9..dbaf803b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -127,6 +127,7 @@ val evar_concl : evar_info -> constr val evar_context : evar_info -> named_context val evar_filtered_context : evar_info -> named_context val evar_hyps : evar_info -> named_context_val +val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body val evar_filter : evar_info -> bool list val evar_unfiltered_env : evar_info -> env diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index bb0a0e92..bdccc57b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -290,6 +290,7 @@ let find_rectype env sigma c = match kind_of_term t with | Ind ind -> let (mib,mip) = Inductive.lookup_mind_specif env ind in + if mib.mind_nparams > List.length l then raise Not_found; let (par,rargs) = list_chop mib.mind_nparams l in IndType((ind, par),rargs) | _ -> raise Not_found diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d8678371..1dd71fab 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -69,8 +69,9 @@ let search_guard loc env possible_indexes fixdefs = if List.for_all (fun l->1=List.length l) possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env fix with - | e -> if loc = dummy_loc then raise e else Loc.raise loc e); + (try check_fix env fix + with e when Errors.noncritical e -> + if loc = dummy_loc then raise e else Loc.raise loc e); indexes else (* we now search recursively amoungst all combinations *) @@ -109,7 +110,8 @@ let resolve_evars env evdref fail_evar resolve_classes = (* Resolve eagerly, potentially making wrong choices *) evdref := (try consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env !evdref - with e -> if fail_evar then raise e else !evdref) + with e when Errors.noncritical e -> + if fail_evar then raise e else !evdref) let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) = let evdref = ref evd in @@ -441,7 +443,8 @@ module Pretyping_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 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 0f04549f..434fe80c 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -207,16 +207,16 @@ let cs_pattern_of_constr t = match kind_of_term t with App (f,vargs) -> begin - try Const_cs (global_of_constr f) , -1, Array.to_list vargs with - _ -> raise Not_found + try Const_cs (global_of_constr f) , -1, Array.to_list vargs + with e when Errors.noncritical e -> raise Not_found end | Rel n -> Default_cs, pred n, [] | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b] | Sort s -> Sort_cs (family_of_sort s), -1, [] | _ -> begin - try Const_cs (global_of_constr t) , -1, [] with - _ -> raise Not_found + try Const_cs (global_of_constr t) , -1, [] + with e when Errors.noncritical e -> raise Not_found end (* Intended to always succeed *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index fddc7fc7..993ad46b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -924,7 +924,10 @@ let meta_reducible_instance evd b = let u = whd_betaiota Evd.empty u in match kind_of_term u with | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) -> - let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in + let m = + try destMeta c + with e when Errors.noncritical e -> destMeta (pi1 (destCast c)) + in (match try let g,s = List.assoc m metas in @@ -934,7 +937,10 @@ let meta_reducible_instance evd b = | Some g -> irec (mkCase (ci,p,g,bl)) | None -> mkCase (ci,irec p,c,Array.map irec bl)) | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) -> - let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in + let m = + try destMeta f + with e when Errors.noncritical e -> destMeta (pi1 (destCast f)) + in (match try let g,s = List.assoc m metas in diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f16eed6c..3b679fce 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -30,12 +30,12 @@ let rec subst_type env sigma typ = function (* et sinon on substitue *) let sort_of_atomic_type env sigma ft args = - let rec concl_of_arity env ar = - match kind_of_term (whd_betadeltaiota env sigma ar) with - | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b - | Sort s -> s - | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args)) - in concl_of_arity env ft + let rec concl_of_arity env ar args = + match kind_of_term (whd_betadeltaiota env sigma ar), args with + | Prod (na, t, b), h::l -> concl_of_arity (push_rel (na,Some h,t) env) b l + | Sort s, [] -> s + | _ -> anomaly "Not a sort" + in concl_of_arity env ft (Array.to_list args) let type_of_var env id = try let (_,_,ty) = lookup_named id env in ty diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b43b9adb..78b239c0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -125,12 +125,12 @@ type constant_evaluation = (* We use a cache registered as a global table *) -let eval_table = ref Cmap.empty +let eval_table = ref Cmap_env.empty -type frozen = (int * constant_evaluation) Cmap.t +type frozen = (int * constant_evaluation) Cmap_env.t let init () = - eval_table := Cmap.empty + eval_table := Cmap_env.empty let freeze () = !eval_table @@ -291,10 +291,10 @@ let compute_consteval sigma env ref = let reference_eval sigma env = function | EvalConst cst as ref -> (try - Cmap.find cst !eval_table + Cmap_env.find cst !eval_table with Not_found -> begin let v = compute_consteval sigma env ref in - eval_table := Cmap.add cst v !eval_table; + eval_table := Cmap_env.add cst v !eval_table; v end) | ref -> compute_consteval sigma env ref diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b78850d3..0344ebcc 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -118,7 +118,7 @@ let _ = let class_info c = try Gmap.find c !classes - with _ -> not_a_class (Global.env()) (constr_of_global c) + with Not_found -> not_a_class (Global.env()) (constr_of_global c) let global_class_of_constr env c = try class_info (global_of_constr c) @@ -132,7 +132,9 @@ let dest_class_arity env c = let rels, c = Term.decompose_prod_assum c in rels, dest_class_app env c -let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None +let class_of_constr c = + try Some (dest_class_arity (Global.env ()) c) + with e when Errors.noncritical e -> None let rec is_class_type evd c = match kind_of_term c with @@ -215,7 +217,7 @@ let rebuild_class cl = try let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in set_typeclass_transparency cst false false; cl - with _ -> cl + with e when Errors.noncritical e -> cl let class_input : typeclass -> obj = declare_object @@ -238,7 +240,7 @@ let check_instance env sigma c = let (evd, c) = resolve_one_typeclass env sigma (Retyping.get_type_of env sigma c) in Evd.is_empty (Evd.undefined_evars evd) - with _ -> false + with e when Errors.noncritical e -> false let build_subclasses ~check env sigma glob pri = let rec aux pri c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 63cdb378..df5eff6a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -430,8 +430,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag then Evd.set_leq_sort sigma s1 s2 else Evd.set_eq_sort sigma s1 s2 in (sigma', metasubst, evarsubst) - with _ -> error_cannot_unify curenv sigma (m,n)) - + with e when Errors.noncritical e -> + error_cannot_unify curenv sigma (m,n)) + | Lambda (na,t1,c1), Lambda (_,t2,c2) -> unirec_rec (push (na,t1) curenvnb) CONV true wt (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2 @@ -708,10 +709,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 = else (right, st2, res) | (IsSuperType,IsSubType) -> (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1) - with _ -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2)) + with e when Errors.noncritical e -> + (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2)) | (IsSubType,IsSuperType) -> (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2) - with _ -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1)) + with e when Errors.noncritical e -> + (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1)) (* Unification * @@ -913,7 +916,7 @@ let w_merge env with_types flags (evd,metas,evars) = let rec process_eqns failures = function | (mv,status,c)::eqns -> (match (try Inl (unify_type env evd flags mv status c) - with e -> Inr e) + with e when Errors.noncritical e -> Inr e) with | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns | Inl (evd,metas,evars) -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 00efa981..3966146d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -44,7 +44,7 @@ let invert_tag cst tag reloc_tbl = let find_rectype_a env c = let (t, l) = let t = whd_betadeltaiota env c in - try destApp t with _ -> (t,[||]) in + try destApp t with e when Errors.noncritical e -> (t,[||]) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -176,7 +176,10 @@ and nf_stk env c t stk = nf_stk env (mkApp(c,args)) t stk | Zfix (f,vargs) :: stk -> let fa, typ = nf_fix_app env f vargs in - let _,_,codom = try decompose_prod env typ with _ -> exit 120 in + let _,_,codom = + try decompose_prod env typ + with e when Errors.noncritical e -> exit 120 + in nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> let (mind,_ as ind),allargs = find_rectype_a env t in @@ -206,7 +209,10 @@ and nf_predicate env ind mip params v pT = | Vfun f, Prod _ -> let k = nb_rel env in let vb = body_of_vfun k f in - let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in + let name,dom,codom = + try decompose_prod env pT + with e when Errors.noncritical e -> exit 121 + in let dep,body = nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in dep, mkLambda(name,dom,body) @@ -228,7 +234,10 @@ and nf_args env vargs t = let args = Array.init len (fun i -> - let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in + let _,dom,codom = + try decompose_prod env !t + with e when Errors.noncritical e -> exit 123 + in let c = nf_val env (arg vargs i) dom in t := subst1 c codom; c) in !t,args @@ -239,7 +248,10 @@ and nf_bargs env b t = let args = Array.init len (fun i -> - let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in + let _,dom,codom = + try decompose_prod env !t + with e when Errors.noncritical e -> exit 124 + in let c = nf_val env (bfield b i) dom in t := subst1 c codom; c) in args @@ -249,7 +261,7 @@ and nf_fun env f typ = let vb = body_of_vfun k f in let name,dom,codom = try decompose_prod env typ - with _ -> + with e when Errors.noncritical e -> raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ)) in let body = nf_val (push_rel (name,None,dom) env) vb codom in diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 4462062c..f271a6bd 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -42,7 +42,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let sigma',typed_c = try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc - with _ -> + with e when Errors.noncritical e -> let loc = Glob_term.loc_of_glob_constr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ diff --git a/proofs/goal.ml b/proofs/goal.ml index dc1ac5dd..37ebce67 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -276,7 +276,7 @@ let check_typability env sigma c = let recheck_typability (what,id) env sigma t = try check_typability env sigma t - with _ -> + with e when Errors.noncritical e -> let s = match what with | None -> "the conclusion" | Some id -> "hypothesis "^(Names.string_of_id id) in @@ -474,7 +474,7 @@ module V82 = struct (* Old style hyps primitive *) let hyps evars gl = let evi = content evars gl in - evi.Evd.evar_hyps + Evd.evar_filtered_hyps evi (* Access to ".evar_concl" *) let concl evars gl = @@ -554,10 +554,16 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl new_hyps = + (* Used for congruence closure and change *) + let new_goal_with sigma gl extra_hyps = let evi = content sigma gl in - let new_evi = { evi with Evd.evar_hyps = new_hyps } in + let hyps = evi.Evd.evar_hyps in + let new_hyps = + List.fold_right Environ.push_named_context_val extra_hyps hyps in + let extra_filter = List.map (fun _ -> true) extra_hyps in + let new_filter = extra_filter @ evi.Evd.evar_filter in + let new_evi = + { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in let evk = Evarutil.new_untyped_evar () in let new_sigma = Evd.add Evd.empty evk new_evi in diff --git a/proofs/goal.mli b/proofs/goal.mli index 9cd439ab..c0a094d3 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -232,7 +232,7 @@ module V82 : sig val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Environ.named_context_val -> goal Evd.sigma + val new_goal_with : Evd.evar_map -> goal -> Sign.named_context -> goal Evd.sigma (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index d240c1e1..497ab1fa 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -105,7 +105,7 @@ let clear_hyps sigma ids sign cl = let recheck_typability (what,id) env sigma t = try check_typability env sigma t - with _ -> + with e when Errors.noncritical e -> let s = match what with | None -> "the conclusion" | Some id -> "hypothesis "^(string_of_id id) in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 45e4a84e..7bac87d2 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -68,7 +68,7 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook = | None -> Proofview.tclUNIT () in try Proof_global.run_tactic tac - with e -> Proof_global.discard_current (); raise e + with reraise -> Proof_global.discard_current (); raise reraise let restart_proof () = undo_todepth 1 @@ -164,9 +164,9 @@ let build_constant_by_tactic id sign typ tac = let _,(const,_,_,_) = cook_proof (fun _ -> ()) in delete_current_proof (); const - with e -> + with reraise -> delete_current_proof (); - raise e + raise reraise let build_by_tactic env typ tac = let id = id_of_string ("temporary_proof"^string_of_int (next())) in diff --git a/proofs/proof.ml b/proofs/proof.ml index a4e556c5..012a4dc1 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -323,7 +323,7 @@ let rec rollback pr = let transaction pr t = init_transaction pr; try t (); commit pr - with e -> rollback pr; raise e + with reraise -> rollback pr; raise reraise (* Focus command (focuses on the [i]th subgoal) *) @@ -429,9 +429,9 @@ let run_tactic env tac pr = let tacticced_proofview = Proofview.apply env tac sp in pr.state <- { pr.state with proofview = tacticced_proofview }; push_undo starting_point pr - with e -> + with reraise -> restore_state starting_point pr; - raise e + raise reraise (*** Commands ***) @@ -476,7 +476,7 @@ module V82 = struct let new_proofview = Proofview.V82.instantiate_evar n com sp in pr.state <- { pr.state with proofview = new_proofview }; push_undo starting_point pr - with e -> + with reraise -> restore_state starting_point pr; - raise e + raise reraise end diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 74e40e3b..d299a520 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -320,10 +320,12 @@ let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step -> (* takes a tactic which can raise exception and makes it pure by *failing* on with these exceptions. Does not catch anomalies. *) let purify t = - let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step - with Util.Anomaly _ as e -> raise e - | e -> sk (Util.Inr e) fk step - } + let t' env = + { go = fun sk fk step -> + try (t env).go (fun x -> sk (Util.Inl x)) fk step + with Util.Anomaly _ as e -> raise e + | e when Errors.noncritical e -> sk (Util.Inr e) fk step + } in tclBIND t' begin function | Util.Inl x -> tclUNIT x diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 37c63644..21b43212 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -255,7 +255,7 @@ let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e -> catch_failerror e; t2 g + | e when Errors.noncritical e -> catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -267,7 +267,7 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) - with e -> catch_failerror e; None + with e when Errors.noncritical e -> catch_failerror e; None with | None -> t2else gls | Some sgl -> @@ -298,7 +298,7 @@ let ite_gen tcal tac_if continue tac_else gl= try tcal tac_if0 continue gl with (* Breakpoint *) - | e -> catch_failerror e; tac_else0 e gl + | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) @@ -352,7 +352,7 @@ let tclTIMEOUT n t g = | TacTimeout | Loc.Exc_located(_,TacTimeout) -> restore_timeout (); errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!") - | e -> restore_timeout (); raise e + | reraise -> restore_timeout (); raise reraise (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index b56cb844..27ab990c 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -140,11 +140,11 @@ let debug_prompt lev g tac f = else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in (* What to execute *) try f newlevel - with e -> + with reraise -> skip:=0; skipped:=0; - if Logic.catchable_exception e then - ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e); - raise e + if Logic.catchable_exception reraise then + ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise); + raise reraise (* Prints a constr *) let db_constr debug env c = diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 5bc77457..b75984e3 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -45,8 +45,7 @@ let camlp4topobjs = [ "Camlp4Top.cmo"; "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo"; "Camlp4Parsers/Camlp4OCamlParser.cmo"; - "Camlp4Parsers/Camlp4GrammarParser.cmo"; - "q_util.cmo"; "q_coqast.cmo" ] + "Camlp4Parsers/Camlp4GrammarParser.cmo" ] let topobjs = camlp4topobjs let gramobjs = [] @@ -257,8 +256,8 @@ let create_tmp_main_file modules = output_string oc "Coqtop.start();;\n"; close_out oc; main_name - with e -> - clean main_name; raise e + with reraise -> + clean main_name; raise reraise (* main part *) let main () = @@ -311,10 +310,10 @@ let main () = clean main_file; (* command gives the exit code in HSB, and signal in LSB !!! *) if retcode > 255 then retcode lsr 8 else retcode - with e -> - clean main_file; raise e + with reraise -> + clean main_file; raise reraise let retcode = - try Printexc.print main () with _ -> 1 + try Printexc.print main () with any -> 1 let _ = exit retcode diff --git a/tactics/auto.ml b/tactics/auto.ml index f7d63dcd..44fea151 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -829,7 +829,8 @@ let prepare_hint env (sigma,c) = let path_of_constr_expr c = match c with - | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny) + | Topconstr.CRef r -> + (try PathHints [global r] with e when Errors.noncritical e -> PathAny) | _ -> PathAny let interp_hints h = @@ -1170,9 +1171,9 @@ let tclLOG (dbg,depth,trace) pp tac = let out = tac gl in msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); out - with e -> + with reraise -> msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); - raise e + raise reraise end | Info -> (* For "info (trivial/auto)", we store a log trace *) @@ -1181,9 +1182,9 @@ let tclLOG (dbg,depth,trace) pp tac = let out = tac gl in trace := (depth, Some pp) :: !trace; out - with e -> + with reraise -> trace := (depth, None) :: !trace; - raise e + raise reraise end (** For info, from the linear trace information, we reconstitute the part diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 039f022d..8e1d7cbf 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -208,8 +208,14 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl = (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = - let base = try find_base rbase with _ -> HintDN.empty in - let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in + let base = + try find_base rbase + with e when Errors.noncritical e -> HintDN.empty + in + let max = + try fst (Util.list_last (HintDN.find_all base)) + with e when Errors.noncritical e -> 0 + in let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab @@ -248,7 +254,7 @@ let evd_convertible env evd x y = try ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true (* try ignore(Evarconv.the_conv_x env x y evd); true *) - with _ -> false + with e when Errors.noncritical e -> false let decompose_applied_relation metas env sigma c ctype left2right = let find_rel ty = diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index cf4a267f..d05ae680 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -685,7 +685,7 @@ let resolve_typeclass_evars debug m env evd filter split fail = let evd = try Evarconv.consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env evd - with _ -> evd + with e when Errors.noncritical e -> evd in resolve_all_evars debug m env (initial_select_evars filter) evd split fail @@ -776,7 +776,10 @@ END let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl = try - let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in + let dbs = list_map_filter + (fun db -> try Some (Auto.searchtable_map db) + with e when Errors.noncritical e -> None) dbs + in let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 68dd5dba..6981a733 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -205,7 +205,8 @@ module SearchProblem = struct (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls,pptac) :: aux tacl - with e -> Refiner.catch_failerror e; aux tacl + with e when Errors.noncritical e -> + Refiner.catch_failerror e; aux tacl in aux l (* Ordering of states is lexicographic on depth (greatest first) then diff --git a/tactics/equality.ml b/tactics/equality.ml index a352355b..1c5e4b2f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -334,7 +334,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac try rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl - with e -> (* Try to see if there's an equality hidden *) + with e when Errors.noncritical e -> + (* Try to see if there's an equality hidden *) let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) match match_with_equality_type t' with @@ -1156,7 +1157,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = ] (* not a dep eq or no decidable type found *) ) else (raise Not_dep_pair) - ) with _ -> + ) with e when Errors.noncritical e -> inject_at_positions env sigma u eq_clause posns (fun _ -> intros_pattern no_move ipats) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f5fcb736..f6ecb47c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -606,7 +606,7 @@ let hResolve_auto id c t gl = hResolve id c n t gl with | UserError _ as e -> raise e - | _ -> resolve_auto (n+1) + | e when Errors.noncritical e -> resolve_auto (n+1) in resolve_auto 1 diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 47e3b7ca..c6f32ce2 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -64,9 +64,12 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) (* Test dependencies *) +(* NB: we consider also the let-in case in the following function, + since they may appear in types of inductive constructors (see #2629) *) + let rec has_nodep_prod_after n c = match kind_of_term c with - | Prod (_,_,b) -> + | Prod (_,_,b) | LetIn (_,_,_,b) -> ( n>0 || not (dependent (mkRel 1) b)) && (has_nodep_prod_after (n-1) b) | _ -> true @@ -355,7 +358,10 @@ let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ] let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ] let match_eq eqn eq_pat = - let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in + let pat = + try Lazy.force eq_pat + with e when Errors.noncritical e -> raise PatternMatchingFailure + in match matches pat eqn with | [(m1,t);(m2,x);(m3,y)] -> assert (m1 = meta1 & m2 = meta2 & m3 = meta3); diff --git a/tactics/inv.ml b/tactics/inv.ml index b7f6addc..e4b3bdb1 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -497,7 +497,7 @@ let wrap_inv_error id = function (* The most general inversion tactic *) let inversion inv_kind status names id gls = try (raw_inversion inv_kind id status names) gls - with e -> wrap_inv_error id e + with e when Errors.noncritical e -> wrap_inv_error id e (* Specializing it... *) @@ -540,7 +540,7 @@ let invIn k names ids id gls = inversion (false,k) NoDep names id; intros_replace_ids]) gls - with e -> wrap_inv_error id e + with e when Errors.noncritical e -> wrap_inv_error id e let invIn_gen k names idl = try_intros_until (invIn k names idl) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index b90a911a..98885af8 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -121,7 +121,7 @@ let is_applied_rewrite_relation env sigma rels t = let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in let _ = Typeclasses.resolve_one_typeclass env' evd inst in Some (it_mkProd_or_LetIn t rels) - with _ -> None) + with e when Errors.noncritical e -> None) | _ -> None let _ = @@ -145,11 +145,14 @@ let build_signature evars env m (cstrs : (types * types option) option list) new_cstr_evar evars env (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in - let mk_relty evars env ty obj = + let mk_relty evars newenv ty obj = match obj with | None | Some (_, None) -> let relty = mk_relation ty in - new_evar evars env relty + if closed0 ty then + let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in + new_evar evars env' relty + else new_evar evars newenv relty | Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = @@ -227,7 +230,7 @@ let cstrevars evars = snd evars let evd_convertible env evd x y = try ignore(Evarconv.the_conv_x env x y evd); true - with _ -> false + with e when Errors.noncritical e -> false let rec decompose_app_rel env evd t = match kind_of_term t with @@ -493,7 +496,7 @@ let rec apply_pointwise rel = function | [] -> rel let pointwise_or_dep_relation n t car rel = - if noccurn 1 car then + if noccurn 1 car && noccurn 1 rel then mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |]) else mkApp (Lazy.force forall_relation, @@ -1048,7 +1051,8 @@ module Strategies = let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1056,7 +1060,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None let fold_glob c : strategy = fun env avoid t ty cstr evars -> @@ -1064,7 +1068,8 @@ module Strategies = let sigma, c = Pretyping.Default.understand_tcc (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1072,7 +1077,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None end @@ -1977,7 +1982,7 @@ let setoid_proof gl ty fn fallback = let evm = project gl in let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in fn env evm car rel gl - with e -> + with e when Errors.noncritical e -> try fallback gl with Hipattern.NoEquationFound -> match e with diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3ff0cf93..7479ee9a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -50,7 +50,7 @@ open Compat open Evd let safe_msgnl s = - try msgnl s with e -> + try msgnl s with e when Errors.noncritical e -> msgnl (str "bug in the debugger: " ++ str "an exception is raised while printing debug information") @@ -92,7 +92,7 @@ let catch_error call_trace tac g = if call_trace = [] then tac g else try tac g with | LtacLocated _ as e -> raise e | Loc.Exc_located (_,LtacLocated _) as e -> raise e - | e -> + | e when Errors.noncritical e -> let (nrep,loc',c),tail = list_sep_last call_trace in let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in if tail = [] then @@ -569,13 +569,13 @@ let dump_glob_red_expr = function try Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) - with _ -> ()) occs + with e when Errors.noncritical e -> ()) occs | Cbv grf | Lazy grf -> List.iter (fun r -> try Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) - with _ -> ()) grf.rConst + with e when Errors.noncritical e -> ()) grf.rConst | _ -> () let intern_red_expr ist = function @@ -1412,19 +1412,20 @@ let interp_may_eval f ist gl = function | ConstrTerm c -> try f ist gl c - with e -> - debugging_exception_step ist false e (fun () -> + with reraise -> + debugging_exception_step ist false reraise (fun () -> str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c)); - raise e + raise reraise (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist gl c = let (sigma,csr) = try interp_may_eval pf_interp_constr ist gl c - with e -> - debugging_exception_step ist false e (fun () -> str"evaluation of term"); - raise e + with reraise -> + debugging_exception_step ist false reraise (fun () -> + str"evaluation of term"); + raise reraise in begin db_constr ist.debug (pf_env gl) csr; @@ -1762,10 +1763,7 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) let pack_sigma (sigma,c) = {it=c;sigma=sigma} let extend_gl_hyps { it=gl ; sigma=sigma } sign = - let hyps = Goal.V82.hyps sigma gl in - let new_hyps = List.fold_right Environ.push_named_context_val sign hyps in - (* spiwack: (2010/01/13) if a bug was reintroduced in [change] in is probably here *) - Goal.V82.new_goal_with sigma gl new_hyps + Goal.V82.new_goal_with sigma gl sign (* Interprets an l-tac expression into a value *) let rec val_interp ist gl (tac:glob_tactic_expr) = @@ -1925,9 +1923,11 @@ and interp_app loc ist gl fv largs = try catch_error trace (val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body - with e -> - debugging_exception_step ist false e (fun () -> str "evaluation"); - raise e in + with reraise -> + debugging_exception_step ist false reraise + (fun () -> str "evaluation"); + raise reraise + in let gl = { gl with sigma=sigma } in debugging_step ist (fun () -> @@ -2212,19 +2212,20 @@ and interp_match ist g lz constr lmr = (try let lmatch = try extended_matches c csr - with e -> - debugging_exception_step ist false e (fun () -> + with reraise -> + debugging_exception_step ist false reraise (fun () -> str "matching with pattern" ++ fnl () ++ pr_constr_pattern_env (pf_env g) c); - raise e in + raise reraise + in try let lfun = extend_values_with_bindings lmatch ist.lfun in eval_with_fail { ist with lfun=lfun } lz g mt - with e -> - debugging_exception_step ist false e (fun () -> + with reraise -> + debugging_exception_step ist false reraise (fun () -> str "rule body for pattern" ++ pr_constr_pattern_env (pf_env g) c); - raise e + raise reraise with e when is_match_catchable e -> debugging_step ist (fun () -> str "switching to the next rule"); apply_match ist sigma csr tl) @@ -2236,15 +2237,16 @@ and interp_match ist g lz constr lmr = errorlabstrm "Tacinterp.apply_match" (str "No matching clauses for match.") in let (sigma,csr) = - try interp_ltac_constr ist g constr with e -> - debugging_exception_step ist true e + try interp_ltac_constr ist g constr with reraise -> + debugging_exception_step ist true reraise (fun () -> str "evaluation of the matched expression"); - raise e in + raise reraise in let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in let res = - try apply_match ist sigma csr ilr with e -> - debugging_exception_step ist true e (fun () -> str "match expression"); - raise e in + try apply_match ist sigma csr ilr with reraise -> + debugging_exception_step ist true reraise + (fun () -> str "match expression"); + raise reraise in debugging_step ist (fun () -> str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res)); res @@ -2404,6 +2406,7 @@ and interp_atomic ist gl tac = (h_generalize_dep c_interp) | TacLetTac (na,c,clp,b,eqpat) -> let clp = interp_clause ist gl clp in + let eqpat = Option.map (interp_intro_pattern ist gl) eqpat in if clp = nowhere then (* We try to fully-typecheck the term *) let (sigma,c_interp) = pf_interp_constr ist gl c in @@ -3180,7 +3183,8 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) let tacticIn t = globTacticIn (fun ist -> try glob_tactic (t ist) - with e -> anomalylabstrm "tacticIn" + with e when Errors.noncritical e -> + anomalylabstrm "tacticIn" (str "Incorrect tactic expression. Received exception is:" ++ Errors.print e)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 12292196..ac00a73d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1018,7 +1018,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl = let thm = nf_betaiota gl.sigma (pf_type_of gl d) in let rec aux clause = try progress_with_clause flags innerclause clause - with err -> + with err when Errors.noncritical err -> try aux (clenv_push_prod clause) with NotExtensibleClause -> raise err in aux (make_clenv_binding gl (d,thm) lbind) @@ -1708,7 +1708,7 @@ let make_pattern_test env sigma0 (sigma,c) = let flags = default_matching_flags sigma0 in let matching_fun t = try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t) - with _ -> raise NotUnifiable in + with e when Errors.noncritical e -> raise NotUnifiable in let merge_fun c1 c2 = match c1, c2 with | Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) -> @@ -2554,7 +2554,10 @@ let specialize_eqs id gl = let specialize_eqs id gl = - if try ignore(clear [id] gl); false with _ -> true then + if + (try ignore(clear [id] gl); false + with e when Errors.noncritical e -> true) + then tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl else specialize_eqs id gl @@ -2716,7 +2719,8 @@ let compute_elim_sig ?elimc elimt = | Some ( _,None,ind) -> let indhd,indargs = decompose_app ind in try {!res with indref = Some (global_of_constr indhd) } - with _ -> error "Cannot find the inductive type of the inductive scheme.";; + with e when Errors.noncritical e -> + error "Cannot find the inductive type of the inductive scheme.";; let compute_scheme_signature scheme names_info ind_type_guess = let f,l = decompose_app scheme.concl in @@ -3551,4 +3555,5 @@ let unify ?(state=full_transparent_state) x y gl = in let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y in tclEVARS evd gl - with _ -> tclFAIL 0 (str"Not unifiable") gl + with e when Errors.noncritical e -> + tclFAIL 0 (str"Not unifiable") gl diff --git a/test-suite/bugs/closed/2955.v b/test-suite/bugs/closed/2955.v new file mode 100644 index 00000000..45e24b5f --- /dev/null +++ b/test-suite/bugs/closed/2955.v @@ -0,0 +1,52 @@ +Require Import Coq.Arith.Arith. + +Module A. + + Fixpoint foo (n:nat) := + match n with + | 0 => 0 + | S n => bar n + end + + with bar (n:nat) := + match n with + | 0 => 0 + | S n => foo n + end. + + Lemma using_foo: + forall (n:nat), foo n = 0 /\ bar n = 0. + Proof. + induction n ; split ; auto ; + destruct IHn ; auto. + Qed. + +End A. + + +Module B. + + Module A := A. + Import A. + +End B. + +Module E. + + Module B := B. + Import B.A. + + (* Bug 1 *) + Lemma test_1: + forall (n:nat), foo n = 0. + Proof. + intros ; destruct n. + reflexivity. + specialize (A.using_foo (S n)) ; intros. + simpl in H. + simpl. + destruct H. + assumption. + Qed. + +End E. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2629.v b/test-suite/bugs/closed/shouldsucceed/2629.v new file mode 100644 index 00000000..759cd3dd --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2629.v @@ -0,0 +1,22 @@ +Class Join (t: Type) : Type := mkJoin {join: t -> t -> t -> Prop}. + +Class sepalg (t: Type) {JOIN: Join t} : Type := + SepAlg { + join_eq: forall {x y z z'}, join x y z -> join x y z' -> z = z'; + join_assoc: forall {a b c d e}, join a b d -> join d c e -> + {f : t & join b c f /\ join a f e}; + join_com: forall {a b c}, join a b c -> join b a c; + join_canc: forall {a1 a2 b c}, join a1 b c -> join a2 b c -> a1=a2; + + unit_for : t -> t -> Prop := fun e a => join e a a; + join_ex_units: forall a, {e : t & unit_for e a} +}. + +Definition joins {A} `{Join A} (a b : A) : Prop := + exists c, join a b c. + +Lemma join_joins {A} `{sepalg A}: forall {a b c}, + join a b c -> joins a b. +Proof. + firstorder. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v new file mode 100644 index 00000000..74c8fa34 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2668.v @@ -0,0 +1,6 @@ +Require Import MSetPositive. +Require Import MSetProperties. + +Module Pos := MSetPositive.PositiveSet. +Module PPPP := MSetProperties.WPropertiesOn(Pos). +Print Module PPPP. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2734.v b/test-suite/bugs/closed/shouldsucceed/2734.v new file mode 100644 index 00000000..826361be --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2734.v @@ -0,0 +1,15 @@ +Require Import Arith List. +Require Import OrderedTypeEx. + +Module Adr. + Include Nat_as_OT. + Definition nat2t (i: nat) : t := i. +End Adr. + +Inductive expr := Const: Adr.t -> expr. + +Inductive control := Go: expr -> control. + +Definition program := (Adr.t * (control))%type. + +Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ). \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2750.v b/test-suite/bugs/closed/shouldsucceed/2750.v new file mode 100644 index 00000000..fc580f10 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2750.v @@ -0,0 +1,23 @@ + +Module Type ModWithRecord. + + Record foo : Type := + { A : nat + ; B : nat + }. +End ModWithRecord. + +Module Test_ModWithRecord (M : ModWithRecord). + + Definition test1 : M.foo := + {| M.A := 0 + ; M.B := 2 + |}. + + Module B := M. + + Definition test2 : M.foo := + {| M.A := 0 + ; M.B := 2 + |}. +End Test_ModWithRecord. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/shouldsucceed/2928.v new file mode 100644 index 00000000..21e92ae2 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2928.v @@ -0,0 +1,11 @@ +Class Equiv A := equiv: A -> A -> Prop. +Infix "=" := equiv : type_scope. + +Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z. + +Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }. + +Class SemiLattice A op `{Equiv A} := + { semilattice_sg :>> SemiGroup A op + ; redundant : Associative op + }. diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v new file mode 100644 index 00000000..15598352 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2983.v @@ -0,0 +1,8 @@ +Module Type ModA. +End ModA. +Module Type ModB(A : ModA). +End ModB. +Module Foo(A : ModA)(B : ModB A). +End Foo. + +Print Module Foo. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v new file mode 100644 index 00000000..ba3acd08 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2995.v @@ -0,0 +1,9 @@ +Module Type Interface. + Parameter error: nat. +End Interface. + +Module Implementation <: Interface. + Definition t := bool. + Definition error: t := false. +Fail End Implementation. +(* A UserError here is expected, not an uncaught Not_found *) \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v new file mode 100644 index 00000000..27de34ed --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/3000.v @@ -0,0 +1,2 @@ +Inductive t (t':Type) : Type := A | B. +Definition d := match t with _ => 1 end. (* used to fail on list_chop *) diff --git a/test-suite/bugs/closed/shouldsucceed/3004.v b/test-suite/bugs/closed/shouldsucceed/3004.v new file mode 100644 index 00000000..896b1958 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/3004.v @@ -0,0 +1,7 @@ +Set Implicit Arguments. +Unset Strict Implicit. +Parameter (M : nat -> Type). +Parameter (mp : forall (T1 T2 : Type) (f : T1 -> T2), list T1 -> list T2). + +Definition foo (s : list {n : nat & M n}) := + let exT := existT in mp (fun x => projT1 x) s. diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v new file mode 100644 index 00000000..3f3a979a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/3008.v @@ -0,0 +1,29 @@ +Module Type Intf1. +Parameter T : Type. +Inductive a := A. +End Intf1. + +Module Impl1 <: Intf1. +Definition T := unit. +Inductive a := A. +End Impl1. + +Module Type Intf2 + (Impl1 : Intf1). +Parameter x : Impl1.A=Impl1.A -> Impl1.T. +End Intf2. + +Module Type Intf3 + (Impl1 : Intf1) + (Impl2 : Intf2(Impl1)). +End Intf3. + +Fail Module Toto + (Impl1' : Intf1) + (Impl2 : Intf2(Impl1')) + (Impl3 : Intf3(Impl1)(Impl2)). +(* A UserError is expected here, not an uncaught Not_found *) + +(* NB : the Inductive above and the A=A weren't in the initial test, + they are here only to force an access to the environment + (cf [Printer.qualid_of_global]) and check that this env is ok. *) \ No newline at end of file diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index bca3b361..4f8de1dc 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -4,3 +4,7 @@ fun e : option L => match e with | None => None end : option L -> option L +fun n : nat => let x := A n in ?12 ?15:T n + : forall n : nat, T n +fun n : nat => ?20 ?23:T n + : forall n : nat, T n diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 968ea71a..2b564f48 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -12,3 +12,15 @@ Definition P (e:option L) := end. Print P. + +(* Check that the heuristic to solve constraints is not artificially + dependent on the presence of a let-in, and in particular that the + second [_] below is not inferred to be n, as if obtained by + first-order unification with [T n] of the conclusion [T _] of the + type of the first [_]. *) + +(* Note: exact numbers of evars are not important... *) + +Inductive T (n:nat) : Type := A : T n. +Check fun n (x:=A n:T n) => _ _ : T n. +Check fun n => _ _ : T n. diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v index 5f8ed03d..0befe054 100644 --- a/test-suite/success/remember.v +++ b/test-suite/success/remember.v @@ -6,3 +6,11 @@ Fail remember nat as X. Fail remember nat as X in H. (* This line used to succeed in 8.3 *) Fail remember nat as X. Abort. + +(* Testing Ltac interpretation of remember (was not working up to r16181) *) + +Goal (1 + 2 + 3 = 6). +let name := fresh "fresh" in +remember (1 + 2) as x eqn:name. +rewrite fresh. +Abort. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 5582438b..3dae9c70 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -646,4 +646,4 @@ End NZOrderProp. Module NZOrderedType (NZ : NZDecOrdSig') <: DecidableTypeFull <: OrderedTypeFull - := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec. + := NZ <+ NZBaseProp <+ NZOrderProp NZ <+ Compare2EqBool <+ HasEqBool2Dec. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 3690b924..b9ab68ec 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -111,7 +111,7 @@ let mkFullInd ind n = let check_bool_is_defined () = try let _ = Global.type_of_global Coqlib.glob_bool in () - with _ -> raise (UndefinedCst "bool") + with e when Errors.noncritical e -> raise (UndefinedCst "bool") let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -304,8 +304,9 @@ let destruct_ind c = try let u,v = destApp c in let indc = destInd u in indc,v - with _-> let indc = destInd c in - indc,[||] + with e when Errors.noncritical e -> + let indc = destInd c in + indc,[||] (* In the following, avoid is the list of names to avoid. @@ -329,8 +330,9 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = else error ("Var "^(string_of_id s)^" seems unknown.") ) in mkVar (find 1) - with _ -> (* if this happen then the args have to be already declared as a - Parameter*) + with e when Errors.noncritical e -> + (* if this happen then the args have to be already declared as a + Parameter*) ( let mp,dir,lbl = repr_con (destConst v) in mkConst (make_con mp dir (mk_label ( @@ -376,8 +378,9 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = else error ("Var "^(string_of_id s)^" seems unknown.") ) in mkVar (find 1) - with _ -> (* if this happen then the args have to be already declared as a - Parameter*) + with e when Errors.noncritical e -> + (* if this happen then the args have to be already declared as a + Parameter*) ( let mp,dir,lbl = repr_con (destConst v) in mkConst (make_con mp dir (mk_label ( @@ -394,7 +397,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = else ( let u,v = try destruct_ind tt1 (* trick so that the good sequence is returned*) - with _ -> ind,[||] + with e when Errors.noncritical e -> ind,[||] in if u = ind then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2) else ( @@ -427,17 +430,19 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = | ([],[]) -> [] | _ -> error "Both side of the equality must have the same arity." in - let (ind1,ca1) = try destApp lft with - _ -> error "replace failed." - and (ind2,ca2) = try destApp rgt with - _ -> error "replace failed." + let (ind1,ca1) = + try destApp lft with e when Errors.noncritical e -> error "replace failed." + and (ind2,ca2) = + try destApp rgt with e when Errors.noncritical e -> error "replace failed." in - let (sp1,i1) = try destInd ind1 with - _ -> (try fst (destConstruct ind1) with _ -> - error "The expected type is an inductive one.") - and (sp2,i2) = try destInd ind2 with - _ -> (try fst (destConstruct ind2) with _ -> - error "The expected type is an inductive one.") + let (sp1,i1) = + try destInd ind1 with e when Errors.noncritical e -> + try fst (destConstruct ind1) with e when Errors.noncritical e -> + error "The expected type is an inductive one." + and (sp2,i2) = + try destInd ind2 with e when Errors.noncritical e -> + try fst (destConstruct ind2) with e when Errors.noncritical e -> + error "The expected type is an inductive one." in if (sp1 <> sp2) || (i1 <> i2) then (error "Eq should be on the same type") @@ -714,7 +719,8 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind (* Decidable equality *) let check_not_is_defined () = - try ignore (Coqlib.build_coq_not ()) with _ -> raise (UndefinedCst "not") + try ignore (Coqlib.build_coq_not ()) + with e when Errors.noncritical e -> raise (UndefinedCst "not") (* {n=m}+{n<>m} part *) let compute_dec_goal ind lnamesparrec nparrec = diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 10709abc..f43fc505 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -204,7 +204,8 @@ let declare_class_instance gr ctx params = (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst)); new_instance_message ident typ def - with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e) + with e when Errors.noncritical e -> + msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e) let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t; match kind_of_term t with diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 912d694e..f444fc2d 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -96,7 +96,9 @@ let mark_command ast = Stack.push { label = Lib.current_command_label (); nproofs = List.length (Pfedit.get_all_proof_names ()); - prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None); + prfname = + (try Some (Pfedit.get_current_proof_name ()) + with Proof_global.NoCurrentProof -> None); prfdepth = max 0 (Pfedit.current_proof_depth ()); reachable = true; ngoals = get_ngoals (); diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 6914b8f0..de4d1ab1 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -37,7 +37,10 @@ let set_typeclass_transparency c local b = let _ = Typeclasses.register_add_instance_hint (fun inst local pri -> - let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in + let path = + try Auto.PathHints [global_of_constr inst] + with e when Errors.noncritical e -> Auto.PathAny + in Flags.silently (fun () -> Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry @@ -300,8 +303,10 @@ let context l = let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; - let ctx = try named_of_rel_context fullctx with _ -> - error "Anonymous variables not allowed in contexts." + let ctx = + try named_of_rel_context fullctx + with e when Errors.noncritical e -> + error "Anonymous variables not allowed in contexts." in let fn (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 66a9516a..8f954573 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -46,9 +46,9 @@ let load_rcfile() = mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ " found. Skipping rcfile loading.")) *) - with e -> + with reraise -> (msgnl (str"Load of rcfile failed."); - raise e) + raise reraise) else Flags.if_verbose msgnl (str"Skipping rcfile loading.") diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index df388d1d..adbdb31b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -24,7 +24,8 @@ let get_version_date () = let ver = input_line ch in let rev = input_line ch in (ver,rev) - with _ -> (Coq_config.version,Coq_config.date) + with e when Errors.noncritical e -> + (Coq_config.version,Coq_config.date) let print_header () = let (ver,rev) = (get_version_date ()) in @@ -310,7 +311,7 @@ let parse_args arglist = with Stream.Failure -> msgnl (Errors.print e); exit 1 end - | e -> begin msgnl (Errors.print e); exit 1 end + | any -> begin msgnl (Errors.print any); exit 1 end let init arglist = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) @@ -344,10 +345,10 @@ let init arglist = load_vernacular (); compile_files (); outputstate () - with e -> + with any -> flush_all(); if not !batch_mode then message "Error during initialization:"; - msgnl (Toplevel.print_toplevel_error e); + msgnl (Toplevel.print_toplevel_error any); exit 1 end; if !batch_mode then diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e7b5a0f2..f550df16 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -28,6 +28,8 @@ open Logic open Printer open Glob_term open Evd +open Libnames +open Declarations let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) @@ -307,7 +309,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = let fixenv = make_all_name_different fixenv in let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." - with _ -> mt ()) + with e when Errors.noncritical e -> mt ()) let explain_ill_typed_rec_body env sigma i names vdefj vargs = let vdefj = jv_nf_evar sigma vdefj in @@ -542,8 +544,11 @@ let explain_not_match_error = function str "types given to " ++ str (string_of_id id) ++ str " differ" | NotConvertibleBodyField -> str "the body of definitions differs" - | NotConvertibleTypeField -> - str "types differ" + | NotConvertibleTypeField (env, typ1, typ2) -> + str "expected type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++ + str "but found type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ1) | NotSameConstructorNamesField -> str "constructor names differ" | NotSameInductiveNameInBlockField -> diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 28f97dc8..6937eeb8 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -89,8 +89,8 @@ let abstract_eval_call handler c = | Quit -> Obj.magic (handler.quit () : unit) | About -> Obj.magic (handler.about () : coq_info) in Good res - with e -> - let (l, str) = handler.handle_exn e in + with any -> + let (l, str) = handler.handle_exn any in Fail (l,str) (** * XML data marshalling *) @@ -275,7 +275,7 @@ let to_value f = function let loc_s = int_of_string (List.assoc "loc_s" attrs) in let loc_e = int_of_string (List.assoc "loc_e" attrs) in Some (loc_s, loc_e) - with _ -> None + with e when e <> Sys.Break -> None in let msg = raw_string l in Fail (loc, msg) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index d67b272e..6e9a0ee0 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -237,7 +237,7 @@ let status () = in let proof = try Some (Names.string_of_id (Proof_global.get_current_proof_name ())) - with _ -> None + with Proof_global.NoCurrentProof -> None in let allproofs = let l = Proof_global.get_all_proof_names () in @@ -259,7 +259,8 @@ let search flags = | (Interface.Name_Pattern s, b) :: l -> let regexp = try Str.regexp s - with _ -> Util.error ("Invalid regexp: " ^ s) + with e when Errors.noncritical e -> + Util.error ("Invalid regexp: " ^ s) in extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l | (Interface.Type_Pattern s, b) :: l -> @@ -454,12 +455,12 @@ let loop () = Xml_utils.print_xml !orig_stdout xml_answer; flush !orig_stdout done - with e -> - let msg = Printexc.to_string e in + with any -> + let msg = Printexc.to_string any in let r = "Fatal exception in coqtop:\n" ^ msg in pr_debug ("==> " ^ r); (try Xml_utils.print_xml !orig_stdout (fail r); flush !orig_stdout - with _ -> ()); + with any -> ()); exit 1 diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 9f1a0218..77cfa6fa 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -86,8 +86,9 @@ let scheme_object_table = (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) let declare_scheme_object s aux f = - (try check_ident ("ind"^s) with _ -> - error ("Illegal induction scheme suffix: "^s)); + (try check_ident ("ind"^s) + with e when Errors.noncritical e -> + error ("Illegal induction scheme suffix: "^s)); let key = if aux = "" then s else aux in try let _ = Hashtbl.find scheme_object_table key in diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index fa6885af..e30404e1 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -159,7 +159,7 @@ let try_declare_scheme what f internal names kn = (strbrk "Required constant " ++ str s ++ str " undefined.") | AlreadyDeclared msg -> alarm what internal (msg ++ str ".") - | _ -> + | e when Errors.noncritical e -> alarm what internal (str "Unknown exception during scheme creation.") @@ -245,7 +245,8 @@ let try_declare_eq_decidability kn = let declare_eq_decidability = declare_eq_decidability_scheme_with [] -let ignore_error f x = try ignore (f x) with _ -> () +let ignore_error f x = + try ignore (f x) with e when Errors.noncritical e -> () let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin @@ -266,7 +267,7 @@ let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true - with _ -> false + with e when Errors.noncritical e -> false then ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index d6ab44c6..30f07fed 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -229,23 +229,32 @@ let get_proof opacity = id,{const with const_entry_opaque = opacity},do_guard,persistence,hook let save_named opacity = - let id,const,do_guard,persistence,hook = get_proof opacity in - save id const do_guard persistence hook + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + let id,const,do_guard,persistence,hook = get_proof opacity in + save id const do_guard persistence hook + end let check_anonymity id save_ident = if atompart_of_id id <> string_of_id (default_thm_id) then error "This command can only be used for unnamed theorem." let save_anonymous opacity save_ident = - let id,const,do_guard,persistence,hook = get_proof opacity in - check_anonymity id save_ident; - save save_ident const do_guard persistence hook + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + let id,const,do_guard,persistence,hook = get_proof opacity in + check_anonymity id save_ident; + save save_ident const do_guard persistence hook + end let save_anonymous_with_strength kind opacity save_ident = - let id,const,do_guard,_,hook = get_proof opacity in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save save_ident const do_guard (Global, Proof kind) hook + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + let id,const,do_guard,_,hook = get_proof opacity in + check_anonymity id save_ident; + (* we consider that non opaque behaves as local for discharge *) + save save_ident const do_guard (Global, Proof kind) hook + end (* Starting a goal *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 775a3af4..006dc5ec 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -237,7 +237,7 @@ let parse_format (loc,str) = | _ -> error "Box closed without being opened in format." else error "Empty format." - with e -> + with e when Errors.noncritical e -> Loc.raise loc e (***********************) @@ -277,6 +277,9 @@ let split_notation_string str = let out_nt = function NonTerminal x -> x | _ -> assert false +let msg_expected_form_of_recursive_notation = + "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"." + let rec find_pattern nt xl = function | Break n as x :: l, Break n' :: l' when n=n' -> find_pattern nt (x::xl) (l,l') @@ -289,13 +292,14 @@ let rec find_pattern nt xl = function | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | _, [] -> - error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") + error msg_expected_form_of_recursive_notation | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> anomaly "Only Terminal or Break expected on left, non-SProdList on right" let rec interp_list_parser hd = function | [] -> [], List.rev hd | NonTerminal id :: tl when id = ldots_var -> + if hd = [] then error msg_expected_form_of_recursive_notation; let hd = List.rev hd in let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in let xyl,tl'' = interp_list_parser [] tl' in @@ -337,7 +341,8 @@ let rec raw_analyze_notation_tokens = function let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with | ([Terminal "-"; Terminal x] | [Terminal x]) -> - (try let _ = Bigint.of_string x in true with _ -> false) + (try let _ = Bigint.of_string x in true + with e when Errors.noncritical e -> false) | _ -> false @@ -995,7 +1000,7 @@ let inNotation : notation_obj -> obj = let with_lib_stk_protection f x = let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a - with e -> Lib.unfreeze fs; raise e + with reraise -> Lib.unfreeze fs; raise reraise let with_syntax_protection f x = with_lib_stk_protection diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 2059ca60..f08308d3 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -92,8 +92,9 @@ let dir_ml_load s = (try t.load_obj s with | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u - | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ - str s ++ str" to Coq code.")) + | e when Errors.noncritical e -> + errorlabstrm "Mltop.load_object" + (str"Cannot link ml-object " ++ str s ++ str" to Coq code.")) (* TO DO: .cma loading without toplevel *) | WithoutTop -> IFDEF HasDynlink THEN @@ -142,7 +143,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.id_of_string d - with _ -> + with e when Errors.noncritical e -> if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); flush_all (); @@ -269,9 +270,9 @@ let if_verbose_load verb f name fname = try f name fname; msgnl (str (info^" done]")); - with e -> + with reraise -> msgnl (str (info^" failed]")); - raise e + raise reraise (** Load a module for the first time (i.e. dynlink it) or simulate its reload (i.e. doing nothing except maybe diff --git a/toplevel/search.ml b/toplevel/search.ml index 3e182689..19d696a1 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -137,7 +137,7 @@ let pattern_filter pat _ a c = try try is_matching pat (head c) - with _ -> + with e when Errors.noncritical e -> is_matching pat (head (Typing.type_of (Global.env()) Evd.empty c)) with UserError _ -> diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index d5321623..cc659e36 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -180,7 +180,7 @@ let print_location_in_file s inlibrary fname loc = str", line " ++ int line ++ str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () - with e -> + with e when Errors.noncritical e -> (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) @@ -208,7 +208,7 @@ let valid_buffer_loc ib dloc loc = let make_prompt () = try (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < " - with _ -> + with Proof_global.NoCurrentProof -> "Coq < " (*let build_pending_list l = @@ -340,7 +340,7 @@ let process_error = function discard_to_dot (); e with | End_of_input -> End_of_input - | de -> if is_pervasive_exn de then de else e + | any -> if is_pervasive_exn any then any else e (* do_vernac reads and executes a toplevel phrase, and print error messages when an exception is raised, except for the following: @@ -354,8 +354,8 @@ let do_vernac () = begin try raw_do_vernac top_buffer.tokens - with e -> - msgnl (print_toplevel_error (process_error e)) + with any -> + msgnl (print_toplevel_error (process_error any)) end; flush_all() @@ -374,6 +374,6 @@ let rec loop () = | Vernacexpr.Drop -> () | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Vernacexpr.Quit -> exit 0 - | e -> + | any -> msgerrnl (str"Anomaly. Please report."); loop () diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3314e82c..ed8e215f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -156,7 +156,7 @@ let close_input in_chan (_,verb) = match verb with | Some verb_ch -> close_in verb_ch | _ -> () - with _ -> () + with e when Errors.noncritical e -> () let verbose_phrase verbch loc = let loc = unloc loc in @@ -232,13 +232,13 @@ let rec vernac_com interpfun checknav (loc,com) = Lexer.restore_com_state cs; Pp.comments := cl; Dumpglob.coqdoc_unfreeze cds - with e -> + with reraise -> if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; Lexer.restore_com_state cs; Pp.comments := cl; Dumpglob.coqdoc_unfreeze cds; - raise e + raise reraise end | VernacList l -> List.iter (fun (_,v) -> interp v) l @@ -250,7 +250,7 @@ let rec vernac_com interpfun checknav (loc,com) = (* If the command actually works, ignore its effects on the state *) States.with_state_protection (fun v -> interp v; raise HasNotFailed) v - with e -> match real_error e with + with e when Errors.noncritical e -> match real_error e with | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed !") | e -> @@ -278,16 +278,16 @@ let rec vernac_com interpfun checknav (loc,com) = States.with_heavy_rollback interpfun Cerrors.process_vernac_interp_error v; restore_timeout psh - with e -> restore_timeout psh; raise e + with reraise -> restore_timeout psh; raise reraise in try checknav loc com; current_timeout := !default_timeout; if do_beautify () then pr_new_syntax loc (Some com); interp com - with e -> + with any -> Format.set_formatter_out_channel stdout; - raise (DuringCommandInterp (loc, e)) + raise (DuringCommandInterp (loc, any)) and read_vernac_file verbosely s = Flags.make_warn verbosely; @@ -316,13 +316,13 @@ and read_vernac_file verbosely s = end_inner_command (snd loc_ast); pp_flush () done - with e -> (* whatever the exception *) + with reraise -> (* whatever the exception *) Format.set_formatter_out_channel stdout; close_input in_chan input; (* we must close the file first *) - match real_error e with + match real_error reraise with | End_of_input -> if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None - | _ -> raise_with_file fname e + | _ -> raise_with_file fname reraise (** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit] It executes one vernacular command. By default the command is @@ -359,9 +359,9 @@ let load_vernac verb file = Lib.mark_end_of_command (); (* in case we're still in coqtop init *) read_vernac_file verb file; if !Flags.beautify_file then close_out !chan_beautify; - with e -> + with reraise -> if !Flags.beautify_file then close_out !chan_beautify; - raise_with_file file e + raise_with_file file reraise (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6618b695..75efe139 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -295,7 +295,7 @@ let dump_universes_gen g s = close (); msgnl (str ("Universes written to file \""^s^"\".")) with - e -> close (); raise e + reraise -> close (); raise reraise let dump_universes sorted s = let g = Global.universes () in @@ -331,7 +331,7 @@ let msg_notfound_library loc qid = function let print_located_library r = let (loc,qid) = qualid_of_reference r in try msg_found_library (Library.locate_qualified_library false qid) - with e -> msg_notfound_library loc qid e + with e when Errors.noncritical e -> msg_notfound_library loc qid e let print_located_module r = let (loc,qid) = qualid_of_reference r in @@ -364,7 +364,7 @@ let dump_global r = try let gr = Smartlocate.smart_global r in Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr - with _ -> () + with e when Errors.noncritical e -> () (**********) (* Syntax *) @@ -388,6 +388,7 @@ let vernac_notation = Metasyntax.add_notation (* Gallina *) let start_proof_and_print k l hook = + check_locality (); (* early check, cf #2975 *) start_proof_com k l hook; print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () @@ -910,7 +911,9 @@ let vernac_declare_arguments local r l nargs flags = | None -> None | Some (o, k) -> try Some(ignore(Notation.find_scope k); k) - with _ -> Some (Notation.find_delimiters_scope o k)) scopes in + with e when Errors.noncritical e -> + Some (Notation.find_delimiters_scope o k)) scopes + in let some_scopes_specified = List.exists ((<>) None) scopes in let rargs = Util.list_map_filter (function (n, true) -> Some n | _ -> None) @@ -1417,7 +1420,7 @@ let vernac_reset_name id = let gr = Smartlocate.global_with_alias (Ident id) in Dumpglob.add_glob (fst id) gr; true - with _ -> false in + with e when Errors.noncritical e -> false in if not globalized then begin try begin match Lib.find_opening_node (snd id) with diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index c4cc4ae5..a1b76d3d 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -60,7 +60,7 @@ let call (opn,converted_args) = hunk() with | Drop -> raise Drop - | e -> + | reraise -> if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); - raise e + raise reraise -- cgit v1.2.3