summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:16 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:16 +0200
commit813d651c75cb954677a483b60d880600b421e011 (patch)
treef917021e7e7083cf1ce84f9a560179603f0c7af6
parent0c6687c12b628881d5660d57707f0e7ca9e521b7 (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge tag 'upstream/8.4pl2dfsg' into experimental/master
Upstream version 8.4pl2dfsg
-rw-r--r--CHANGES29
-rw-r--r--checker/check.ml6
-rw-r--r--checker/checker.ml3
-rw-r--r--checker/mod_checking.ml7
-rwxr-xr-xconfigure2
-rw-r--r--dev/base_include4
-rw-r--r--dev/top_printers.ml6
-rw-r--r--ide/coqide.ml7
-rw-r--r--ide/coqide_main.ml452
-rw-r--r--ide/gtk_parsing.ml1
-rw-r--r--ide/ide_win32_stubs.c44
-rw-r--r--interp/constrextern.ml33
-rw-r--r--interp/constrextern.mli9
-rw-r--r--interp/constrintern.ml14
-rw-r--r--interp/implicit_quantifiers.ml4
-rw-r--r--interp/notation.ml2
-rw-r--r--kernel/csymtable.ml4
-rw-r--r--kernel/mod_subst.ml25
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/modops.mli3
-rw-r--r--kernel/names.ml10
-rw-r--r--kernel/pre_env.ml2
-rw-r--r--kernel/safe_typing.ml5
-rw-r--r--kernel/subtyping.ml12
-rw-r--r--lib/envars.ml19
-rw-r--r--lib/errors.ml13
-rw-r--r--lib/errors.mli8
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/hashtbl_alt.ml2
-rw-r--r--lib/pp.ml42
-rw-r--r--lib/profile.ml30
-rw-r--r--lib/store.ml2
-rw-r--r--lib/system.ml24
-rw-r--r--lib/system.mli2
-rw-r--r--lib/xml_parser.ml6
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/heads.ml2
-rw-r--r--library/impargs.ml4
-rw-r--r--library/library.ml17
-rw-r--r--myocamlbuild.ml15
-rw-r--r--parsing/argextend.ml42
-rw-r--r--parsing/egrammar.ml2
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_xml.ml43
-rw-r--r--parsing/prettyp.ml8
-rw-r--r--parsing/printer.ml65
-rw-r--r--parsing/printer.mli11
-rw-r--r--parsing/printmod.ml59
-rw-r--r--parsing/tacextend.ml44
-rw-r--r--parsing/vernacextend.ml44
-rw-r--r--plugins/cc/ccalgo.ml7
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--plugins/decl_mode/decl_mode.ml4
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml9
-rw-r--r--plugins/extraction/extract_env.ml18
-rw-r--r--plugins/extraction/extraction.ml4
-rw-r--r--plugins/extraction/haskell.ml4
-rw-r--r--plugins/extraction/mlutil.ml4
-rw-r--r--plugins/extraction/ocaml.ml5
-rw-r--r--plugins/extraction/table.ml6
-rw-r--r--plugins/firstorder/g_ground.ml42
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/fourier/fourier.ml2
-rw-r--r--plugins/fourier/fourierR.ml18
-rw-r--r--plugins/funind/functional_principles_proofs.ml23
-rw-r--r--plugins/funind/functional_principles_types.ml13
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml13
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml14
-rw-r--r--plugins/funind/indfun_common.ml18
-rw-r--r--plugins/funind/invfun.ml17
-rw-r--r--plugins/funind/merge.ml6
-rw-r--r--plugins/funind/recdef.ml37
-rw-r--r--plugins/micromega/certificate.ml7
-rw-r--r--plugins/micromega/coq_micromega.ml24
-rw-r--r--plugins/micromega/csdpcert.ml6
-rw-r--r--plugins/micromega/mfourier.ml3
-rw-r--r--plugins/micromega/mutils.ml12
-rw-r--r--plugins/micromega/persistent_cache.ml10
-rw-r--r--plugins/nsatz/ideal.ml5
-rw-r--r--plugins/nsatz/polynom.ml4
-rw-r--r--plugins/nsatz/utile.ml16
-rw-r--r--plugins/omega/coq_omega.ml5
-rw-r--r--plugins/quote/quote.ml5
-rw-r--r--plugins/ring/ring.ml3
-rw-r--r--plugins/romega/const_omega.ml4
-rw-r--r--plugins/romega/refl_omega.ml30
-rw-r--r--plugins/subtac/g_subtac.ml43
-rw-r--r--plugins/subtac/subtac.ml4
-rw-r--r--plugins/subtac/subtac_cases.ml5
-rw-r--r--plugins/subtac/subtac_coercion.ml4
-rw-r--r--plugins/subtac/subtac_command.ml4
-rw-r--r--plugins/subtac/subtac_obligations.ml7
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml6
-rw-r--r--plugins/subtac/subtac_utils.ml8
-rw-r--r--plugins/xml/cic2acic.ml2
-rw-r--r--plugins/xml/doubleTypeInference.ml3
-rw-r--r--plugins/xml/xmlcommand.ml2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarutil.ml27
-rw-r--r--pretyping/evarutil.mli1
-rw-r--r--pretyping/evd.ml5
-rw-r--r--pretyping/evd.mli1
-rw-r--r--pretyping/inductiveops.ml1
-rw-r--r--pretyping/pretyping.ml11
-rw-r--r--pretyping/recordops.ml8
-rw-r--r--pretyping/reductionops.ml10
-rw-r--r--pretyping/retyping.ml12
-rw-r--r--pretyping/tacred.ml10
-rw-r--r--pretyping/typeclasses.ml10
-rw-r--r--pretyping/unification.ml13
-rw-r--r--pretyping/vnorm.ml24
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/goal.ml16
-rw-r--r--proofs/goal.mli2
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/pfedit.ml6
-rw-r--r--proofs/proof.ml10
-rw-r--r--proofs/proofview.ml10
-rw-r--r--proofs/refiner.ml8
-rw-r--r--proofs/tactic_debug.ml8
-rw-r--r--scripts/coqmktop.ml13
-rw-r--r--tactics/auto.ml11
-rw-r--r--tactics/autorewrite.ml12
-rw-r--r--tactics/class_tactics.ml47
-rw-r--r--tactics/eauto.ml43
-rw-r--r--tactics/equality.ml5
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/hipattern.ml410
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/rewrite.ml425
-rw-r--r--tactics/tacinterp.ml64
-rw-r--r--tactics/tactics.ml15
-rw-r--r--test-suite/bugs/closed/2955.v52
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2629.v22
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2668.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2734.v15
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2750.v23
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2928.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2983.v8
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2995.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/3000.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/3004.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/3008.v29
-rw-r--r--test-suite/output/inference.out4
-rw-r--r--test-suite/output/inference.v12
-rw-r--r--test-suite/success/remember.v8
-rw-r--r--theories/Numbers/NatInt/NZOrder.v2
-rw-r--r--toplevel/auto_ind_decl.ml44
-rw-r--r--toplevel/autoinstance.ml3
-rw-r--r--toplevel/backtrack.ml4
-rw-r--r--toplevel/classes.ml11
-rw-r--r--toplevel/coqinit.ml4
-rw-r--r--toplevel/coqtop.ml9
-rw-r--r--toplevel/himsg.ml11
-rw-r--r--toplevel/ide_intf.ml6
-rw-r--r--toplevel/ide_slave.ml11
-rw-r--r--toplevel/ind_tables.ml5
-rw-r--r--toplevel/indschemes.ml7
-rw-r--r--toplevel/lemmas.ml27
-rw-r--r--toplevel/metasyntax.ml13
-rw-r--r--toplevel/mltop.ml411
-rw-r--r--toplevel/search.ml2
-rw-r--r--toplevel/toplevel.ml12
-rw-r--r--toplevel/vernac.ml24
-rw-r--r--toplevel/vernacentries.ml13
-rw-r--r--toplevel/vernacinterp.ml4
170 files changed, 1205 insertions, 632 deletions
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:"<Ctrl>," ~stock:`PREFERENCES;
+ reset_revert_timer ()) ~accel:"<Ctrl>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