Commit 813d651c75cb954677a483b60d880600b421e011 - coq

+29

-0

CHANGES less more

	0	Changes from V8.4pl1 to V8.4pl2
	1	===============================
	2
	3	Bug fixes
	4
	5	- Solved bugs :
	6	#2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967
	7	#2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008
	8	- Partially fixed bugs : #2830 #2949
	9	- Coqtop should now react more reliably when receiving interrupt signals:
	10	all the "try...with" constructs have been protected against undue
	11	handling of the Sys.Break exception.
	12
	13	Coqide
	14
	15	- The Windows-specific code handling the interrupt button of Coqide
	16	had to be reworked (cf. bug #2869). Now, in Win32 this button does
	17	not target a specific coqtop client, but instead sends a Ctrl-C to
	18	any process sharing its console with Coqide. To avoid awkward
	19	effects, it is recommended to launch Coqide via its icon, its menu,
	20	or in a dedicated console window.
	21
	22	Extraction
	23
	24	- The option Extraction AccessOpaque is now set by default,
	25	restoring compatibility of older versions of Coq (cf bug #2952).
	26
0	27	Changes from V8.4 to V8.4pl1
1	28	============================
2	29

2437	2464
2438	2465	- Correctness proof of Stalmarck tautology checker algorithm
2439	2466	[Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis)
	2467
	2468	LocalWords: recommended

+3

-3

checker/check.ml less more

289	289	let (md,table,digest) =
290	290	try
291	291	let ch = with_magic_number_check raw_intern_library f in
292		let (md:library_disk) = System.marshal_in ch in
293		let digest = System.marshal_in ch in
294		let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
	292	let (md:library_disk) = System.marshal_in f ch in
	293	let digest = System.marshal_in f ch in
	294	let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
295	295	close_in ch;
296	296	if dir <> md.md_name then
297	297	errorlabstrm "load_physical_library"

+2

-1

checker/checker.ml less more

370	370	compile_files ();
371	371	flush_all()
372	372	with e ->
373		(Pp.ppnl(explain_exn e);
	373	(flush_all();
	374	Pp.ppnl(explain_exn e);
374	375	flush_all();
375	376	exit 1)
376	377

+6

-1

checker/mod_checking.ml less more

132	132	with Not_found ->
133	133	failwith ("Unknown module type: "^string_of_mp mp)
134	134
	135	let lookup_module mp env =
	136	try Environ.lookup_module mp env
	137	with Not_found ->
	138	failwith ("Unknown module: "^string_of_mp mp)
	139
135	140	let rec check_with env mtb with_decl mp=
136	141	match with_decl with
137	142	\| With_definition_body (idl,c) ->

198	203	SFBmodule msb -> msb
199	204	\| _ -> error_not_a_module l
200	205	in
201		let (_:module_body) = (lookup_module mp1 env) in ()
	206	let (_:module_body) = (Environ.lookup_module mp1 env) in ()
202	207	else
203	208	let old = match spec with
204	209	SFBmodule msb -> msb

+1

-1

configure less more

5	5	#
6	6	##################################
7	7
8		VERSION=8.4pl1
	8	VERSION=8.4pl2
9	9	VOMAGIC=08400
10	10	STATEMAGIC=58400
11	11	DATE=`LC_ALL=C LANG=C date +"%B %Y"`

+2

-2

dev/base_include less more

199	199
200	200	(* Set usual printing since the global env is available from the tracer *)
201	201	let _ = Constrextern.in_debugger := false
202		let _ = Constrextern.set_debug_global_reference_printer
203		(fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
	202	let _ = Constrextern.set_extern_reference
	203	(fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
204	204
205	205	open Toplevel
206	206	let go = loop

+3

-3

dev/top_printers.ml less more

458	458	Qualid (loc, make_qualid
459	459	(make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
460	460
461		let raw_string_of_ref loc = function
	461	let raw_string_of_ref loc _ = function
462	462	\| ConstRef cst ->
463	463	let (mp,dir,id) = repr_con cst in
464	464	encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)

474	474	\| VarRef id ->
475	475	encode_path loc "SECVAR" None [] id
476	476
477		let short_string_of_ref loc = function
	477	let short_string_of_ref loc _ = function
478	478	\| VarRef id -> Ident (loc,id)
479	479	\| ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst)))
480	480	\| IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn)))

490	490	pretty-printer should not make calls to the global env since ocamldebug
491	491	runs in a different process and does not have the proper env at hand *)
492	492	let _ = Constrextern.in_debugger := true
493		let _ = Constrextern.set_debug_global_reference_printer
	493	let _ = Constrextern.set_extern_reference
494	494	(if !rawdebug then raw_string_of_ref else short_string_of_ref)

+5

-2

ide/coqide.ml less more

211	211	try Sys.set_signal i (Sys.Signal_handle crash_save)
212	212	with _ -> prerr_endline "Signal ignored (normal if Win32)")
213	213	signals_to_crash;
	214	(* We ignore the Ctrl-C, this is required for the Stop button to work,
	215	since we will actually send Ctrl-C to all processes sharing
	216	our console (including us) *)
214	217	Sys.set_signal Sys.sigint Sys.Signal_ignore
215	218
216	219

901	904	if stop#compare start > 0 && is_sentence_end stop#backward_char
902	905	then Some (start,stop)
903	906	else None
904		with Not_found -> None
	907	with StartError -> None
905	908
906	909	method complete_at_offset (offset:int) =
907	910	prerr_endline ("Completion at offset : " ^ string_of_int offset);

2448	2451	try configure ~apply:update_notebook_pos ()
2449	2452	with _ -> flash_info "Cannot save preferences"
2450	2453	end;
2451		reset_revert_timer ()) ~accel:"<Ctrl>," ~stock:`PREFERENCES;
	2454	reset_revert_timer ()) ~accel:"<Ctrl>comma" ~stock:`PREFERENCES;
2452	2455	(* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
2453	2456	GAction.add_actions view_actions [
2454	2457	GAction.add_action "View" ~label:"_View";

+20

-30

ide/coqide_main.ml4 less more

37	37
38	38	let () = catch_gtk_messages ()
39	39
	40	(* We anticipate a bit the argument parsing and look for -debug *)
	41
	42	let early_set_debug () =
	43	Ideutils.debug := List.mem "-debug" (Array.to_list Sys.argv)
	44
40	45	(* On win32, we add the directory of coqide to the PATH at launch-time
41	46	(this used to be done in a .bat script). *)
42	47

45	50	(Filename.dirname Sys.executable_name ^ ";" ^
46	51	(try Sys.getenv "PATH" with _ -> ""))
47	52
48		(* On win32, since coqide is now console-free, we re-route stdout/stderr
49		to avoid Sys_error if someone writes to them. We write to a pipe which
50		is never read (by default) or to a temp log file (when in debug mode).
51		*)
	53	(* On win32, in debug mode we duplicate stdout/stderr in a log file. *)
52	54
53		let reroute_stdout_stderr () =
54		(* We anticipate a bit the argument parsing and look for -debug *)
55		let debug = List.mem "-debug" (Array.to_list Sys.argv) in
56		Ideutils.debug := debug;
57		let out_descr =
58		if debug then
59		let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
60		Coqide.logfile := Some name;
61		Unix.descr_of_out_channel chan
62		else
63		snd (Unix.pipe ())
64		in
	55	let log_stdout_stderr () =
	56	let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
	57	Coqide.logfile := Some name;
	58	let out_descr = Unix.descr_of_out_channel chan in
65	59	Unix.set_close_on_exec out_descr;
66	60	Unix.dup2 out_descr Unix.stdout;
67	61	Unix.dup2 out_descr Unix.stderr
68	62
69	63	(* We also provide specific kill and interrupt functions. *)
70	64
71		(* Since [win32_interrupt] involves some hack about the process console,
72		only one should run at the same time, we simply skip execution of
73		[win32_interrupt] if another instance is already running *)
74
75		let ctrl_c_mtx = Mutex.create ()
76
77		let ctrl_c_protect f i =
78		if not (Mutex.try_lock ctrl_c_mtx) then ()
79		else try f i; Mutex.unlock ctrl_c_mtx with _ -> Mutex.unlock ctrl_c_mtx
80
81	65	IFDEF WIN32 THEN
82	66	external win32_kill : int -> unit = "win32_kill"
83		external win32_interrupt : int -> unit = "win32_interrupt"
	67	external win32_interrupt_all : unit -> unit = "win32_interrupt_all"
	68	external win32_hide_console : unit -> unit = "win32_hide_console"
	69
84	70	let () =
	71	set_win32_path ();
85	72	Coq.killer := win32_kill;
86		Coq.interrupter := ctrl_c_protect win32_interrupt;
87		set_win32_path ();
88		reroute_stdout_stderr ()
	73	Coq.interrupter := (fun pid -> win32_interrupt_all ());
	74	early_set_debug ();
	75	if !Ideutils.debug then
	76	log_stdout_stderr ()
	77	else
	78	win32_hide_console ()
89	79	END
90	80
91	81	IFDEF QUARTZ THEN

+1

-0

ide/gtk_parsing.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
	8	open Ideutils
8	9
9	10	let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
10	11	let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)

+25

-23

ide/ide_win32_stubs.c less more

18	18	CAMLreturn(Val_unit);
19	19	}
20	20
21
22	21	/* Win32 emulation of a kill -2 (SIGINT) */
23	22
24		/* This code rely of the fact that coqide is now without initial console.
25		Otherwise, no console creation in win32unix/createprocess.c, hence
26		the same console for coqide and all coqtop, and everybody will be
27		signaled at the same time by the code below. */
	23	/* For simplicity, we signal all processes sharing a console with coqide.
	24	This shouldn't be an issue since currently at most one coqtop is busy
	25	at a given time. Earlier, we tried to be more precise via
	26	FreeConsole and AttachConsole before generating the Ctrl-C, but
	27	that wasn't working so well (see #2869).
	28	This code rely now on the fact that coqide is a console app,
	29	and that coqide itself ignores Ctrl-C.
	30	*/
28	31
29		/* Moreover, AttachConsole exists only since WinXP, and GetProcessId
30		since WinXP SP1. For avoiding the GetProcessId, we could adapt code
31		from win32unix/createprocess.c to make it return both the pid and the
32		handle. For avoiding the AttachConsole, I don't know, maybe having
33		an intermediate process between coqide and coqtop ? */
34
35		CAMLprim value win32_interrupt(value pseudopid) {
36		CAMLparam1(pseudopid);
37		HANDLE h;
38		DWORD pid;
39		FreeConsole(); /* Normally unnecessary, just to be sure... */
40		h = (HANDLE)(Long_val(pseudopid));
41		pid = GetProcessId(h);
42		AttachConsole(pid);
43		/* We want to survive the Ctrl-C that will also concerns us */
44		SetConsoleCtrlHandler(NULL,TRUE); /* NULL + TRUE means ignore */
45		GenerateConsoleCtrlEvent(CTRL_C_EVENT,0); /* signal our co-console */
46		FreeConsole();
	32	CAMLprim value win32_interrupt_all(value unit) {
	33	CAMLparam1(unit);
	34	GenerateConsoleCtrlEvent(CTRL_C_EVENT,0);
47	35	CAMLreturn(Val_unit);
48	36	}
	37
	38	/* Get rid of the nasty console window (only if we created it) */
	39
	40	CAMLprim value win32_hide_console (value unit) {
	41	CAMLparam1(unit);
	42	DWORD pid;
	43	HWND hw = GetConsoleWindow();
	44	if (hw != NULL) {
	45	GetWindowThreadProcessId(hw, &pid);
	46	if (pid == GetCurrentProcessId())
	47	ShowWindow(hw, SW_HIDE);
	48	}
	49	CAMLreturn(Val_unit);
	50	}

+19

-16

interp/constrextern.ml less more

136	136	let extern_evar loc n l =
137	137	if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
138	138
139		let debug_global_reference_printer =
140		ref (fun _ -> failwith "Cannot print a global reference")
	139	(** We allow customization of the global_reference printer.
	140	For instance, in the debugger the tables of global references
	141	may be inaccurate *)
	142
	143	let default_extern_reference loc vars r =
	144	Qualid (loc,shortest_qualid_of_global vars r)
	145
	146	let my_extern_reference = ref default_extern_reference
	147
	148	let set_extern_reference f = my_extern_reference := f
	149	let get_extern_reference () = !my_extern_reference
	150
	151	let extern_reference loc vars l = !my_extern_reference loc vars l
141	152
142	153	let in_debugger = ref false
143
144		let set_debug_global_reference_printer f =
145		debug_global_reference_printer := f
146
147		let extern_reference loc vars r =
148		if !in_debugger then
149		(* Debugger does not have the tables of global reference at hand *)
150		!debug_global_reference_printer loc r
151		else
152		Qualid (loc,shortest_qualid_of_global vars r)
153	154
154	155
155	156	(************************************************************************)

302	303	match decompose_notation_key ntn, l with
303	304	\| [Terminal "-"; Terminal x], [] ->
304	305	(try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
305		with _ -> mknot (loc,ntn,[]))
	306	with e when Errors.noncritical e -> mknot (loc,ntn,[]))
306	307	\| [Terminal x], [] ->
307	308	(try mkprim (loc, Numeral (Bigint.of_string x))
308		with _ -> mknot (loc,ntn,[]))
	309	with e when Errors.noncritical e -> mknot (loc,ntn,[]))
309	310	\| _ ->
310	311	mknot (loc,ntn,l)
311	312

815	816	match f with
816	817	\| GRef (_,ref) ->
817	818	let subscopes =
818		try list_skipn n (find_arguments_scope ref) with _ -> [] in
	819	try list_skipn n (find_arguments_scope ref)
	820	with e when Errors.noncritical e -> [] in
819	821	let impls =
820	822	let impls =
821	823	select_impargs_size
822	824	(List.length args) (implicits_of_global ref) in
823		try list_skipn n impls with _ -> [] in
	825	try list_skipn n impls
	826	with e when Errors.noncritical e -> [] in
824	827	subscopes,impls
825	828	\| _ ->
826	829	[], [] in

+6

-3

interp/constrextern.mli less more

49	49	val print_no_symbol : bool ref
50	50	val print_projections : bool ref
51	51
52		(** Debug printing options *)
53		val set_debug_global_reference_printer :
54		(loc -> global_reference -> reference) -> unit
	52	(** Customization of the global_reference printer *)
	53	val set_extern_reference :
	54	(loc -> Idset.t -> global_reference -> reference) -> unit
	55	val get_extern_reference :
	56	unit -> (loc -> Idset.t -> global_reference -> reference)
	57
55	58	val in_debugger : bool ref
56	59
57	60	(** This governs printing of implicit arguments. If [with_implicits] is

+7

-7

interp/constrintern.ml less more

649	649	let scopes = find_arguments_scope ref in
650	650	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
651	651	GRef (loc, ref), impls, scopes, []
652		with _ ->
	652	with e when Errors.noncritical e ->
653	653	(* [id] a goal variable *)
654	654	GVar (loc,id), [], [], []
655	655

715	715	try
716	716	let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
717	717	find_appl_head_data r, args2
718		with e ->
	718	with e when Errors.noncritical e ->
719	719	(* Extra allowance for non globalizing functions *)
720	720	if !interning_grammar \|\| env.unb then
721	721	(GVar (loc,id), [], [], []),args

968	968	\| [] -> anomaly "Number of projections mismatch"
969	969	\| (_, regular)::tm ->
970	970	let boolean = not regular in
971		if ConstRef name = global_reference_of_reference refer
972		then
	971	(match global_reference_of_reference refer with
	972	\| ConstRef name' when eq_constant name name' ->
973	973	if boolean && mode then
974	974	user_err_loc (loc, "", str"No local fields allowed in a record construction.")
975	975	else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
976		else
	976	\| _ ->
977	977	build_patt b tm (if boolean&&mode then i else i + 1)
978	978	(if boolean && mode then acc
979		else fst acc, (i, ConstRef name) :: snd acc))
	979	else fst acc, (i, ConstRef name) :: snd acc)))
980	980	\| None :: b-> (* we don't want anonymous fields *)
981	981	if mode then
982	982	user_err_loc (loc, "", str "This record contains anonymous fields.")

1008	1008	(loc, "",
1009	1009	str "This record contains fields of different records.")
1010	1010	\| (i, a) :: b->
1011		if glob_refer = a
	1011	if eq_gr glob_refer a
1012	1012	then (i,List.rev_append acc l)
1013	1013	else add_patt b ((i,a)::acc)
1014	1014	in

+2

-2

interp/implicit_quantifiers.ml less more

87	87	if Idset.mem x ids then false
88	88	else
89	89	try ignore(Environ.lookup_named x env) ; false
90		with _ -> not (is_global x)
91		with _ -> true
	90	with e when Errors.noncritical e -> not (is_global x)
	91	with e when Errors.noncritical e -> true
92	92
93	93	(* Auxiliary functions for the inference of implicitly quantified variables. *)
94	94

+1

-1

interp/notation.ml less more

837	837	let with_notation_protection f x =
838	838	let fs = freeze () in
839	839	try let a = f x in unfreeze fs; a
840		with e -> unfreeze fs; raise e
	840	with reraise -> unfreeze fs; raise reraise

+3

-1

kernel/csymtable.ml less more

189	189	and val_of_constr env c =
190	190	let (_,fun_code,_ as ccfv) =
191	191	try compile env c
192		with e -> print_string "can not compile \n";Format.print_flush();raise e in
	192	with reraise ->
	193	print_string "can not compile \n";Format.print_flush();raise reraise
	194	in
193	195	eval_to_patch env (to_memory ccfv)
194	196
195	197	let set_transparent_const kn =

+17

-12

kernel/mod_subst.ml less more

82	82	\| Equiv kn -> string_of_kn kn
83	83
84	84	let debug_string_of_delta resolve =
85		let kn_to_string kn hint s =
86		s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint)
87		in
88		let mp_to_string mp mp' s =
89		s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp')
90		in
91		Deltamap.fold mp_to_string kn_to_string resolve ""
	85	let kn_to_string kn hint l =
	86	(string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l
	87	in
	88	let mp_to_string mp mp' l =
	89	(string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l
	90	in
	91	let l = Deltamap.fold mp_to_string kn_to_string resolve [] in
	92	String.concat ", " (List.rev l)
92	93
93	94	let list_contents sub =
94	95	let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in

172	173
173	174	let kn_of_delta resolve kn =
174	175	try solve_delta_kn resolve kn
175		with _ -> kn
	176	with e when Errors.noncritical e -> kn
176	177
177	178	let constant_of_delta_kn resolve kn =
178	179	constant_of_kn_equiv kn (kn_of_delta resolve kn)

181	182	try
182	183	let new_kn = solve_delta_kn resolve kn in
183	184	if kn == new_kn then x else fix_can new_kn
184		with _ -> x
	185	with e when Errors.noncritical e -> x
185	186
186	187	let constant_of_delta resolve con =
187	188	let kn = user_con con in

222	223	let kn1,kn2 = canonical_con con,user_con con in
223	224	try find_inline_of_delta kn2 resolve
224	225	with Not_found ->
225		try find_inline_of_delta kn1 resolve
226		with Not_found -> None
	226	if kn1 == kn2 then None
	227	else
	228	try find_inline_of_delta kn1 resolve
	229	with Not_found -> None
227	230
228	231	let subst_mp0 sub mp = (* 's like subst *)
229	232	let rec aux mp =

271	274	\| Canonical
272	275
273	276	let gen_subst_mp f sub mp1 mp2 =
274		match subst_mp0 sub mp1, subst_mp0 sub mp2 with
	277	let o1 = subst_mp0 sub mp1 in
	278	let o2 = if mp1 == mp2 then o1 else subst_mp0 sub mp2 in
	279	match o1, o2 with
275	280	\| None, None -> raise No_subst
276	281	\| Some (mp',resolve), None -> User, (f mp' mp2), resolve
277	282	\| None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve

+1

-1

kernel/modops.ml less more

32	32	\| NotConvertibleInductiveField of identifier
33	33	\| NotConvertibleConstructorField of identifier
34	34	\| NotConvertibleBodyField
35		\| NotConvertibleTypeField
	35	\| NotConvertibleTypeField of env * types * types
36	36	\| NotSameConstructorNamesField
37	37	\| NotSameInductiveNameInBlockField
38	38	\| FiniteInductiveFieldExpected of bool

+2

-1

kernel/modops.mli less more

8	8	open Util
9	9	open Names
10	10	open Univ
	11	open Term
11	12	open Environ
12	13	open Declarations
13	14	open Entries

59	60	\| NotConvertibleInductiveField of identifier
60	61	\| NotConvertibleConstructorField of identifier
61	62	\| NotConvertibleBodyField
62		\| NotConvertibleTypeField
	63	\| NotConvertibleTypeField of env * types * types
63	64	\| NotSameConstructorNamesField
64	65	\| NotSameInductiveNameInBlockField
65	66	\| FiniteInductiveFieldExpected of bool

+7

-3

kernel/names.ml less more

204	204	let constant_of_kn kn = (kn,kn)
205	205	let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
206	206	let make_con mp dir l = constant_of_kn (mp,dir,l)
207		let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
	207	let make_con_equiv mp1 mp2 dir l =
	208	if mp1 == mp2 then make_con mp1 dir l
	209	else ((mp1,dir,l),(mp2,dir,l))
208	210	let canonical_con con = snd con
209	211	let user_con con = fst con
210	212	let repr_con con = fst con

262	264
263	265	let mind_of_kn kn = (kn,kn)
264	266	let mind_of_kn_equiv kn1 kn2 = (kn1,kn2)
265		let make_mind mp dir l = ((mp,dir,l),(mp,dir,l))
266		let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
	267	let make_mind mp dir l = mind_of_kn (mp,dir,l)
	268	let make_mind_equiv mp1 mp2 dir l =
	269	if mp1 == mp2 then make_mind mp1 dir l
	270	else ((mp1,dir,l),(mp2,dir,l))
267	271	let canonical_mind mind = snd mind
268	272	let user_mind mind = fst mind
269	273	let repr_mind mind = fst mind

+1

-1

kernel/pre_env.ml less more

89	89
90	90	let lookup_rel_val n env =
91	91	try List.nth env.env_rel_val (n - 1)
92		with _ -> raise Not_found
	92	with e when Errors.noncritical e -> raise Not_found
93	93
94	94	let env_of_rel n env =
95	95	{ env with

+3

-2

kernel/safe_typing.ml less more

476	476	in
477	477	let str = match sign with
478	478	\| SEBstruct(str_l) -> str_l
479		\| _ -> error ("You cannot Include a high-order structure.")
	479	\| _ -> error ("You cannot Include a higher-order structure.")
480	480	in
481	481	let senv = update_resolver (add_delta_resolver resolver) senv
482	482	in

872	872	let k = key_of_lazy_constr k in
873	873	let access key =
874	874	try (Lazy.force table).(key)
875		with _ -> error "Error while retrieving an opaque body"
	875	with e when Errors.noncritical e ->
	876	error "Error while retrieving an opaque body"
876	877	in
877	878	match load_proof with
878	879	\| Flags.Force ->

+8

-4

kernel/subtyping.ml less more

218	218	let check_conv cst f = check_conv_error error cst f in
219	219	let check_type cst env t1 t2 =
220	220
	221	let err = NotConvertibleTypeField (env, t1, t2) in
	222
221	223	(* If the type of a constant is generated, it may mention
222	224	non-variable algebraic universes that the general conversion
223	225	algorithm is not ready to handle. Anyway, generated types of

256	258	(the user has to use an explicit type in the interface *)
257	259	error NoTypeConstraintExpected
258	260	with NotArity ->
259		error NotConvertibleTypeField end
	261	error err end
260	262	\| _ ->
261	263	t1,t2
262	264	else
263	265	(t1,t2) in
264		check_conv NotConvertibleTypeField cst conv_leq env t1 t2
	266	check_conv err cst conv_leq env t1 t2
265	267	in
266	268
267	269	match info1 with

300	302	if constant_has_body cb2 then error DefinitionFieldExpected;
301	303	let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
302	304	let typ2 = Typeops.type_of_constant_type env cb2.const_type in
303		check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
	305	let error = NotConvertibleTypeField (env, arity1, typ2) in
	306	check_conv error cst conv_leq env arity1 typ2
304	307	\| IndConstr (((kn,i),j) as cstr,mind1) ->
305	308	ignore (Util.error (
306	309	"The kernel does not recognize yet that a parameter can be " ^

311	314	if constant_has_body cb2 then error DefinitionFieldExpected;
312	315	let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
313	316	let ty2 = Typeops.type_of_constant_type env cb2.const_type in
314		check_conv NotConvertibleTypeField cst conv env ty1 ty2
	317	let error = NotConvertibleTypeField (env, ty1, ty2) in
	318	check_conv error cst conv env ty1 ty2
315	319
316	320	let rec check_modules cst env msb1 msb2 subst1 subst2 =
317	321	let mty1 = module_type_of_module None msb1 in

+11

-8

lib/envars.ml less more

21	21	let _ =
22	22	if Coq_config.arch = "win32" then
23	23	Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "")
	24
	25	let exe s = s ^ Coq_config.exec_extension
24	26
25	27	let reldir instdir testfile oth =
26	28	let rpath = if Coq_config.local then [] else instdir in

86	88	else which tl f
87	89
88	90	let guess_camlbin () =
89		let path = try Sys.getenv "PATH" with _ -> raise Not_found in
	91	let path = Sys.getenv "PATH" in (* may raise Not_found *)
90	92	let lpath = path_to_list path in
91		which lpath "ocamlc"
	93	which lpath (exe "ocamlc")
92	94
93	95	let guess_camlp4bin () =
94		let path = try Sys.getenv "PATH" with _ -> raise Not_found in
	96	let path = Sys.getenv "PATH" in (* may raise Not_found *)
95	97	let lpath = path_to_list path in
96		which lpath Coq_config.camlp4
	98	which lpath (exe Coq_config.camlp4)
97	99
98	100	let camlbin () =
99	101	if !Flags.camlbin_spec then !Flags.camlbin else
100	102	if !Flags.boot then Coq_config.camlbin else
101		try guess_camlbin () with _ -> Coq_config.camlbin
	103	try guess_camlbin () with e when e <> Sys.Break -> Coq_config.camlbin
102	104
103	105	let camllib () =
104	106	if !Flags.boot

112	114	let camlp4bin () =
113	115	if !Flags.camlp4bin_spec then !Flags.camlp4bin else
114	116	if !Flags.boot then Coq_config.camlp4bin else
115		try guess_camlp4bin () with _ -> let cb = camlbin () in
116		if Sys.file_exists (Filename.concat cb Coq_config.camlp4) then cb
117		else Coq_config.camlp4bin
	117	try guess_camlp4bin () with e when e <> Sys.Break ->
	118	let cb = camlbin () in
	119	if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb
	120	else Coq_config.camlp4bin
118	121
119	122	let camlp4lib () =
120	123	if !Flags.boot

+12

-1

lib/errors.ml less more

27	27	try h e
28	28	with
29	29	\| Unhandled -> print_gen bottom stk' e
30		\| e' -> print_gen bottom stk' e'
	30	\| any -> print_gen bottom stk' any
31	31
32	32	(** Only anomalies should reach the bottom of the handler stack.
33	33	In usual situation, the [handle_stack] is treated as it if was always

65	65	\| _ -> raise Unhandled
66	66	end
67	67
	68	(** Critical exceptions shouldn't be catched and ignored by mistake
	69	by inner functions during a [vernacinterp]. They should be handled
	70	only at the very end of interp, to be displayed to the user. *)
	71
	72	(** NB: in the 8.4 branch, for maximal compatibility, anomalies
	73	are considered non-critical *)
	74
	75	let noncritical = function
	76	\| Sys.Break \| Out_of_memory \| Stack_overflow -> false
	77	\| _ -> true
	78

+8

-0

lib/errors.mli less more

38	38	(** Same as [print], except that anomalies are not printed but re-raised
39	39	(used for the Fail command) *)
40	40	val print_no_anomaly : exn -> Pp.std_ppcmds
	41
	42	(** Critical exceptions shouldn't be catched and ignored by mistake
	43	by inner functions during a [vernacinterp]. They should be handled
	44	only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user.
	45	Typical example: [Sys.Break]. In the 8.4 branch, for maximal
	46	compatibility, anomalies are not considered as critical...
	47	*)
	48	val noncritical : exn -> bool

+2

-2

lib/flags.ml less more

8	8	let with_option o f x =
9	9	let old = !o in o:=true;
10	10	try let r = f x in o := old; r
11		with e -> o := old; raise e
	11	with reraise -> o := old; raise reraise
12	12
13	13	let without_option o f x =
14	14	let old = !o in o:=false;
15	15	try let r = f x in o := old; r
16		with e -> o := old; raise e
	16	with reraise -> o := old; raise reraise
17	17
18	18	let boot = ref false
19	19

+1

-1

lib/hashtbl_alt.ml less more

88	88	match rest2 with
89	89	\| Empty -> add hash key; key
90	90	\| Cons (k3, h3, rest3) ->
91		if hash == h2 && E.equals key k3 then k3
	91	if hash == h3 && E.equals key k3 then k3
92	92	else find_rec hash key rest3
93	93
94	94	end

+1

-1

lib/pp.ml4 less more

278	278	try
279	279	Stream.iter pp_dir dirstream; com_brk ft
280	280	with
281		\| e -> Format.pp_print_flush ft () ; raise e
	281	\| reraise -> Format.pp_print_flush ft () ; raise reraise
282	282
283	283
284	284	(* pretty print on stdout and stderr *)

+99

-99

lib/profile.ml less more

259	259	let _dw = dummy_spent_alloc () in
260	260	let _dt = get_time () in
261	261	()
262		with _ -> assert false
	262	with e when e <> Sys.Break -> assert false
263	263	done;
264	264	let after = get_time () in
265	265	let beforeloop = get_time () in

389	389	(match !stack with [] -> assert false \| _::s -> stack := s);
390	390	last_alloc := get_alloc ();
391	391	r
392		with exn ->
393		let dw = spent_alloc () in
394		let dt = get_time () - t in
395		e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
396		ajoute_ownalloc e dw;
397		ajoute_totalloc e dw;
398		p.owntime <- p.owntime - dt;
399		ajoute_totalloc p (e.totalloc -. totalloc0);
400		p.intcount <- p.intcount + e.intcount - intcount0 + 1;
401		p.immcount <- p.immcount + 1;
402		if not (p==e) then
403		(match !stack with [] -> assert false \| _::s -> stack := s);
404		last_alloc := get_alloc ();
405		raise exn
	392	with reraise ->
	393	let dw = spent_alloc () in
	394	let dt = get_time () - t in
	395	e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
	396	ajoute_ownalloc e dw;
	397	ajoute_totalloc e dw;
	398	p.owntime <- p.owntime - dt;
	399	ajoute_totalloc p (e.totalloc -. totalloc0);
	400	p.intcount <- p.intcount + e.intcount - intcount0 + 1;
	401	p.immcount <- p.immcount + 1;
	402	if not (p==e) then
	403	(match !stack with [] -> assert false \| _::s -> stack := s);
	404	last_alloc := get_alloc ();
	405	raise reraise
406	406
407	407	let profile2 e f a b =
408	408	let dw = spent_alloc () in

431	431	(match !stack with [] -> assert false \| _::s -> stack := s);
432	432	last_alloc := get_alloc ();
433	433	r
434		with exn ->
435		let dw = spent_alloc () in
436		let dt = get_time () - t in
437		e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
438		ajoute_ownalloc e dw;
439		ajoute_totalloc e dw;
440		p.owntime <- p.owntime - dt;
441		ajoute_totalloc p (e.totalloc -. totalloc0);
442		p.intcount <- p.intcount + e.intcount - intcount0 + 1;
443		p.immcount <- p.immcount + 1;
444		if not (p==e) then
445		(match !stack with [] -> assert false \| _::s -> stack := s);
446		last_alloc := get_alloc ();
447		raise exn
	434	with reraise ->
	435	let dw = spent_alloc () in
	436	let dt = get_time () - t in
	437	e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
	438	ajoute_ownalloc e dw;
	439	ajoute_totalloc e dw;
	440	p.owntime <- p.owntime - dt;
	441	ajoute_totalloc p (e.totalloc -. totalloc0);
	442	p.intcount <- p.intcount + e.intcount - intcount0 + 1;
	443	p.immcount <- p.immcount + 1;
	444	if not (p==e) then
	445	(match !stack with [] -> assert false \| _::s -> stack := s);
	446	last_alloc := get_alloc ();
	447	raise reraise
448	448
449	449	let profile3 e f a b c =
450	450	let dw = spent_alloc () in

473	473	(match !stack with [] -> assert false \| _::s -> stack := s);
474	474	last_alloc := get_alloc ();
475	475	r
476		with exn ->
477		let dw = spent_alloc () in
478		let dt = get_time () - t in
479		e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
480		ajoute_ownalloc e dw;
481		ajoute_totalloc e dw;
482		p.owntime <- p.owntime - dt;
483		ajoute_totalloc p (e.totalloc -. totalloc0);
484		p.intcount <- p.intcount + e.intcount - intcount0 + 1;
485		p.immcount <- p.immcount + 1;
486		if not (p==e) then
487		(match !stack with [] -> assert false \| _::s -> stack := s);
488		last_alloc := get_alloc ();
489		raise exn
	476	with reraise ->
	477	let dw = spent_alloc () in
	478	let dt = get_time () - t in
	479	e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
	480	ajoute_ownalloc e dw;
	481	ajoute_totalloc e dw;
	482	p.owntime <- p.owntime - dt;
	483	ajoute_totalloc p (e.totalloc -. totalloc0);
	484	p.intcount <- p.intcount + e.intcount - intcount0 + 1;
	485	p.immcount <- p.immcount + 1;
	486	if not (p==e) then
	487	(match !stack with [] -> assert false \| _::s -> stack := s);
	488	last_alloc := get_alloc ();
	489	raise reraise
490	490
491	491	let profile4 e f a b c d =
492	492	let dw = spent_alloc () in

515	515	(match !stack with [] -> assert false \| _::s -> stack := s);
516	516	last_alloc := get_alloc ();
517	517	r
518		with exn ->
519		let dw = spent_alloc () in
520		let dt = get_time () - t in
521		e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
522		ajoute_ownalloc e dw;
523		ajoute_totalloc e dw;
524		p.owntime <- p.owntime - dt;
525		ajoute_totalloc p (e.totalloc -. totalloc0);
526		p.intcount <- p.intcount + e.intcount - intcount0 + 1;
527		p.immcount <- p.immcount + 1;
528		if not (p==e) then
529		(match !stack with [] -> assert false \| _::s -> stack := s);
530		last_alloc := get_alloc ();
531		raise exn
	518	with reraise ->
	519	let dw = spent_alloc () in
	520	let dt = get_time () - t in
	521	e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
	522	ajoute_ownalloc e dw;
	523	ajoute_totalloc e dw;
	524	p.owntime <- p.owntime - dt;
	525	ajoute_totalloc p (e.totalloc -. totalloc0);
	526	p.intcount <- p.intcount + e.intcount - intcount0 + 1;
	527	p.immcount <- p.immcount + 1;
	528	if not (p==e) then
	529	(match !stack with [] -> assert false \| _::s -> stack := s);
	530	last_alloc := get_alloc ();
	531	raise reraise
532	532
533	533	let profile5 e f a b c d g =
534	534	let dw = spent_alloc () in

557	557	(match !stack with [] -> assert false \| _::s -> stack := s);
558	558	last_alloc := get_alloc ();
559	559	r
560		with exn ->
561		let dw = spent_alloc () in
562		let dt = get_time () - t in
563		e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
564		ajoute_ownalloc e dw;
565		ajoute_totalloc e dw;
566		p.owntime <- p.owntime - dt;
567		ajoute_totalloc p (e.totalloc -. totalloc0);
568		p.intcount <- p.intcount + e.intcount - intcount0 + 1;
569		p.immcount <- p.immcount + 1;
570		if not (p==e) then
571		(match !stack with [] -> assert false \| _::s -> stack := s);
572		last_alloc := get_alloc ();
573		raise exn
	560	with reraise ->
	561	let dw = spent_alloc () in
	562	let dt = get_time () - t in
	563	e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
	564	ajoute_ownalloc e dw;
	565	ajoute_totalloc e dw;
	566	p.owntime <- p.owntime - dt;
	567	ajoute_totalloc p (e.totalloc -. totalloc0);
	568	p.intcount <- p.intcount + e.intcount - intcount0 + 1;
	569	p.immcount <- p.immcount + 1;
	570	if not (p==e) then
	571	(match !stack with [] -> assert false \| _::s -> stack := s);
	572	last_alloc := get_alloc ();
	573	raise reraise
574	574
575	575	let profile6 e f a b c d g h =
576	576	let dw = spent_alloc () in

599	599	(match !stack with [] -> assert false \| _::s -> stack := s);
600	600	last_alloc := get_alloc ();
601	601	r
602		with exn ->
603		let dw = spent_alloc () in
604		let dt = get_time () - t in
605		e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
606		ajoute_ownalloc e dw;
607		ajoute_totalloc e dw;
608		p.owntime <- p.owntime - dt;
609		ajoute_totalloc p (e.totalloc -. totalloc0);
610		p.intcount <- p.intcount + e.intcount - intcount0 + 1;
611		p.immcount <- p.immcount + 1;
612		if not (p==e) then
613		(match !stack with [] -> assert false \| _::s -> stack := s);
614		last_alloc := get_alloc ();
615		raise exn
	602	with reraise ->
	603	let dw = spent_alloc () in
	604	let dt = get_time () - t in
	605	e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
	606	ajoute_ownalloc e dw;
	607	ajoute_totalloc e dw;
	608	p.owntime <- p.owntime - dt;
	609	ajoute_totalloc p (e.totalloc -. totalloc0);
	610	p.intcount <- p.intcount + e.intcount - intcount0 + 1;
	611	p.immcount <- p.immcount + 1;
	612	if not (p==e) then
	613	(match !stack with [] -> assert false \| _::s -> stack := s);
	614	last_alloc := get_alloc ();
	615	raise reraise
616	616
617	617	let profile7 e f a b c d g h i =
618	618	let dw = spent_alloc () in

641	641	(match !stack with [] -> assert false \| _::s -> stack := s);
642	642	last_alloc := get_alloc ();
643	643	r
644		with exn ->
645		let dw = spent_alloc () in
646		let dt = get_time () - t in
647		e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
648		ajoute_ownalloc e dw;
649		ajoute_totalloc e dw;
650		p.owntime <- p.owntime - dt;
651		ajoute_totalloc p (e.totalloc -. totalloc0);
652		p.intcount <- p.intcount + e.intcount - intcount0 + 1;
653		p.immcount <- p.immcount + 1;
654		if not (p==e) then
655		(match !stack with [] -> assert false \| _::s -> stack := s);
656		last_alloc := get_alloc ();
657		raise exn
	644	with reraise ->
	645	let dw = spent_alloc () in
	646	let dt = get_time () - t in
	647	e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
	648	ajoute_ownalloc e dw;
	649	ajoute_totalloc e dw;
	650	p.owntime <- p.owntime - dt;
	651	ajoute_totalloc p (e.totalloc -. totalloc0);
	652	p.intcount <- p.intcount + e.intcount - intcount0 + 1;
	653	p.immcount <- p.immcount + 1;
	654	if not (p==e) then
	655	(match !stack with [] -> assert false \| _::s -> stack := s);
	656	last_alloc := get_alloc ();
	657	raise reraise
658	658
659	659	(* Some utilities to compute the logical and physical sizes and depth
660	660	of ML objects *)

+1

-1

lib/store.ml less more

52	52	in
53	53	let get s =
54	54	try Some (Obj.obj (Util.Intmap.find fid s))
55		with _ -> None
	55	with Not_found -> None
56	56	in
57	57	let remove s =
58	58	Util.Intmap.remove fid s

+15

-9

lib/system.ml less more

139	139
140	140	let ok_dirname f =
141	141	f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
142		try ignore (check_ident f); true with _ -> false
	142	try ignore (check_ident f); true
	143	with e when e <> Sys.Break -> false
143	144
144	145	let all_subdirs ~unix_path:root =
145	146	let l = ref [] in

222	223	try access name [R_OK];true with Unix_error (_, _, _) -> false
223	224
224	225	let open_trapping_failure name =
225		try open_out_bin name with _ -> error ("Can't open " ^ name)
	226	try open_out_bin name
	227	with e when e <> Sys.Break -> error ("Can't open " ^ name)
226	228
227	229	let try_remove filename =
228	230	try Sys.remove filename
229		with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
230		str filename ++ str" which is corrupted!" )
	231	with e when e <> Sys.Break ->
	232	msgnl (str"Warning: " ++ str"Could not remove file " ++
	233	str filename ++ str" which is corrupted!" )
231	234
232	235	let marshal_out ch v = Marshal.to_channel ch v []
233		let marshal_in ch =
	236	let marshal_in filename ch =
234	237	try Marshal.from_channel ch
235		with End_of_file -> error "corrupted file: reached end of file"
	238	with
	239	\| End_of_file -> error "corrupted file: reached end of file"
	240	\| Failure _ (* e.g. "truncated object" *) ->
	241	error (filename ^ " is corrupted, try to rebuild it.")
236	242
237	243	exception Bad_magic_number of string
238	244

258	264	try
259	265	marshal_out channel val_0;
260	266	close_out channel
261		with e ->
262		begin try_remove filename; raise e end
	267	with reraise ->
	268	begin try_remove filename; raise reraise end
263	269	with Sys_error s -> error ("System error: " ^ s)
264	270	and intern_state paths name =
265	271	try
266	272	let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in
267	273	let channel = raw_intern filename in
268		let v = marshal_in channel in
	274	let v = marshal_in filename channel in
269	275	close_in channel;
270	276	v
271	277	with Sys_error s ->

+1

-1

lib/system.mli less more

46	46	when the check fails, with the full file name. *)
47	47
48	48	val marshal_out : out_channel -> 'a -> unit
49		val marshal_in : in_channel -> 'a
	49	val marshal_in : string -> in_channel -> 'a
50	50
51	51	exception Bad_magic_number of string
52	52

+3

-3

lib/xml_parser.ml less more

174	174	if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
175	175	Xml_lexer.close source;
176	176	x
177		with e ->
	177	with e when e <> Sys.Break ->
178	178	Xml_lexer.close source;
179	179	raise (!xml_error (error_of_exn stk e) source)
180	180

189	189	close_in ch;
190	190	x
191	191	with
192		e ->
	192	reraise ->
193	193	close_in ch;
194		raise e
	194	raise reraise
195	195
196	196
197	197	let error_msg = function

+2

-2

library/declaremods.ml less more

989	989	let protect_summaries f =
990	990	let fs = Summary.freeze_summaries () in
991	991	try f fs
992		with e ->
	992	with reraise ->
993	993	(* Something wrong: undo the whole process *)
994		Summary.unfreeze_summaries fs; raise e
	994	Summary.unfreeze_summaries fs; raise reraise
995	995
996	996	let declare_include interp_struct me_asts =
997	997	protect_summaries

+1

-1

library/heads.ml less more

87	87	\| Sort _ \| Ind _ \| Prod _ -> RigidHead RigidType
88	88	\| Cast (c,_,_) -> aux k l c b
89	89	\| Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b
90		\| Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b
	90	\| Lambda (_,_,c) -> aux k (List.tl l) (subst1 (List.hd l) c) b
91	91	\| LetIn _ -> assert false
92	92	\| Meta _ \| Evar _ -> NotImmediatelyComputableHead
93	93	\| App (c,al) -> aux k (Array.to_list al @ l) c b

+2

-2

library/impargs.ml less more

73	73	let rslt = f x in
74	74	implicit_args := oflags;
75	75	rslt
76		with e -> begin
	76	with reraise -> begin
77	77	implicit_args := oflags;
78		raise e
	78	raise reraise
79	79	end
80	80
81	81	let set_maximality imps b =

+9

-8

library/library.ml less more

367	367	let try_locate_absolute_library dir =
368	368	try
369	369	locate_absolute_library dir
370		with e ->
	370	with e when Errors.noncritical e ->
371	371	explain_locate_library_error (qualid_of_dirpath dir) e
372	372
373	373	let try_locate_qualified_library (loc,qid) =
374	374	try
375	375	let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
376	376	dir,f
377		with e ->
	377	with e when Errors.noncritical e ->
378	378	explain_locate_library_error qid e
379	379
380	380

397	397	try
398	398	let ch = System.with_magic_number_check raw_intern_library f in
399	399	seek_in ch pos;
400		if System.marshal_in ch <> digest then failwith "File changed!";
401		let table = (System.marshal_in ch : LightenLibrary.table) in
	400	if System.marshal_in f ch <> digest then failwith "File changed!";
	401	let table = (System.marshal_in f ch : LightenLibrary.table) in
402	402	close_in ch;
403	403	table
404		with _ ->
	404	with e when Errors.noncritical e ->
405	405	error
406	406	("The file "^f^" is inaccessible or has changed,\n" ^
407	407	"cannot load some opaque constant bodies in it.\n")
408	408
409	409	let intern_from_file f =
410	410	let ch = System.with_magic_number_check raw_intern_library f in
411		let lmd = System.marshal_in ch in
	411	let lmd = System.marshal_in f ch in
412	412	let pos = pos_in ch in
413		let digest = System.marshal_in ch in
	413	let digest = System.marshal_in f ch in
414	414	let table = lazy (fetch_opaque_table (f,pos,digest)) in
415	415	register_library_filename lmd.md_name f;
416	416	let library = mk_library lmd table digest in

654	654	System.marshal_out ch di;
655	655	System.marshal_out ch table;
656	656	close_out ch
657		with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e
	657	with reraise ->
	658	warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise
658	659
659	660	(************************************************************************)
660	661	(s Display the memory use of a library. )

+9

-6

myocamlbuild.ml less more

392	392	Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc;
393	393	A "--output-format";A "coff";A "--output"; Px o]));
394	394
395		(** The windows version of Coqide is now a console-free win32 app,
396		which moreover contains the Coq icon. If necessary, the mkwinapp
397		tool can be used later to restore or suppress the console of Coqide. *)
	395	(** Embed the Coq icon inside the windows version of Coqide *)
398	396
399	397	if w32 then dep ["link"; "ocaml"; "program"; "ide"] [w32ico];
400
401		if w32 then flag ["link"; "ocaml"; "program"; "ide"]
402		(S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]);
	398	if w32 then flag ["link"; "ocaml"; "program"; "ide"] (P w32ico);
	399
	400	(** Ealier we tried to make Coqide a console-free win32 app,
	401	but that was troublesome (unavailable stdout/stderr, issues
	402	with the stop button,...). If somebody really want to try again,
	403	the extra args to add are :
	404	[A "-ccopt"; A "-link -Wl,-subsystem,windows"]
	405	Other solution: use the mkwinapp tool. *)
403	406
404	407	(** The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
405	408	Let's tweak that... *)

+1

-1

parsing/argextend.ml4 less more

145	145	(* an exception rather than returning a value; *)
146	146	(* declares loc because some code can refer to it; *)
147	147	(* ensures loc is used to avoid "unused variable" warning *)
148		(true, <:expr< try Some $aux prods$ with [ _ -> None ] >>)
	148	(true, <:expr< try Some $aux prods$ with [ e when Errors.noncritical e -> None ] >>)
149	149	else
150	150	(* Static optimisation *)
151	151	(false, aux prods)

+1

-1

parsing/egrammar.ml less more

364	364	let with_grammar_rule_protection f x =
365	365	let fs = freeze () in
366	366	try let a = f x in unfreeze fs; a
367		with e -> unfreeze fs; raise e
	367	with reraise -> unfreeze fs; raise reraise

+1

-1

parsing/g_tactic.ml4 less more

125	125	let induction_arg_of_constr (c,lbind as clbind) =
126	126	if lbind = NoBindings then
127	127	try ElimOnIdent (constr_loc c,snd(coerce_to_id c))
128		with _ -> ElimOnConstr clbind
	128	with e when Errors.noncritical e -> ElimOnConstr clbind
129	129	else ElimOnConstr clbind
130	130
131	131	let mkTacCase with_evar = function

+2

-1

parsing/g_xml.ml4 less more

103	103
104	104	let get_xml_inductive_kn al =
105	105	inductive_of_cdata (* uriType apparent synonym of uri *)
106		(try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al)
	106	(try get_xml_attr "uri" al
	107	with e when Errors.noncritical e -> get_xml_attr "uriType" al)
107	108
108	109	let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
109	110

+5

-3

parsing/prettyp.ml less more

272	272
273	273	let print_inductive_renames =
274	274	print_args_data_of_inductive_ids
275		(fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> [])
	275	(fun r ->
	276	try List.hd (Arguments_renaming.arguments_names r)
	277	with e when Errors.noncritical e -> [])
276	278	((<>) Anonymous)
277	279	print_renames_list
278	280

736	738	let index_of_class cl =
737	739	try
738	740	fst (class_info cl)
739		with _ ->
	741	with e when Errors.noncritical e ->
740	742	errorlabstrm "index_of_class"
741	743	(pr_class cl ++ spc() ++ str "not a defined class.")
742	744

746	748	let p =
747	749	try
748	750	lookup_path_between_class (i,j)
749		with _ ->
	751	with e when Errors.noncritical e ->
750	752	errorlabstrm "index_cl_of_id"
751	753	(str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
752	754	++ str ".")

+61

-4

parsing/printer.ml less more

23	23	open Ppconstr
24	24	open Constrextern
25	25	open Tacexpr
	26	open Declarations
26	27
27	28	open Store.Field
28	29

116	117	let pr_sort s = pr_glob_sort (extern_sort s)
117	118
118	119	let _ = Termops.set_print_constr pr_lconstr_env
	120
	121
	122	(** Term printers resilient to [Nametab] errors *)
	123
	124	(** When the nametab isn't up-to-date, the term printers above
	125	could raise [Not_found] during [Nametab.shortest_qualid_of_global].
	126	In this case, we build here a fully-qualified name based upon
	127	the kernel modpath and label of constants, and the idents in
	128	the [mutual_inductive_body] for the inductives and constructors
	129	(needs an environment for this). *)
	130
	131	let id_of_global env = function
	132	\| ConstRef kn -> id_of_label (con_label kn)
	133	\| IndRef (kn,0) -> id_of_label (mind_label kn)
	134	\| IndRef (kn,i) ->
	135	(Environ.lookup_mind kn env).mind_packets.(i).mind_typename
	136	\| ConstructRef ((kn,i),j) ->
	137	(Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
	138	\| VarRef v -> v
	139
	140	let cons_dirpath id dp = make_dirpath (id :: repr_dirpath dp)
	141
	142	let rec dirpath_of_mp = function
	143	\| MPfile sl -> sl
	144	\| MPbound uid -> make_dirpath [id_of_mbid uid]
	145	\| MPdot (mp,l) -> cons_dirpath (id_of_label l) (dirpath_of_mp mp)
	146
	147	let dirpath_of_global = function
	148	\| ConstRef kn -> dirpath_of_mp (con_modpath kn)
	149	\| IndRef (kn,_) \| ConstructRef ((kn,_),_) ->
	150	dirpath_of_mp (mind_modpath kn)
	151	\| VarRef _ -> empty_dirpath
	152
	153	let qualid_of_global env r =
	154	Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
	155
	156	let safe_gen f env c =
	157	let orig_extern_ref = Constrextern.get_extern_reference () in
	158	let extern_ref loc vars r =
	159	try orig_extern_ref loc vars r
	160	with e when Errors.noncritical e ->
	161	Libnames.Qualid (loc, qualid_of_global env r)
	162	in
	163	Constrextern.set_extern_reference extern_ref;
	164	try
	165	let p = f env c in
	166	Constrextern.set_extern_reference orig_extern_ref;
	167	p
	168	with e when Errors.noncritical e ->
	169	Constrextern.set_extern_reference orig_extern_ref;
	170	str "??"
	171
	172	let safe_pr_lconstr_env = safe_gen pr_lconstr_env
	173	let safe_pr_constr_env = safe_gen pr_constr_env
	174	let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t
	175	let safe_pr_constr t = safe_pr_constr_env (Global.env()) t
	176
119	177
120	178	(**********************************************************************)
121	179	(* Global references *)

388	446	\| None ->
389	447	let exl = Evarutil.non_instantiated sigma in
390	448	if exl = [] then
391		(str"No more subgoals."
	449	(str"No more subgoals." ++ fnl ()
392	450	++ emacs_print_dependent_evars sigma seeds)
393	451	else
394	452	let pei = pr_evars_int 1 exl in

414	472	v 0 (
415	473	int(List.length rest+1) ++ str" subgoals" ++
416	474	str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
417		++ goals
	475	++ goals ++ fnl ()
418	476	++ emacs_print_dependent_evars sigma seeds
419	477	)
420	478	\| g1::rest,a::l ->

588	646	str (string_of_mp mp ^ "." ^ string_of_label lab)
589	647	in
590	648	let safe_pr_ltype typ =
591		try str " : " ++ pr_ltype typ with _ -> mt ()
	649	try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt ()
592	650	in
593	651	let (vars,axioms,opaque) =
594	652	ContextObjectMap.fold (fun t typ r ->

646	704
647	705	(** Inductive declarations *)
648	706
649		open Declarations
650	707	open Termops
651	708	open Reduction
652	709	open Inductive

+11

-0

parsing/printer.mli less more

29	29
30	30	val pr_constr_env : env -> constr -> std_ppcmds
31	31	val pr_constr : constr -> std_ppcmds
	32
	33	(** Same, but resilient to [Nametab] errors. Prints fully-qualified
	34	names when [shortest_qualid_of_global] has failed. Prints "??"
	35	in case of remaining issues (such as reference not in env). *)
	36
	37	val safe_pr_lconstr_env : env -> constr -> std_ppcmds
	38	val safe_pr_lconstr : constr -> std_ppcmds
	39
	40	val safe_pr_constr_env : env -> constr -> std_ppcmds
	41	val safe_pr_constr : constr -> std_ppcmds
	42
32	43
33	44	val pr_open_constr_env : env -> open_constr -> std_ppcmds
34	45	val pr_open_constr : open_constr -> std_ppcmds

+40

-19

parsing/printmod.ml less more

67	67	with
68	68	Not_found -> print_modpath locals kn
69	69
	70	(** Each time we have to print a non-globally visible structure,
	71	we place its elements in a fake fresh namespace. *)
	72
	73	let mk_fake_top =
	74	let r = ref 0 in
	75	fun () -> incr r; id_of_string ("FAKETOP"^(string_of_int !r))
	76
70	77	let nametab_register_dir mp =
71		let id = id_of_string "FAKETOP" in
72		let fp = Libnames.make_path empty_dirpath id in
	78	let id = mk_fake_top () in
73	79	let dir = make_dirpath [id] in
74		Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
75		fp
	80	Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)))
76	81
77	82	(** Nota: the [global_reference] we register in the nametab below
78	83	might differ from internal ones, since we cannot recreate here

80	85	the user names. This works nonetheless since we search now
81	86	[Nametab.the_globrevtab] modulo user name. *)
82	87
83		let nametab_register_body mp fp (l,body) =
	88	let nametab_register_body mp dir (l,body) =
84	89	let push id ref =
85		Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref
	90	Nametab.push (Nametab.Until (1+List.length (repr_dirpath dir)))
	91	(make_path dir id) ref
86	92	in
87	93	match body with
88	94	\| SFBmodule _ -> () (* TODO *)

97	103	Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1)))
98	104	mip.mind_consnames)
99	105	mib.mind_packets
	106
	107	let nametab_register_module_body mp struc =
	108	(* If [mp] is a globally visible module, we simply import it *)
	109	try Declaremods.really_import_module mp
	110	with Not_found ->
	111	(* Otherwise we try to emulate an import by playing with nametab *)
	112	nametab_register_dir mp;
	113	List.iter (nametab_register_body mp empty_dirpath) struc
	114
	115	let nametab_register_module_param mbid seb =
	116	(* For algebraic seb, we use a Declaremods function that converts into mse *)
	117	try Declaremods.process_module_seb_binding mbid seb
	118	with e when Errors.noncritical e ->
	119	(* Otherwise, for expanded structure, we try to play with the nametab *)
	120	match seb with
	121	\| SEBstruct struc ->
	122	let mp = MPbound mbid in
	123	let dir = make_dirpath [id_of_mbid mbid] in
	124	nametab_register_dir mp;
	125	List.iter (nametab_register_body mp dir) struc
	126	\| _ -> ()
100	127
101	128	let print_body is_impl env mp (l,body) =
102	129	let name = str (string_of_label l) in

125	152	try
126	153	let env = Option.get env in
127	154	Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib
128		with _ ->
	155	with e when Errors.noncritical e ->
129	156	(if mib.mind_finite then str "Inductive " else str "CoInductive")
130	157	++ name)
131	158
132	159	let print_struct is_impl env mp struc =
133		begin
134		(* If [mp] is a globally visible module, we simply import it *)
135		try Declaremods.really_import_module mp
136		with _ ->
137		(* Otherwise we try to emulate an import by playing with nametab *)
138		let fp = nametab_register_dir mp in
139		List.iter (nametab_register_body mp fp) struc
140		end;
141	160	prlist_with_sep spc (print_body is_impl env mp) struc
142	161
143	162	let rec flatten_app mexpr l = match mexpr with

155	174	let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
156	175	let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals
157	176	in
158		(try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
	177	nametab_register_module_param mbid seb1;
159	178	hov 2 (str "Funsig" ++ spc () ++ str "(" ++
160	179	pr_id (id_of_mbid mbid) ++ str ":" ++
161	180	print_modtype env mp1 locals seb1 ++

163	182	\| SEBstruct (sign) ->
164	183	let env' = Option.map
165	184	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
	185	nametab_register_module_body mp sign;
166	186	hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
167	187	brk (1,-2) ++ str "End")
168	188	\| SEBapply _ ->

189	209	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
190	210	let typ = Option.default mty.typ_expr mty.typ_expr_alg in
191	211	let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
192		(try Declaremods.process_module_seb_binding mbid typ with _ -> ());
	212	nametab_register_module_param mbid typ;
193	213	hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
194	214	str ":" ++ print_modtype env mp' locals typ ++
195	215	str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
196	216	\| SEBstruct struc ->
197	217	let env' = Option.map
198	218	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
	219	nametab_register_module_body mp struc;
199	220	hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
200	221	brk (1,-2) ++ str "End")
201	222	\| SEBapply _ ->

242	263	try
243	264	if !short then raise ShortPrinting;
244	265	print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
245		with _ ->
	266	with e when Errors.noncritical e ->
246	267	print_module' None mp with_body me ++ fnl ()
247	268
248	269	let print_modtype kn =

253	274	(try
254	275	if !short then raise ShortPrinting;
255	276	print_modtype' (Some (Global.env ())) kn mtb.typ_expr
256		with _ ->
	277	with e when Errors.noncritical e ->
257	278	print_modtype' None kn mtb.typ_expr))

+2

-2

parsing/tacextend.ml4 less more

187	187	Tacexpr.TacExtend($default_loc$,$se$,l)))
188	188	\| None -> () ])
189	189	$atomic_tactics$
190		with e ->
	190	with [ e when Errors.noncritical e ->
191	191	Pp.msg_warning
192	192	(Stream.iapp
193	193	(Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
194		(Errors.print e));
	194	(Errors.print e)) ];
195	195	Egrammar.extend_tactic_grammar $se$ $gl$;
196	196	List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
197	197	])

+2

-2

parsing/vernacextend.ml4 less more

54	54	declare_str_items loc
55	55	[ <:str_item< do {
56	56	try Vernacinterp.vinterp_add $se$ $funcl$
57		with e ->
	57	with [ e when Errors.noncritical e ->
58	58	Pp.msg_warning
59	59	(Stream.iapp
60	60	(Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
61		(Errors.print e));
	61	(Errors.print e)) ];
62	62	Egrammar.extend_vernac_command_grammar $se$ $nt$ $gl$
63	63	} >> ]
64	64

+3

-4

plugins/cc/ccalgo.ml less more

403	403	let build_subst uf subst =
404	404	Array.map (fun i ->
405	405	try term uf i
406		with _ -> anomaly "incomplete matching") subst
	406	with e when Errors.noncritical e ->
	407	anomaly "incomplete matching") subst
407	408
408	409	let rec inst_pattern subst = function
409	410	PVar i ->

729	730	let new_state_var typ state =
730	731	let id = pf_get_new_id __eps__ state.gls in
731	732	let {it=gl ; sigma=sigma} = state.gls in
732		let new_hyps =
733		Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in
734		let gls = Goal.V82.new_goal_with sigma gl new_hyps in
	733	let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
735	734	state.gls<- gls;
736	735	id
737	736

+3

-1

plugins/cc/cctac.ml less more

128	128
129	129	let patterns_of_constr env sigma nrels term=
130	130	let f,args=
131		try destApp (whd_delta env term) with _ -> raise Not_found in
	131	try destApp (whd_delta env term)
	132	with e when Errors.noncritical e -> raise Not_found
	133	in
132	134	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
133	135	then
134	136	let patt1,rels1 = pattern_of_constr env sigma args.(1)

+2

-2

plugins/decl_mode/decl_mode.ml less more

74	74	Mode_proof
75	75
76	76	let get_current_mode () =
77		try
	77	try
78	78	mode_of_pftreestate (Pfedit.get_pftreestate ())
79		with _ -> Mode_none
	79	with e when Errors.noncritical e -> Mode_none
80	80
81	81	let check_not_proof_mode str =
82	82	if get_current_mode () = Mode_proof then

+6

-3

plugins/decl_mode/decl_proof_instr.ml less more

380	380	se.se_meta submetas se.se_meta_list}
381	381	else
382	382	dfs (pred n)
383		with _ ->
	383	with e when Errors.noncritical e ->
384	384	begin
385	385	enstack_subsubgoals env se stack gls;
386	386	dfs n

518	518
519	519	let instr_rew _thus rew_side cut gls0 =
520	520	let last_id =
521		try get_last (pf_env gls0) with _ -> error "No previous equality." in
	521	try get_last (pf_env gls0)
	522	with e when Errors.noncritical e ->
	523	error "No previous equality."
	524	in
522	525	let typ,lhs,rhs = decompose_eq last_id gls0 in
523	526	let items_tac gls =
524	527	match cut.cut_by with

848	851	let ind =
849	852	try
850	853	destInd hd
851		with _ ->
	854	with e when Errors.noncritical e ->
852	855	error "Case analysis must be done on an inductive object." in
853	856	let mind,oind = Global.lookup_inductive ind in
854	857	let nparams,index =

+11

-7

plugins/extraction/extract_env.ml less more

396	396	in
397	397	let id =
398	398	if lang () <> Haskell then default_id
399		else try id_of_string (Filename.basename f)
400		with _ -> error "Extraction: provided filename is not a valid identifier"
	399	else
	400	try id_of_string (Filename.basename f)
	401	with e when Errors.noncritical e ->
	402	error "Extraction: provided filename is not a valid identifier"
401	403	in
402	404	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
403	405

472	474	msg_with ft (d.preamble mo opened unsafe_needs);
473	475	msg_with ft (d.pp_struct struc);
474	476	Option.iter close_out cout;
475		with e ->
476		Option.iter close_out cout; raise e
	477	with reraise ->
	478	Option.iter close_out cout; raise reraise
477	479	end;
478	480	if not dry then Option.iter info_file fn;
479	481	(* Now, let's print the signature *)

486	488	msg_with ft (d.sig_preamble mo opened unsafe_needs);
487	489	msg_with ft (d.pp_sig (signature_of_structure struc));
488	490	close_out cout;
489		with e ->
490		close_out cout; raise e
	491	with reraise ->
	492	close_out cout; raise reraise
491	493	end;
492	494	info_file si)
493	495	(if dry then None else si);

526	528	\| r::l ->
527	529	let q = snd (qualid_of_reference r) in
528	530	let mpo = try Some (Nametab.locate_module q) with Not_found -> None
529		and ro = try Some (Smartlocate.global_with_alias r) with _ -> None
	531	and ro =
	532	try Some (Smartlocate.global_with_alias r)
	533	with e when Errors.noncritical e -> None
530	534	in
531	535	match mpo, ro with
532	536	\| None, None -> Nametab.error_global_not_found q

+2

-2

plugins/extraction/extraction.ml less more

148	148	(fun i ->
149	149	assert ((0 < i) && (i <= n));
150	150	MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
151		with _ -> MLexn s)
	151	with e when Errors.noncritical e -> MLexn s)
152	152	\| a -> ast_map (handle_exn r n fn_name) a
153	153
154	154	(S Management of type variable contexts. )

682	682	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
683	683	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
684	684	else mla
685		with _ -> mla
	685	with e when Errors.noncritical e -> mla
686	686	in
687	687	(* For strict languages, purely logical signatures with at least
688	688	one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left

+3

-1

plugins/extraction/haskell.ml less more

80	80	let rec pp_type par vl t =
81	81	let rec pp_rec par = function
82	82	\| Tmeta _ \| Tvar' _ -> assert false
83		\| Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
	83	\| Tvar i ->
	84	(try pr_id (List.nth vl (pred i))
	85	with e when Errors.noncritical e -> (str "a" ++ int i))
84	86	\| Tglob (r,[]) -> pp_global Type r
85	87	\| Tglob (IndRef(kn,0),l)
86	88	when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->

+2

-2

plugins/extraction/mlutil.ml less more

878	878	(try
879	879	ignore (int_of_string (String.sub s n (String.length s - n)));
880	880	String.sub s 0 n = br
881		with _ -> false)
	881	with e when Errors.noncritical e -> false)
882	882	\| Tmp _ \| Dummy -> false
883	883
884	884	let expand_linear_let o id e =

1311	1311	let c = match r with ConstRef c -> c \| _ -> assert false in
1312	1312	let has_body =
1313	1313	try constant_has_body (Global.lookup_constant c)
1314		with _ -> false
	1314	with e when Errors.noncritical e -> false
1315	1315	in
1316	1316	has_body &&
1317	1317	(let t1 = eta_red t in

+3

-2

plugins/extraction/ocaml.ml less more

118	118	let rec pp_rec par = function
119	119	\| Tmeta _ \| Tvar' _ \| Taxiom -> assert false
120	120	\| Tvar i -> (try pp_tvar (List.nth vl (pred i))
121		with _ -> (str "'a" ++ int i))
	121	with e when Errors.noncritical e ->
	122	(str "'a" ++ int i))
122	123	\| Tglob (r,[a1;a2]) when is_infix r ->
123	124	pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
124	125	\| Tglob (r,[]) -> pp_global Type r

187	188	let args = list_skipn (projection_arity r) args in
188	189	let record = List.hd args in
189	190	pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
190		with _ -> apply (pp_global Term r))
	191	with e when Errors.noncritical e -> apply (pp_global Term r))
191	192	\| MLfix (i,ids,defs) ->
192	193	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
193	194	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args

+3

-3

plugins/extraction/table.ml less more

254	254
255	255	let string_of_global r =
256	256	try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
257		with _ -> string_of_id (safe_basename_of_global r)
	257	with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r)
258	258
259	259	let safe_pr_global r = str (string_of_global r)
260	260

262	262
263	263	let safe_pr_long_global r =
264	264	try Printer.pr_global r
265		with _ -> match r with
	265	with e when Errors.noncritical e -> match r with
266	266	\| ConstRef kn ->
267	267	let mp,_,l = repr_con kn in
268	268	str ((string_of_mp mp)^"."^(string_of_label l))

451	451
452	452	(s Extraction AccessOpaque )
453	453
454		let access_opaque = my_bool_option "AccessOpaque" false
	454	let access_opaque = my_bool_option "AccessOpaque" true
455	455
456	456	(s Extraction AutoInline )
457	457

+1

-1

plugins/firstorder/g_ground.ml4 less more

84	84	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
85	85	let result=ground_tac solver startseq gl in
86	86	qflag:=backup;result
87		with e ->qflag:=backup;raise e
	87	with reraise ->qflag:=backup;raise reraise
88	88
89	89	(* special for compatibility with Intuition
90	90

+1

-1

plugins/firstorder/instances.ml less more

128	128	\| _-> anomaly "can't happen" in
129	129	let ntt=try
130	130	Pretyping.Default.understand evmap env (raux m rawt)
131		with _ ->
	131	with e when Errors.noncritical e ->
132	132	error "Untypable instance, maybe higher-order non-prenex quantification" in
133	133	decompose_lam_n_assum m ntt
134	134

+1

-1

plugins/fourier/fourier.ml less more

174	174	raise (Failure "contradiction found"))
175	175	\|_->assert false)
176	176	lr)
177		with _ -> ());
	177	with e when Errors.noncritical e -> ());
178	178	!res
179	179	;;
180	180

+11

-7

plugins/fourier/fourierR.ml less more

39	39
40	40	let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
41	41
42		let flin_coef f x = try (Constrhash.find f.fhom x) with _-> r0;;
	42	let flin_coef f x = try (Constrhash.find f.fhom x) with Not_found -> r0;;
43	43
44	44	let flin_add f x c =
45	45	let cx = flin_coef f x in

140	140	(try (let a=(rational_of_constr args.(0)) in
141	141	try (let b = (rational_of_constr args.(1)) in
142	142	(flin_add_cste (flin_zero()) (rmult a b)))
143		with _-> (flin_add (flin_zero())
	143	with e when Errors.noncritical e ->
	144	(flin_add (flin_zero())
144	145	args.(1)
145	146	a))
146		with _-> (flin_add (flin_zero())
	147	with e when Errors.noncritical e ->
	148	(flin_add (flin_zero())
147	149	args.(0)
148	150	(rational_of_constr args.(1))))
149	151	\| "Rinv"->

153	155	(let b=(rational_of_constr args.(1)) in
154	156	try (let a = (rational_of_constr args.(0)) in
155	157	(flin_add_cste (flin_zero()) (rdiv a b)))
156		with _-> (flin_add (flin_zero())
	158	with e when Errors.noncritical e ->
	159	(flin_add (flin_zero())
157	160	args.(0)
158	161	(rinv b)))
159	162	\|_->assert false)

163	166	\|"R0" -> flin_zero ()
164	167	\|_-> assert false)
165	168	\|_-> assert false)
166		with _ -> flin_add (flin_zero())
	169	with e when Errors.noncritical e ->
	170	flin_add (flin_zero())
167	171	c
168	172	r1
169	173	;;

493	497	\|_->assert false)
494	498	\|_->assert false
495	499	in tac gl)
496		with _ ->
	500	with e when Errors.noncritical e ->
497	501	(* les hypothèses *)
498	502	let hyps = List.map (fun (h,t)-> (mkVar h,t))
499	503	(list_of_sign (pf_hyps gl)) in
500	504	let lineq =ref [] in
501	505	List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
502		with _ -> ())
	506	with e when Errors.noncritical e -> ())
503	507	hyps;
504	508	(* lineq = les inéquations découlant des hypothèses *)
505	509	if !lineq=[] then Util.error "No inequalities";

+15

-8

plugins/funind/functional_principles_proofs.ml less more

32	32
33	33	let do_observe_tac s tac g =
34	34	try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
35		with e ->
36		let e = Cerrors.process_vernac_interp_error e in
37		let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
	35	with reraise ->
	36	let e = Cerrors.process_vernac_interp_error reraise in
	37	let goal =
	38	try (Printer.pr_goal g)
	39	with e when Errors.noncritical e -> assert false
	40	in
38	41	msgnl (str "observation "++ s++str " raised exception " ++
39	42	Errors.print e ++ str " on goal " ++ goal );
40	43	raise e;;

118	121	eq_constr t1 t2 && eq_constr a1 a2
119	122	\| _ -> false
120	123	end
121		with _ -> false
	124	with e when Errors.noncritical e -> false
122	125	in
123	126	(* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
124	127	res

144	147	(eq_constr u1 u2 &&
145	148	incompatible_constructor_terms t1 t2)
146	149	\| _ -> false
147		with _ -> false
	150	with e when Errors.noncritical e -> false
148	151	in
149	152	if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
150	153	res

231	234	then
232	235	(jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
233	236	else nochange "not an equality"
234		with _ -> nochange "not an equality"
	237	with e when Errors.noncritical e -> nochange "not an equality"
235	238	in
236	239	if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
237	240	let rec compute_substitution sub t1 t2 =

607	610	let my_orelse tac1 tac2 g =
608	611	try
609	612	tac1 g
610		with e ->
	613	with e when Errors.noncritical e ->
611	614	(* observe (str "using snd tac since : " ++ Errors.print e); *)
612	615	tac2 g
613	616

1211	1214	let ctxt,pte_app = (decompose_prod_assum (pf_concl gl)) in
1212	1215	let pte,pte_args = (decompose_app pte_app) in
1213	1216	try
1214		let pte = try destVar pte with _ -> anomaly "Property is not a variable" in
	1217	let pte =
	1218	try destVar pte
	1219	with e when Errors.noncritical e ->
	1220	anomaly "Property is not a variable"
	1221	in
1215	1222	let fix_info = Idmap.find pte ptes_to_fix in
1216	1223	let nb_args = fix_info.nb_realargs in
1217	1224	tclTHENSEQ

+5

-8

plugins/funind/functional_principles_types.ml less more

301	301	"defined"
302	302	((try
303	303	str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl ()
304		with _ -> mt ()
	304	with e when Errors.noncritical e -> mt ()
305	305	) ++msg)
306		\| e -> raise e
307
308
309	306
310	307	let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
311	308	(* First we get the type of the old graph principle *)

400	397	Don't forget to close the goal if an error is raised !!!!
401	398	*)
402	399	save false new_princ_name entry g_kind hook
403		with e ->
	400	with e when Errors.noncritical e ->
404	401	begin
405	402	begin
406	403	try

412	409	then Pfedit.delete_current_proof ()
413	410	else ()
414	411	else ()
415		with _ -> ()
	412	with e when Errors.noncritical e -> ()
416	413	end;
417	414	raise (Defining_principle e)
418	415	end

553	550	0
554	551	(prove_princ_for_struct false 0 (Array.of_list funs))
555	552	(fun _ _ _ -> ())
556		with e ->
	553	with e when Errors.noncritical e ->
557	554	begin
558	555	begin
559	556	try

565	562	then Pfedit.delete_current_proof ()
566	563	else ()
567	564	else ()
568		with _ -> ()
	565	with e when Errors.noncritical e -> ()
569	566	end;
570	567	raise (Defining_principle e)
571	568	end

+2

-2

plugins/funind/g_indfun.ml4 less more

207	207	try Functional_principles_types.build_scheme fas
208	208	with Functional_principles_types.No_graph_found ->
209	209	Util.error ("Cannot generate induction principle(s)")
210		\| e ->
	210	\| e when Errors.noncritical e ->
211	211	let names = List.map (fun (_,na,_) -> na) fas in
212	212	warning_error names e
213	213
214	214	end
215	215	\| _ -> assert false (* we can only have non empty list *)
216	216	end
217		\| e ->
	217	\| e when Errors.noncritical e ->
218	218	let names = List.map (fun (_,na,_) -> na) fas in
219	219	warning_error names e
220	220	end

+9

-8

plugins/funind/glob_term_to_relation.ml less more

947	947	try
948	948	observe (str "computing new type for eq : " ++ pr_glob_constr rt);
949	949	let t' =
950		try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue
	950	try Pretyping.Default.understand Evd.empty env t
	951	with e when Errors.noncritical e -> raise Continue
951	952	in
952	953	let is_in_b = is_free_in id b in
953	954	let _keep_eq =

1246	1247	l := param::!l
1247	1248	)
1248	1249	rels_params.(0)
1249		with _ ->
	1250	with e when Errors.noncritical e ->
1250	1251	()
1251	1252	in
1252	1253	List.rev !l

1452	1453	in
1453	1454	observe (msg);
1454	1455	raise e
1455		\| e ->
	1456	\| reraise ->
1456	1457	let _time3 = System.get_time () in
1457	1458	(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
1458	1459	let repacked_rel_inds =

1463	1464	str "while trying to define"++ spc () ++
1464	1465	Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
1465	1466	++ fnl () ++
1466		Errors.print e
	1467	Errors.print reraise
1467	1468	in
1468	1469	observe msg;
1469		raise e
	1470	raise reraise
1470	1471
1471	1472
1472	1473
1473	1474	let build_inductive funnames funsargs returned_types rtl =
1474	1475	try
1475	1476	do_build_inductive funnames funsargs returned_types rtl
1476		with e -> raise (Building_graph e)
1477
1478
	1477	with e when Errors.noncritical e -> raise (Building_graph e)
	1478
	1479

+4

-2

plugins/funind/glob_termops.ml less more

533	533	else
534	534	let eqs' =
535	535	try ((List.combine cpl1 cpl2)@eqs)
536		with _ -> anomaly "are_unifiable_aux"
	536	with e when Errors.noncritical e ->
	537	anomaly "are_unifiable_aux"
537	538	in
538	539	are_unifiable_aux eqs'
539	540

555	556	else
556	557	let eqs' =
557	558	try ((List.combine cpl1 cpl2)@eqs)
558		with _ -> anomaly "eq_cases_pattern_aux"
	559	with e when Errors.noncritical e ->
	560	anomaly "eq_cases_pattern_aux"
559	561	in
560	562	eq_cases_pattern_aux eqs'
561	563	\| _ -> raise NotUnifiable

+7

-7

plugins/funind/indfun.ml less more

81	81	List.fold_right
82	82	(fun a acc ->
83	83	try Idset.add (destVar a) acc
84		with _ -> acc
	84	with e when Errors.noncritical e -> acc
85	85	)
86	86	args
87	87	Idset.empty

165	165	sigma rec_sign rec_impls def
166	166	)
167	167	lnameargsardef
168		with e ->
169		States.unfreeze fs; raise e in
	168	with reraise ->
	169	States.unfreeze fs; raise reraise in
170	170	States.unfreeze fs; def
171	171	in
172	172	recdef,rec_impls

250	250	(fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
251	251	fix_names
252	252	)
253		with e ->
	253	with e when Errors.noncritical e ->
254	254	let e' = Cerrors.process_vernac_interp_error e in
255	255	msg_warning
256	256	(str "Cannot build inversion information" ++
257	257	if do_observe () then (fnl() ++ Errors.print e') else mt ())
258		with _ -> ()
	258	with e when Errors.noncritical e -> ()
259	259
260	260	let warning_error names e =
261	261	let e = Cerrors.process_vernac_interp_error e in

345	345	Array.iter (add_Function is_general) funs_kn;
346	346	()
347	347	end
348		with e ->
	348	with e when Errors.noncritical e ->
349	349	on_error names e
350	350
351	351	let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =

412	412	functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
413	413	);
414	414	derive_inversion [fname]
415		with e ->
	415	with e when Errors.noncritical e ->
416	416	(* No proof done *)
417	417	()
418	418	in

+9

-9

plugins/funind/indfun_common.ml less more

54	54	f x
55	55	with
56	56	\| Not_found -> raise (Util.UserError("", msg))
57		\| e -> raise e
58	57
59	58
60	59	let filter_map filter f =

122	121	(try (match Declarations.body_of_constant (Global.lookup_constant sp) with
123	122	\| Some c -> Declarations.force c
124	123	\| _ -> assert false)
125		with _ -> assert false)
	124	with e when Errors.noncritical e -> assert false)
126	125	\|_ -> assert false
127	126
128	127	let coq_constant s =

214	213	Dumpglob.continue ();
215	214	res
216	215	with
217		\| e ->
	216	\| reraise ->
218	217	Impargs.make_implicit_args old_implicit_args;
219	218	Impargs.make_strict_implicit_args old_strict_implicit_args;
220	219	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
221	220	Flags.raw_print := old_rawprint;
222	221	Dumpglob.continue ();
223		raise e
	222	raise reraise
224	223
225	224
226	225

349	348	let pr_info f_info =
350	349	str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
351	350	str "function_constant_type := " ++
352		(try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
	351	(try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant))
	352	with e when Errors.noncritical e -> mt ()) ++ fnl () ++
353	353	str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
354	354	str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
355	355	str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++

501	501	let init_constant dir s =
502	502	try
503	503	Coqlib.gen_constant "Function" dir s
504		with e -> raise (ToShow e)
	504	with e when Errors.noncritical e -> raise (ToShow e)
505	505
506	506	let jmeq () =
507	507	try
508	508	(Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
509	509	init_constant ["Logic";"JMeq"] "JMeq")
510		with e -> raise (ToShow e)
	510	with e when Errors.noncritical e -> raise (ToShow e)
511	511
512	512	let jmeq_rec () =
513	513	try
514	514	Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
515	515	init_constant ["Logic";"JMeq"] "JMeq_rec"
516		with e -> raise (ToShow e)
	516	with e when Errors.noncritical e -> raise (ToShow e)
517	517
518	518	let jmeq_refl () =
519	519	try
520	520	Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
521	521	init_constant ["Logic";"JMeq"] "JMeq_refl"
522		with e -> raise (ToShow e)
	522	with e when Errors.noncritical e -> raise (ToShow e)

+10

-7

plugins/funind/invfun.ml less more

58	58
59	59
60	60	let do_observe_tac s tac g =
61		let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
	61	let goal =
	62	try Printer.pr_goal g
	63	with e when Errors.noncritical e -> assert false
	64	in
62	65	try
63	66	let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
64		with e ->
65		let e' = Cerrors.process_vernac_interp_error e in
	67	with reraise ->
	68	let e' = Cerrors.process_vernac_interp_error reraise in
66	69	msgnl (str "observation "++ s++str " raised exception " ++
67	70	Errors.print e' ++ str " on goal " ++ goal );
68		raise e;;
	71	raise reraise;;
69	72
70	73
71	74	let observe_tac s tac g =

567	570	observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
568	571	]
569	572	\| _ -> reflexivity
570		with _ -> reflexivity
	573	with e when Errors.noncritical e -> reflexivity
571	574	in
572	575	let eq_ind = Coqlib.build_coq_eq () in
573	576	let discr_inject =

861	864	update_Function {finfo with completeness_lemma = Some lem_cst}
862	865	)
863	866	funs;
864		with e ->
	867	with reraise ->
865	868	(* In case of problem, we reset all the lemmas *)
866	869	Pfedit.delete_all_proofs ();
867	870	States.unfreeze previous_state;
868		raise e
	871	raise reraise
869	872
870	873
871	874

+3

-3

plugins/funind/merge.ml less more

69	69	let ans = CRef (Libnames.Ident (dummy_loc,id)) in
70	70	let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
71	71	true
72		with _ -> false
	72	with e when Errors.noncritical e -> false
73	73
74	74	(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
75	75	global env) with base [id]. *)

792	792
793	793	let params1 =
794	794	try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
795		with _ -> [] in
	795	with e when Errors.noncritical e -> [] in
796	796	let params2 =
797	797	try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
798		with _ -> [] in
	798	with e when Errors.noncritical e -> [] in
799	799
800	800	let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
801	801	let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in

+24

-13

plugins/funind/recdef.ml less more

93	93	let v = tac g in
94	94	ignore(Stack.pop debug_queue);
95	95	v
96		with e ->
	96	with reraise ->
97	97	if not (Stack.is_empty debug_queue)
98	98	then
99		print_debug_queue true e;
100		raise e
	99	print_debug_queue true reraise;
	100	raise reraise
101	101
102	102	let observe_tac s tac g =
103	103	if Tacinterp.get_debug () <> Tactic_debug.DebugOff

139	139	(try (match body_of_constant (Global.lookup_constant sp) with
140	140	\| Some c -> Declarations.force c
141	141	\| _ -> assert false)
142		with _ ->
	142	with e when Errors.noncritical e ->
143	143	anomaly ("Cannot find definition of constant "^
144	144	(string_of_id (id_of_label (con_label sp))))
145	145	)

379	379	(fun g1 ->
380	380	let ty_teq = pf_type_of g1 (mkVar teq) in
381	381	let teq_lhs,teq_rhs =
382		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
	382	let _,args =
	383	try destApp ty_teq
	384	with e when Errors.noncritical e ->
	385	Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false
	386	in
383	387	args.(1),args.(2)
384	388	in
385	389	cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1

700	704	(match find_call_occs nb_arg 0 f_constr expr with
701	705	_,[] ->
702	706	(try observe_tac "base_leaf" (base_leaf func eqs expr)
703		with e -> (msgerrnl (str "failure in base case");raise e ))
	707	with reraise ->
	708	(msgerrnl (str "failure in base case");raise reraise ))
704	709	\| _, _::_ ->
705	710	observe_tac "rec_leaf"
706	711	(rec_leaf is_mes acc_inv hrec func eqs expr)) in
707	712	v
708		with e -> begin msgerrnl(str "failure in proveterminate"); raise e end
	713	with reraise ->
	714	begin
	715	msgerrnl(str "failure in proveterminate");
	716	raise reraise
	717	end
709	718	in
710	719	proveterminate
711	720

930	939	let id_name = string_of_id id in
931	940	try
932	941	String.sub id_name 0 (String.length rec_res_name) = rec_res_name
933		with _ -> false
	942	with e when Errors.noncritical e -> false
934	943
935	944	let clear_goals =
936	945	let rec clear_goal t =

968	977	\| Some s -> s
969	978	\| None ->
970	979	try (add_suffix current_proof_name "_subproof")
971		with _ -> anomaly "open_new_goal with an unamed theorem"
	980	with e when Errors.noncritical e ->
	981	anomaly "open_new_goal with an unamed theorem"
972	982	in
973	983	let sign = initialize_named_context_for_proof () in
974	984	let na = next_global_ident_away name [] in

1438	1448	let stop = ref false in
1439	1449	begin
1440	1450	try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
1441		with e ->
	1451	with e when Errors.noncritical e ->
1442	1452	begin
1443	1453	if Tacinterp.get_debug () <> Tactic_debug.DebugOff
1444	1454	then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)

1473	1483	using_lemmas
1474	1484	(List.length res_vars)
1475	1485	hook
1476		with e ->
	1486	with reraise ->
1477	1487	begin
1478		(try ignore (Backtrack.backto previous_label) with _ -> ());
	1488	(try ignore (Backtrack.backto previous_label)
	1489	with e when Errors.noncritical e -> ());
1479	1490	(* anomaly "Cannot create termination Lemma" *)
1480		raise e
	1491	raise reraise
1481	1492	end

+4

-3

plugins/micromega/certificate.ml less more

330	330	\| Inr _ -> None
331	331	\| Inl cert -> Some (rats_to_ints (Vect.to_list cert))
332	332	(* should not use rats_to_ints *)
333		with x ->
	333	with x when Errors.noncritical x ->
334	334	if debug
335	335	then (Printf.printf "raw certificate %s" (Printexc.to_string x);
336	336	flush stdout) ;

376	376
377	377
378	378	let linear_prover n_spec l =
379		try linear_prover n_spec l with
380		x -> (print_string (Printexc.to_string x); None)
	379	try linear_prover n_spec l
	380	with x when x <> Sys.Break ->
	381	(print_string (Printexc.to_string x); None)
381	382
382	383	let linear_prover_with_cert spec l =
383	384	match linear_prover spec l with

+15

-9

plugins/micromega/coq_micromega.ml less more

936	936	let (expr,env) = parse_expr env args.(0) in
937	937	let power = (parse_exp expr args.(1)) in
938	938	(power , env)
939		with _ -> (* if the exponent is a variable *)
	939	with e when e <> Sys.Break ->
	940	(* if the exponent is a variable *)
940	941	let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
941	942	end
942	943	\| Ukn s ->

1111	1112
1112	1113	let parse_formula parse_atom env tg term =
1113	1114
1114		let parse_atom env tg t = try let (at,env) = parse_atom env t in
1115		(A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
	1115	let parse_atom env tg t =
	1116	try
	1117	let (at,env) = parse_atom env t in
	1118	(A(at,tg,t), env,Tag.next tg)
	1119	with e when e <> Sys.Break -> (X(t),env,tg)
	1120	in
1116	1121
1117	1122	let rec xparse_formula env tg term =
1118	1123	match kind_of_term term with

1188	1193	let rec xsame_proof sg =
1189	1194	match sg with
1190	1195	\| [] -> true
1191		\| n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false)
	1196	\| n::sg ->
	1197	(try List.nth cl1 n = List.nth cl2 n with e when e <> Sys.Break -> false)
1192	1198	&& (xsame_proof sg ) in
1193	1199	xsame_proof sg
1194	1200

1252	1258	let btree_of_array typ a =
1253	1259	try
1254	1260	btree_of_array typ a
1255		with x ->
	1261	with x when x <> Sys.Break ->
1256	1262	failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
1257	1263
1258	1264	let dump_varmap typ env =

1321	1327	try
1322	1328	let (c,env,tg) = parse_formula parse_arith env tg t in
1323	1329	((i,c)::lhyps, env,tg)
1324		with _ -> (lhyps,env,tg)
	1330	with e when e <> Sys.Break -> (lhyps,env,tg)
1325	1331	((if debug then Printf.printf "parse_arith : %s\n" x);)
1326	1332
1327	1333

1465	1471	(pp_ml_list prover.pp_f) (List.map fst new_cl) ;
1466	1472	flush stdout
1467	1473	end ; *)
1468		let res = try prover.compact prf remap with x ->
	1474	let res = try prover.compact prf remap with x when x <> Sys.Break ->
1469	1475	if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
1470	1476	(* This should not happen -- this is the recovery plan... *)
1471	1477	match prover.prover (List.map fst new_cl) with

2030	2036	try
2031	2037	micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
2032	2038	[ linear_Z ] gl
2033		with z -> (Printexc.print_backtrace stdout ;) raise z
	2039	with reraise -> (Printexc.print_backtrace stdout ;) raise reraise
2034	2040
2035	2041	let xnlia gl =
2036	2042	try
2037	2043	micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
2038	2044	[ nlinear_Z ] gl
2039		with z -> (Printexc.print_backtrace stdout ;) raise z
	2045	with reraise -> (Printexc.print_backtrace stdout ;) raise reraise
2040	2046
2041	2047
2042	2048

+3

-3

plugins/micromega/csdpcert.ml less more

149	149	S (Some proof)
150	150	with
151	151	\| Sos_lib.TooDeep -> S None
152		\| x -> F (Printexc.to_string x)
	152	\| x when x <> Sys.Break -> F (Printexc.to_string x)
153	153
154	154	(* This is somewhat buggy, over Z, strict inequality vanish... *)
155	155	let pure_sos l =

173	173	S (Some proof)
174	174	with
175	175	(* \| Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *)
176		\| x -> (* May be that could be refined *) S None
	176	\| x when x <> Sys.Break -> (* May be that could be refined *) S None
177	177
178	178
179	179

202	202	Marshal.to_channel chan (cert:csdp_certificate) [] ;
203	203	flush chan ;
204	204	exit 0
205		with x -> (Printf.fprintf chan "error %s" (Printexc.to_string x) ; exit 1)
	205	with any -> (Printf.fprintf chan "error %s" (Printexc.to_string any) ; exit 1)
206	206
207	207	;;
208	208

+2

-1

plugins/micromega/mfourier.ml less more

727	727	try
728	728	Some (bound_of_variable IMap.empty fresh s.sys)
729	729	with
730		x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
	730	x when x <> Sys.Break ->
	731	Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
731	732
732	733
733	734	let find_point cstrs =

+7

-5

plugins/micromega/mutils.ml less more

28	28	try
29	29	let res = f () in
30	30	rst () ; res
31		with x ->
	31	with reraise ->
32	32	(try rst ()
33		with _ -> raise x
34		); raise x
	33	with any -> raise reraise
	34	); raise reraise
35	35
36	36	let map_option f x =
37	37	match x with

430	430	\| Unix.WEXITED 0 ->
431	431	let inch = Unix.in_channel_of_descr stdout_read in
432	432	begin try Marshal.from_channel inch
433		with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x))
	433	with x when x <> Sys.Break ->
	434	failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x))
434	435	end
435	436	\| Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
436	437	\| Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
437	438	\| Unix.WSTOPPED i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
438	439	(* Cleanup *)
439	440	(fun () ->
440		List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write])
	441	List.iter (fun x -> try Unix.close x with e when e <> Sys.Break -> ())
	442	[stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write])
441	443
442	444	(* Local Variables: *)
443	445	(* coding: utf-8 *)

+5

-5

plugins/micromega/persistent_cache.ml less more

81	81	try
82	82	let res = f () in
83	83	rst () ; res
84		with x ->
	84	with reraise ->
85	85	(try rst ()
86		with _ -> raise x
87		); raise x
	86	with any -> raise reraise
	87	); raise reraise
88	88
89	89
90	90	let read_key_elem inch =

92	92	Some (Marshal.from_channel inch)
93	93	with
94	94	\| End_of_file -> None
95		\| _ -> raise InvalidTableFormat
	95	\| e when e <> Sys.Break -> raise InvalidTableFormat
96	96
97	97	(** In win32, it seems that we should unlock the exact zone
98	98	that has been locked, and not the whole file *)

150	150	Table.iter
151	151	(fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
152	152	flush outch ;
153		with _ -> () )
	153	with e when e <> Sys.Break -> () )
154	154	;
155	155	unlock out ;
156	156	{ outch = outch ;

+3

-2

plugins/nsatz/ideal.ml less more

236	236
237	237	let getvar lv i =
238	238	try (nth lv i)
239		with _ -> (fold_left (fun r x -> r^" "^x) "lv= " lv)
	239	with e when Errors.noncritical e ->
	240	(fold_left (fun r x -> r^" "^x) "lv= " lv)
240	241	^" i="^(string_of_int i)
241	242
242	243	let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef

589	590	(* coef of q in p = sum_i c_iq_i )
590	591	let coefpoldep_find p q =
591	592	try (Hashtbl.find coefpoldep (p.num,q.num))
592		with _ -> []
	593	with Not_found -> []
593	594
594	595	let coefpoldep_remove p q =
595	596	Hashtbl.remove coefpoldep (p.num,q.num)

+2

-2

plugins/nsatz/polynom.ml less more

172	172	then failwith "raté")
173	173	p1;
174	174	true)
175		with _ -> false)
	175	with e when Errors.noncritical e -> false)
176	176	\| (_,_) -> false
177	177
178	178	(* normalize polynomial: remove head zeros, coefficients are normalized

523	523	q x in
524	524	(* degueulasse, mais c 'est pour enlever un warning *)
525	525	if s==s then true else true)
526		with _ -> false
	526	with e when Errors.noncritical e -> false
527	527
528	528	(***********************************************************************
529	529	5. Pseudo-division and gcd with subresultants.

+9

-7

plugins/nsatz/utile.ml less more

32	32
33	33	let memos s memoire nf f x =
34	34	try (let v = Hashtbl.find memoire (nf x) in pr s;v)
35		with _ -> (pr "#";
36		let v = f x in
37		Hashtbl.add memoire (nf x) v;
38		v)
	35	with e when Errors.noncritical e ->
	36	(pr "#";
	37	let v = f x in
	38	Hashtbl.add memoire (nf x) v;
	39	v)
39	40
40	41
41	42	(**********************************************************************

63	64	if not (constant r)
64	65	then l1:=r::(!l1)
65	66	else p_dans_lmin:=true)
66		with _ -> ())
	67	with e when Errors.noncritical e -> ())
67	68	lmin;
68	69	if !p_dans_lmin
69	70	then factor lmin lp1

74	75	List.iter (fun q -> try (let r = div q p in
75	76	if not (constant r)
76	77	then l1:=r::(!l1))
77		with _ -> lmin1:=q::(!lmin1))
	78	with e when Errors.noncritical e ->
	79	lmin1:=q::(!lmin1))
78	80	lmin;
79	81	factor (List.rev (p::(!lmin1))) !l1)
80	82	(* au moins un q de lmin divise p non trivialement *)

104	106	li:=j::(!li);
105	107	r:=rr;
106	108	done)
107		with _ -> ())
	109	with e when Errors.noncritical e -> ())
108	110	l1;
109	111	res.(i)<-(!r,!li))
110	112	f;

+3

-2

plugins/omega/coq_omega.ml less more

884	884	try
885	885	let v,th,_ = find_constr t' in
886	886	[clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
887		with _ ->
	887	with e when Errors.noncritical e ->
888	888	let v = new_identifier_var ()
889	889	and th = new_identifier () in
890	890	hide_constr t' v th isnat;

923	923	\| _ -> default false t
924	924	end
925	925	\| Kapp((Zpos\|Zneg\|Z0),_) ->
926		(try ([],Oz(recognize_number t)) with _ -> default false t)
	926	(try ([],Oz(recognize_number t))
	927	with e when Errors.noncritical e -> default false t)
927	928	\| Kvar s -> [],Oatom s
928	929	\| Kapp(Zopp,[t]) ->
929	930	let tac,t' = transform (P_APP 1 :: p) t in

+4

-1

plugins/quote/quote.ml less more

220	220	(s Now the function [compute_ivs] itself )
221	221
222	222	let compute_ivs gl f cs =
223		let cst = try destConst f with _ -> i_can't_do_that () in
	223	let cst =
	224	try destConst f
	225	with e when Errors.noncritical e -> i_can't_do_that ()
	226	in
224	227	let body = Environ.constant_value (Global.env()) cst in
225	228	match decomp_term body with
226	229	\| Fix(([\| len \|], 0), ([\| name \|], [\| typ \|], [\| body2 \|])) ->

+2

-1

plugins/ring/ring.ml less more

291	291	(* Protects the convertibility test against undue exceptions when using it
292	292	with untyped terms *)
293	293
294		let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false
	294	let safe_pf_conv_x gl c1 c2 =
	295	try pf_conv_x gl c1 c2 with e when Errors.noncritical e -> false
295	296
296	297
297	298	(* Add a Ring or a Semi-Ring to the database after a type verification *)

+2

-2

plugins/romega/const_omega.ml less more

334	334	\| Kapp("Z.succ",[t]) -> Tsucc t
335	335	\| Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
336	336	\| Kapp(("Zpos"\|"Zneg"\|"Z0"),_) ->
337		(try Tnum (recognize t) with _ -> Tother)
	337	(try Tnum (recognize t) with e when Errors.noncritical e -> Tother)
338	338	\| _ -> Tother
339	339	with e when Logic.catchable_exception e -> Tother
340	340

356	356	\| Kapp(("Z.opp"\|"Z.succ"\|"Z.pred"),[t]) -> aux t
357	357	\| Kapp(("Zpos"\|"Zneg"\|"Z0"),_) -> let _ = recognize t in true
358	358	\| _ -> false in
359		try aux t with _ -> false
	359	try aux t with e when Errors.noncritical e -> false
360	360
361	361	end

+18

-12

plugins/romega/refl_omega.ml less more

224	224	env.terms <- env.terms @ [t]; i
225	225
226	226	let get_reified_atom env =
227		try List.nth env.terms with _ -> failwith "get_reified_atom"
	227	try List.nth env.terms
	228	with e when Errors.noncritical e -> failwith "get_reified_atom"
228	229
229	230	(* \subsection{Gestion de l'environnement de proposition pour Omega} *)
230	231	(* ajout d'une proposition *)

234	235	let i = List.length env.props in env.props <- env.props @ [t]; i
235	236
236	237	(* accès a une proposition *)
237		let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
	238	let get_prop v env =
	239	try List.nth v env
	240	with e when Errors.noncritical e -> failwith "get_prop"
238	241
239	242	(* \subsection{Gestion du nommage des équations} *)
240	243	(* Ajout d'une equation dans l'environnement de reification *)

246	249	(* accès a une equation *)
247	250	let get_equation env id =
248	251	try Hashtbl.find env.equations id
249		with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e
	252	with Not_found as e ->
	253	Printf.printf "Omega Equation %d non trouvée\n" id; raise e
250	254
251	255	(* Affichage des termes réifiés *)
252	256	let rec oprint ch = function

348	352	app coq_t_minus [\| reified_of_formula env t1; reified_of_formula env t2 \|]
349	353
350	354	let reified_of_formula env f =
351		begin try reified_of_formula env f with e -> oprint stderr f; raise e end
	355	try reified_of_formula env f
	356	with reraise -> oprint stderr f; raise reraise
352	357
353	358	let rec reified_of_proposition env = function
354	359	Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->

379	384	\| Pprop t -> app coq_p_prop [\| mk_nat (add_prop env t) \|]
380	385
381	386	let reified_of_proposition env f =
382		begin try reified_of_proposition env f
383		with e -> pprint stderr f; raise e end
	387	try reified_of_proposition env f
	388	with reraise -> pprint stderr f; raise reraise
384	389
385	390	(* \subsection{Omega vers COQ réifié} *)
386	391

396	401	List.fold_right mk_coeff body coeff_constant
397	402
398	403	let reified_of_omega env body c =
399		begin try
	404	try
400	405	reified_of_omega env body c
401		with e ->
402		display_eq display_omega_var (body,c); raise e
403		end
	406	with reraise ->
	407	display_eq display_omega_var (body,c); raise reraise
	408
404	409
405	410	(* \section{Opérations sur les équations}
406	411	Ces fonctions préparent les traces utilisées par la tactique réfléchie

999	1004	let weighted = filter_compatible_systems path all_solutions in
1000	1005	let (winner_sol,winner_deps) =
1001	1006	try select_smaller weighted
1002		with e ->
	1007	with reraise ->
1003	1008	Printf.printf "%d - %d\n"
1004	1009	(List.length weighted) (List.length all_solutions);
1005		List.iter display_depend path; raise e in
	1010	List.iter display_depend path; raise reraise
	1011	in
1006	1012	build_tree winner_sol (List.rev path) winner_deps
1007	1013
1008	1014	let find_path {o_hyp=id;o_path=p} env =

+2

-1

plugins/subtac/g_subtac.ml4 less more

89	89
90	90	let try_catch_exn f e =
91	91	try f e
92		with exn -> errorlabstrm "Program" (Errors.print exn)
	92	with exn when Errors.noncritical exn ->
	93	errorlabstrm "Program" (Errors.print exn)
93	94
94	95	let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
95	96	let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e

+2

-2

plugins/subtac/subtac.ml less more

220	220	\| (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) \|
221	221	Loc.Exc_located (loc, e') as e) -> raise e
222	222
223		\| e ->
	223	\| reraise ->
224	224	(* msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
225		raise e
	225	raise reraise

+3

-2

plugins/subtac/subtac_cases.ml less more

341	341	let pred = predicate 0 c in
342	342	let env' = push_rel_context (context_of_arsign arsign) env in
343	343	ignore(Typing.sort_of env' evm pred); pred
344		with _ -> lift nar c
	344	with e when Errors.noncritical e -> lift nar c
345	345
346	346	module Cases_F(Coercion : Coercion.S) : S = struct
347	347

1464	1464	\| None -> list_tabulate (fun _ -> Anonymous) nrealargs in
1465	1465	let arsign = fst (get_arity env0 indf) in
1466	1466	(na,None,build_dependent_inductive env0 indf)
1467		::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in
	1467	::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign
	1468	with e when Errors.noncritical e -> assert false) in
1468	1469	let rec buildrec = function
1469	1470	\| [],[] -> []
1470	1471	\| (_,tm)::ltm, x::tmsign ->

+2

-2

plugins/subtac/subtac_coercion.ml less more

355	355	jres),
356	356	jres.uj_type)
357	357	(hj,typ_cl) p)
358		with _ -> anomaly "apply_coercion"
	358	with e when Errors.noncritical e -> anomaly "apply_coercion"
359	359
360	360	let inh_app_fun env isevars j =
361	361	let isevars = ref isevars in

505	505	with NoSubtacCoercion ->
506	506	error_cannot_coerce env' isevars (t, t'))
507	507	else isevars
508		with _ -> isevars
	508	with e when Errors.noncritical e -> isevars
509	509	end

+2

-2

plugins/subtac/subtac_command.ml less more

247	247	\| [(_, None, t); (_, None, u)], Sort (Prop Null)
248	248	when Reductionops.is_conv env !isevars t u -> t
249	249	\| _, _ -> error ()
250		with _ -> error ()
	250	with e when Errors.noncritical e -> error ()
251	251	in
252	252	let measure = interp_casted_constr isevars binders_env measure relargty in
253	253	let wf_rel, wf_rel_fun, measure_fn =

439	439	let sort = Retyping.get_type_of env !evdref t in
440	440	let fixprot =
441	441	try mkApp (delayed_force Subtac_utils.fix_proto, [\|sort; t\|])
442		with e -> t
	442	with e when Errors.noncritical e -> t
443	443	in
444	444	(id,None,fixprot) :: env')
445	445	[] fixnames fixtypes

+4

-3

plugins/subtac/subtac_obligations.ml less more

120	120	let xobl = obls.(x) in
121	121	let oblb =
122	122	try get_obligation_body expand xobl
123		with _ -> assert(false)
	123	with e when Errors.noncritical e -> assert(false)
124	124	in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
125	125	deps []
126	126

497	497	let obls = Array.copy obls in
498	498	let _ = obls.(num) <- obl in
499	499	let res = try update_obls prg obls (pred rem)
500		with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
	500	with e when Errors.noncritical e ->
	501	pperror (Errors.print (Cerrors.process_vernac_interp_error e))
501	502	in
502	503	match res with
503	504	\| Remain n when n > 0 ->

551	552	\| Refiner.FailError (_, s) ->
552	553	user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
553	554	\| Util.Anomaly _ as e -> raise e
554		\| e -> false
	555	\| e when Errors.noncritical e -> false
555	556
556	557	and solve_prg_obligations prg ?oblset tac =
557	558	let obls, rem = prg.prg_obligations in

+4

-2

plugins/subtac/subtac_pretyping_F.ml less more

301	301	make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
302	302	\| GCoFix i ->
303	303	let cofix = (i,(names,ftys,fdefs)) in
304		(try check_cofix env cofix with e -> Loc.raise loc e);
	304	(try check_cofix env cofix
	305	with e when Errors.noncritical e -> Loc.raise loc e);
305	306	make_judge (mkCoFix cofix) ftys.(i) in
306	307	inh_conv_coerce_to_tycon loc env evdref fixj tycon
307	308

600	601	~split:true ~fail:true env !evdref;
601	602	evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
602	603	~split:true ~fail:false env !evdref
603		with e -> if fail_evar then raise e else ());
	604	with e when Errors.noncritical e ->
	605	if fail_evar then raise e else ());
604	606	evdref := consider_remaining_unif_problems env !evdref;
605	607	let c = if expand_evar then nf_evar !evdref c' else c' in
606	608	if fail_evar then check_evars env Evd.empty !evdref c;

+4

-4

plugins/subtac/subtac_utils.ml less more

231	231	let hyptype = substl names t in
232	232	trace (spc () ++ str ("treating evar " ^ string_of_id n));
233	233	(try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
234		with _ -> ());
	234	with e when Errors.noncritical e -> ());
235	235	let tac = assert_tac (Name n) hyptype in
236	236	let conttac =
237	237	(fun cont ->

330	330	Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
331	331	let (dom, rng) =
332	332	try (args.(0), args.(1))
333		with _ -> assert(false)
	333	with e when Errors.noncritical e -> assert(false)
334	334	in
335	335	let pi1 = (mk_ex_pi1 dom rng acc) in
336	336	let rng_body =

374	374	Inductiveops.control_only_guard (Global.env ())
375	375	const.Entries.const_entry_body;
376	376	const.Entries.const_entry_body
377		with e ->
	377	with reraise ->
378	378	Pfedit.delete_current_proof();
379		raise e
	379	raise reraise
380	380
381	381	(* let apply_tac t goal = t goal *)
382	382

+1

-1

plugins/xml/cic2acic.ml less more

348	348	if computeinnertypes then
349	349	try
350	350	Acic.CicHash.find terms_to_types tt
351		with _ ->
	351	with e when e <> Sys.Break ->
352	352	(CSC: Warning: it really happens, for example in Ring_theory!!! )
353	353	Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
354	354	else

+2

-1

plugins/xml/doubleTypeInference.ml less more

146	146	(CSC: universes. )
147	147	(try
148	148	Typeops.judge_of_type u
149		with _ -> (* Successor of a non universe-variable universe anomaly *)
	149	with e when e <> Sys.Break ->
	150	(* Successor of a non universe-variable universe anomaly *)
150	151	(Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
151	152	Typeops.judge_of_type (Termops.new_univ ())
152	153	)

+1

-1

plugins/xml/xmlcommand.ml less more

142	142	\| he::tail ->
143	143	(try
144	144	Unix.mkdir cwd 0o775
145		with _ -> () (* Let's ignore the errors on mkdir *)
	145	with e when e <> Sys.Break -> () (* Let's ignore the errors on mkdir *)
146	146	) ;
147	147	let newcwd = cwd ^ "/" ^ he in
148	148	join_dirs newcwd tail

+1

-1

pretyping/coercion.ml less more

125	125	jres),
126	126	jres.uj_type)
127	127	(hj,typ_cl) p)
128		with _ -> anomaly "apply_coercion"
	128	with e when Errors.noncritical e -> anomaly "apply_coercion"
129	129
130	130	let inh_app_fun env evd j =
131	131	let t = whd_betadeltaiota env evd j.uj_type in

+3

-3

pretyping/detyping.ml less more

271	271	try
272	272	let sign,ccl = decompose_lam_n_assum n c in
273	273	noccur_between 1 (rel_context_length sign) ccl
274		with _ -> (* Not eta-expanded or not reduced *)
	274	with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
275	275	false
276	276
277	277	let extract_nondep_branches test c b n =

385	385	\| Var id ->
386	386	(try
387	387	let _ = Global.lookup_named id in GRef (dl, VarRef id)
388		with _ ->
	388	with e when Errors.noncritical e ->
389	389	GVar (dl, id))
390	390	\| Sort s -> GSort (dl,detype_sort s)
391	391	\| Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->

491	491	let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
492	492	List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
493	493	mat
494		with _ ->
	494	with e when Errors.noncritical e ->
495	495	Array.to_list
496	496	(array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
497	497

+5

-3

pretyping/evarconv.ml less more

453	453	else Evd.set_leq_sort evd s1 s2
454	454	in (evd', true)
455	455	with Univ.UniverseInconsistency _ -> (evd, false)
456		\| _ -> (evd, false))
	456	\| e when Errors.noncritical e -> (evd, false))
457	457
458	458	\| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
459	459	ise_and evd

729	729	let (term2,l2 as appr2) = decompose_app t2 in
730	730	match kind_of_term term1, kind_of_term term2 with
731	731	\| Evar (evk1,args1), (Rel _\|Var _) when l1 = [] & l2 = []
732		& array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 ->
	732	& List.for_all (fun a -> eq_constr a term2 or isEvar a)
	733	(remove_instance_local_defs evd evk1 (Array.to_list args1)) ->
733	734	(* The typical kind of constraint coming from pattern-matching return
734	735	type inference *)
735	736	choose_less_dependent_instance evk1 evd term2 args1
736	737	\| (Rel _\|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
737		& array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
	738	& List.for_all (fun a -> eq_constr a term1 or isEvar a)
	739	(remove_instance_local_defs evd evk2 (Array.to_list args2)) ->
738	740	(* The typical kind of constraint coming from pattern-matching return
739	741	type inference *)
740	742	choose_less_dependent_instance evk2 evd term1 args2

+17

-10

pretyping/evarutil.ml less more

1193	1193
1194	1194	let closure_of_filter evd evk filter =
1195	1195	let evi = Evd.find_undefined evd evk in
1196		let vars = collect_vars (evar_concl evi) in
1197		let ids = List.map pi1 (evar_context evi) in
1198		let test id b = b \|\| Idset.mem id vars in
1199		let newfilter = List.map2 test ids filter in
	1196	let vars = collect_vars (nf_evar evd (evar_concl evi)) in
	1197	let test (id,c,_) b = b \|\| Idset.mem id vars \|\| c <> None in
	1198	let newfilter = List.map2 test (evar_context evi) filter in
1200	1199	if newfilter = evar_filter evi then None else Some newfilter
1201	1200
1202	1201	let restrict_hyps evd evk filter candidates =

1351	1350	let f,args = decompose_app_vect t in
1352	1351	match kind_of_term f with
1353	1352	\| Construct (ind,_) ->
1354		let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
1355		let params,_ = array_chop nparams args in
1356		array_for_all (is_constrainable_in k g) params
	1353	let nparams =
	1354	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams
	1355	in
	1356	if nparams > Array.length args
	1357	then true (* We don't try to be more clever *)
	1358	else
	1359	let params,_ = array_chop nparams args in
	1360	array_for_all (is_constrainable_in k g) params
1357	1361	\| Ind _ -> array_for_all (is_constrainable_in k g) args
1358	1362	\| Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
1359	1363	\| Evar (ev',_) -> ev' <> ev (If ev' needed, one may also try to restrict it)

1441	1445	(* FIXME: The body might be ill-typed when this is called from w_merge *)
1442	1446	let ty =
1443	1447	try Retyping.get_type_of evenv evd body
1444		with _ -> error "Ill-typed evar instance"
	1448	with e when Errors.noncritical e -> error "Ill-typed evar instance"
1445	1449	in
1446	1450	let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in
1447	1451	if b then evd else

1491	1495	(filter_compatible_candidates conv_algo env evd evi args rhs) l in
1492	1496	match l' with
1493	1497	\| [] -> error_cannot_unify env evd (mkEvar ev, rhs)
1494		\| [c,evd] -> Evd.define evk c evd
	1498	\| [c,evd] ->
	1499	(* solve_candidates might have been called recursively in the mean *)
	1500	(* time and the evar been solved by the filtering process *)
	1501	if Evd.is_undefined evd evk then Evd.define evk c evd else evd
1495	1502	\| l when List.length l < List.length l' ->
1496	1503	let candidates = List.map fst l in
1497	1504	restrict_evar evd evk None (Some candidates)

1642	1649	map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
1643	1650	imitate envk t in
1644	1651	t::l
1645		with _ -> l in
	1652	with e when Errors.noncritical e -> l in
1646	1653	(match candidates with
1647	1654	\| [x] -> x
1648	1655	\| _ ->

+1

-0

pretyping/evarutil.mli less more

229	229	val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun ->
230	230	evar_map
231	231
	232	val remove_instance_local_defs : evar_map -> existential_key -> constr list -> constr list

+4

-1

pretyping/evd.ml less more

66	66	let evar_context evi = named_context_of_val evi.evar_hyps
67	67	let evar_body evi = evi.evar_body
68	68	let evar_filter evi = evi.evar_filter
69		let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
70	69	let evar_filtered_context evi =
71	70	snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
	71	let evar_filtered_hyps evi =
	72	List.fold_right push_named_context_val (evar_filtered_context evi)
	73	empty_named_context_val
	74	let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
72	75	let evar_env evi =
73	76	List.fold_right push_named (evar_filtered_context evi)
74	77	(reset_context (Global.env()))

+1

-0

pretyping/evd.mli less more

126	126	val evar_context : evar_info -> named_context
127	127	val evar_filtered_context : evar_info -> named_context
128	128	val evar_hyps : evar_info -> named_context_val
	129	val evar_filtered_hyps : evar_info -> named_context_val
129	130	val evar_body : evar_info -> evar_body
130	131	val evar_filter : evar_info -> bool list
131	132	val evar_unfiltered_env : evar_info -> env

+1

-0

pretyping/inductiveops.ml less more

289	289	match kind_of_term t with
290	290	\| Ind ind ->
291	291	let (mib,mip) = Inductive.lookup_mind_specif env ind in
	292	if mib.mind_nparams > List.length l then raise Not_found;
292	293	let (par,rargs) = list_chop mib.mind_nparams l in
293	294	IndType((ind, par),rargs)
294	295	\| _ -> raise Not_found

+7

-4

pretyping/pretyping.ml less more

68	68	if List.for_all (fun l->1=List.length l) possible_indexes then
69	69	let indexes = Array.of_list (List.map List.hd possible_indexes) in
70	70	let fix = ((indexes, 0),fixdefs) in
71		(try check_fix env fix with
72		\| e -> if loc = dummy_loc then raise e else Loc.raise loc e);
	71	(try check_fix env fix
	72	with e when Errors.noncritical e ->
	73	if loc = dummy_loc then raise e else Loc.raise loc e);
73	74	indexes
74	75	else
75	76	(* we now search recursively amoungst all combinations *)

108	109	(* Resolve eagerly, potentially making wrong choices *)
109	110	evdref := (try consider_remaining_unif_problems
110	111	~ts:(Typeclasses.classes_transparent_state ()) env !evdref
111		with e -> if fail_evar then raise e else !evdref)
	112	with e when Errors.noncritical e ->
	113	if fail_evar then raise e else !evdref)
112	114
113	115	let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
114	116	let evdref = ref evd in

440	442	make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
441	443	\| GCoFix i ->
442	444	let cofix = (i,(names,ftys,fdefs)) in
443		(try check_cofix env cofix with e -> Loc.raise loc e);
	445	(try check_cofix env cofix
	446	with e when Errors.noncritical e -> Loc.raise loc e);
444	447	make_judge (mkCoFix cofix) ftys.(i) in
445	448	inh_conv_coerce_to_tycon loc env evdref fixj tycon
446	449

+4

-4

pretyping/recordops.ml less more

206	206	match kind_of_term t with
207	207	App (f,vargs) ->
208	208	begin
209		try Const_cs (global_of_constr f) , -1, Array.to_list vargs with
210		_ -> raise Not_found
	209	try Const_cs (global_of_constr f) , -1, Array.to_list vargs
	210	with e when Errors.noncritical e -> raise Not_found
211	211	end
212	212	\| Rel n -> Default_cs, pred n, []
213	213	\| Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
214	214	\| Sort s -> Sort_cs (family_of_sort s), -1, []
215	215	\| _ ->
216	216	begin
217		try Const_cs (global_of_constr t) , -1, [] with
218		_ -> raise Not_found
	217	try Const_cs (global_of_constr t) , -1, []
	218	with e when Errors.noncritical e -> raise Not_found
219	219	end
220	220
221	221	(* Intended to always succeed *)

+8

-2

pretyping/reductionops.ml less more

923	923	let u = whd_betaiota Evd.empty u in
924	924	match kind_of_term u with
925	925	\| Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
926		let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
	926	let m =
	927	try destMeta c
	928	with e when Errors.noncritical e -> destMeta (pi1 (destCast c))
	929	in
927	930	(match
928	931	try
929	932	let g,s = List.assoc m metas in

933	936	\| Some g -> irec (mkCase (ci,p,g,bl))
934	937	\| None -> mkCase (ci,irec p,c,Array.map irec bl))
935	938	\| App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
936		let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
	939	let m =
	940	try destMeta f
	941	with e when Errors.noncritical e -> destMeta (pi1 (destCast f))
	942	in
937	943	(match
938	944	try
939	945	let g,s = List.assoc m metas in

+6

-6

pretyping/retyping.ml less more

29	29	(* et sinon on substitue *)
30	30
31	31	let sort_of_atomic_type env sigma ft args =
32		let rec concl_of_arity env ar =
33		match kind_of_term (whd_betadeltaiota env sigma ar) with
34		\| Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
35		\| Sort s -> s
36		\| _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
37		in concl_of_arity env ft
	32	let rec concl_of_arity env ar args =
	33	match kind_of_term (whd_betadeltaiota env sigma ar), args with
	34	\| Prod (na, t, b), h::l -> concl_of_arity (push_rel (na,Some h,t) env) b l
	35	\| Sort s, [] -> s
	36	\| _ -> anomaly "Not a sort"
	37	in concl_of_arity env ft (Array.to_list args)
38	38
39	39	let type_of_var env id =
40	40	try let (_,_,ty) = lookup_named id env in ty

+6

-6

pretyping/tacred.ml less more

124	124
125	125	(* We use a cache registered as a global table *)
126	126
127		let eval_table = ref Cmap.empty
128
129		type frozen = (int * constant_evaluation) Cmap.t
	127	let eval_table = ref Cmap_env.empty
	128
	129	type frozen = (int * constant_evaluation) Cmap_env.t
130	130
131	131	let init () =
132		eval_table := Cmap.empty
	132	eval_table := Cmap_env.empty
133	133
134	134	let freeze () =
135	135	!eval_table

290	290	let reference_eval sigma env = function
291	291	\| EvalConst cst as ref ->
292	292	(try
293		Cmap.find cst !eval_table
	293	Cmap_env.find cst !eval_table
294	294	with Not_found -> begin
295	295	let v = compute_consteval sigma env ref in
296		eval_table := Cmap.add cst v !eval_table;
	296	eval_table := Cmap_env.add cst v !eval_table;
297	297	v
298	298	end)
299	299	\| ref -> compute_consteval sigma env ref

+6

-4

pretyping/typeclasses.ml less more

117	117
118	118	let class_info c =
119	119	try Gmap.find c !classes
120		with _ -> not_a_class (Global.env()) (constr_of_global c)
	120	with Not_found -> not_a_class (Global.env()) (constr_of_global c)
121	121
122	122	let global_class_of_constr env c =
123	123	try class_info (global_of_constr c)

131	131	let rels, c = Term.decompose_prod_assum c in
132	132	rels, dest_class_app env c
133	133
134		let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None
	134	let class_of_constr c =
	135	try Some (dest_class_arity (Global.env ()) c)
	136	with e when Errors.noncritical e -> None
135	137
136	138	let rec is_class_type evd c =
137	139	match kind_of_term c with

214	216	try
215	217	let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
216	218	set_typeclass_transparency cst false false; cl
217		with _ -> cl
	219	with e when Errors.noncritical e -> cl
218	220
219	221	let class_input : typeclass -> obj =
220	222	declare_object

237	239	let (evd, c) = resolve_one_typeclass env sigma
238	240	(Retyping.get_type_of env sigma c) in
239	241	Evd.is_empty (Evd.undefined_evars evd)
240		with _ -> false
	242	with e when Errors.noncritical e -> false
241	243
242	244	let build_subclasses ~check env sigma glob pri =
243	245	let rec aux pri c =

+8

-5

pretyping/unification.ml less more

429	429	then Evd.set_leq_sort sigma s1 s2
430	430	else Evd.set_eq_sort sigma s1 s2
431	431	in (sigma', metasubst, evarsubst)
432		with _ -> error_cannot_unify curenv sigma (m,n))
433
	432	with e when Errors.noncritical e ->
	433	error_cannot_unify curenv sigma (m,n))
	434
434	435	\| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
435	436	unirec_rec (push (na,t1) curenvnb) CONV true wt
436	437	(unirec_rec curenvnb CONV true false substn t1 t2) c1 c2

707	708	else (right, st2, res)
708	709	\| (IsSuperType,IsSubType) ->
709	710	(try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
710		with _ -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
	711	with e when Errors.noncritical e ->
	712	(right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
711	713	\| (IsSubType,IsSuperType) ->
712	714	(try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
713		with _ -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
	715	with e when Errors.noncritical e ->
	716	(right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
714	717
715	718	(* Unification
716	719	*

912	915	let rec process_eqns failures = function
913	916	\| (mv,status,c)::eqns ->
914	917	(match (try Inl (unify_type env evd flags mv status c)
915		with e -> Inr e)
	918	with e when Errors.noncritical e -> Inr e)
916	919	with
917	920	\| Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
918	921	\| Inl (evd,metas,evars) ->

+18

-6

pretyping/vnorm.ml less more

43	43	let find_rectype_a env c =
44	44	let (t, l) =
45	45	let t = whd_betadeltaiota env c in
46		try destApp t with _ -> (t,[\|\|]) in
	46	try destApp t with e when Errors.noncritical e -> (t,[\|\|]) in
47	47	match kind_of_term t with
48	48	\| Ind ind -> (ind, l)
49	49	\| _ -> raise Not_found

175	175	nf_stk env (mkApp(c,args)) t stk
176	176	\| Zfix (f,vargs) :: stk ->
177	177	let fa, typ = nf_fix_app env f vargs in
178		let _,_,codom = try decompose_prod env typ with _ -> exit 120 in
	178	let _,_,codom =
	179	try decompose_prod env typ
	180	with e when Errors.noncritical e -> exit 120
	181	in
179	182	nf_stk env (mkApp(fa,[\|c\|])) (subst1 c codom) stk
180	183	\| Zswitch sw :: stk ->
181	184	let (mind,_ as ind),allargs = find_rectype_a env t in

205	208	\| Vfun f, Prod _ ->
206	209	let k = nb_rel env in
207	210	let vb = body_of_vfun k f in
208		let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
	211	let name,dom,codom =
	212	try decompose_prod env pT
	213	with e when Errors.noncritical e -> exit 121
	214	in
209	215	let dep,body =
210	216	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
211	217	dep, mkLambda(name,dom,body)

227	233	let args =
228	234	Array.init len
229	235	(fun i ->
230		let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
	236	let _,dom,codom =
	237	try decompose_prod env !t
	238	with e when Errors.noncritical e -> exit 123
	239	in
231	240	let c = nf_val env (arg vargs i) dom in
232	241	t := subst1 c codom; c) in
233	242	!t,args

238	247	let args =
239	248	Array.init len
240	249	(fun i ->
241		let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
	250	let _,dom,codom =
	251	try decompose_prod env !t
	252	with e when Errors.noncritical e -> exit 124
	253	in
242	254	let c = nf_val env (bfield b i) dom in
243	255	t := subst1 c codom; c) in
244	256	args

248	260	let vb = body_of_vfun k f in
249	261	let name,dom,codom =
250	262	try decompose_prod env typ
251		with _ ->
	263	with e when Errors.noncritical e ->
252	264	raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
253	265	in
254	266	let body = nf_val (push_rel (name,None,dom) env) vb codom in

+1

-1

proofs/evar_refiner.ml less more

41	41	let sigma',typed_c =
42	42	try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var
43	43	(Pretyping.OfType (Some evi.evar_concl)) rawc
44		with _ ->
	44	with e when Errors.noncritical e ->
45	45	let loc = Glob_term.loc_of_glob_constr rawc in
46	46	user_err_loc
47	47	(loc,"",Pp.str ("Instance is not well-typed in the environment of " ^

+11

-5

proofs/goal.ml less more

275	275
276	276	let recheck_typability (what,id) env sigma t =
277	277	try check_typability env sigma t
278		with _ ->
	278	with e when Errors.noncritical e ->
279	279	let s = match what with
280	280	\| None -> "the conclusion"
281	281	\| Some id -> "hypothesis "^(Names.string_of_id id) in

473	473	(* Old style hyps primitive *)
474	474	let hyps evars gl =
475	475	let evi = content evars gl in
476		evi.Evd.evar_hyps
	476	Evd.evar_filtered_hyps evi
477	477
478	478	(* Access to ".evar_concl" *)
479	479	let concl evars gl =

553	553	with a good implementation of them.
554	554	*)
555	555
556		(* Used for congruence closure *)
557		let new_goal_with sigma gl new_hyps =
	556	(* Used for congruence closure and change *)
	557	let new_goal_with sigma gl extra_hyps =
558	558	let evi = content sigma gl in
559		let new_evi = { evi with Evd.evar_hyps = new_hyps } in
	559	let hyps = evi.Evd.evar_hyps in
	560	let new_hyps =
	561	List.fold_right Environ.push_named_context_val extra_hyps hyps in
	562	let extra_filter = List.map (fun _ -> true) extra_hyps in
	563	let new_filter = extra_filter @ evi.Evd.evar_filter in
	564	let new_evi =
	565	{ evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
560	566	let new_evi = Typeclasses.mark_unresolvable new_evi in
561	567	let evk = Evarutil.new_untyped_evar () in
562	568	let new_sigma = Evd.add Evd.empty evk new_evi in

+1

-1

proofs/goal.mli less more

231	231	val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
232	232
233	233	(* Used for congruence closure *)
234		val new_goal_with : Evd.evar_map -> goal -> Environ.named_context_val -> goal Evd.sigma
	234	val new_goal_with : Evd.evar_map -> goal -> Sign.named_context -> goal Evd.sigma
235	235
236	236	(* Used by the compatibility layer and typeclasses *)
237	237	val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map

+1

-1

proofs/logic.ml less more

104	104
105	105	let recheck_typability (what,id) env sigma t =
106	106	try check_typability env sigma t
107		with _ ->
	107	with e when Errors.noncritical e ->
108	108	let s = match what with
109	109	\| None -> "the conclusion"
110	110	\| Some id -> "hypothesis "^(string_of_id id) in

+3

-3

proofs/pfedit.ml less more

67	67	\| None -> Proofview.tclUNIT ()
68	68	in
69	69	try Proof_global.run_tactic tac
70		with e -> Proof_global.discard_current (); raise e
	70	with reraise -> Proof_global.discard_current (); raise reraise
71	71
72	72	let restart_proof () = undo_todepth 1
73	73

163	163	let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
164	164	delete_current_proof ();
165	165	const
166		with e ->
	166	with reraise ->
167	167	delete_current_proof ();
168		raise e
	168	raise reraise
169	169
170	170	let build_by_tactic env typ tac =
171	171	let id = id_of_string ("temporary_proof"^string_of_int (next())) in

+6

-6

proofs/proof.ml less more

322	322	let transaction pr t =
323	323	init_transaction pr;
324	324	try t (); commit pr
325		with e -> rollback pr; raise e
	325	with reraise -> rollback pr; raise reraise
326	326
327	327
328	328	(* Focus command (focuses on the [i]th subgoal) *)

428	428	let tacticced_proofview = Proofview.apply env tac sp in
429	429	pr.state <- { pr.state with proofview = tacticced_proofview };
430	430	push_undo starting_point pr
431		with e ->
	431	with reraise ->
432	432	restore_state starting_point pr;
433		raise e
	433	raise reraise
434	434
435	435	(* Commands *)
436	436

475	475	let new_proofview = Proofview.V82.instantiate_evar n com sp in
476	476	pr.state <- { pr.state with proofview = new_proofview };
477	477	push_undo starting_point pr
478		with e ->
	478	with reraise ->
479	479	restore_state starting_point pr;
480		raise e
481		end
	480	raise reraise
	481	end

+6

-4

proofs/proofview.ml less more

319	319	(* takes a tactic which can raise exception and makes it pure by failing
320	320	on with these exceptions. Does not catch anomalies. *)
321	321	let purify t =
322		let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
323		with Util.Anomaly _ as e -> raise e
324		\| e -> sk (Util.Inr e) fk step
325		}
	322	let t' env =
	323	{ go = fun sk fk step ->
	324	try (t env).go (fun x -> sk (Util.Inl x)) fk step
	325	with Util.Anomaly _ as e -> raise e
	326	\| e when Errors.noncritical e -> sk (Util.Inr e) fk step
	327	}
326	328	in
327	329	tclBIND t' begin function
328	330	\| Util.Inl x -> tclUNIT x

+4

-4

proofs/refiner.ml less more

254	254	try
255	255	t1 g
256	256	with (* Breakpoint *)
257		\| e -> catch_failerror e; t2 g
	257	\| e when Errors.noncritical e -> catch_failerror e; t2 g
258	258
259	259	(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
260	260	then applies t2 *)

266	266	let tclORELSE_THEN t1 t2then t2else gls =
267	267	match
268	268	try Some(tclPROGRESS t1 gls)
269		with e -> catch_failerror e; None
	269	with e when Errors.noncritical e -> catch_failerror e; None
270	270	with
271	271	\| None -> t2else gls
272	272	\| Some sgl ->

297	297	try
298	298	tcal tac_if0 continue gl
299	299	with (* Breakpoint *)
300		\| e -> catch_failerror e; tac_else0 e gl
	300	\| e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl
301	301
302	302	(* Try the first tactic and, if it succeeds, continue with
303	303	the second one, and if it fails, use the third one *)

351	351	\| TacTimeout \| Loc.Exc_located(_,TacTimeout) ->
352	352	restore_timeout ();
353	353	errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!")
354		\| e -> restore_timeout (); raise e
	354	\| reraise -> restore_timeout (); raise reraise
355	355
356	356	(* Beware: call by need of CAML, g is needed *)
357	357	let rec tclREPEAT t g =

+4

-4

proofs/tactic_debug.ml less more

139	139	else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in
140	140	(* What to execute *)
141	141	try f newlevel
142		with e ->
	142	with reraise ->
143	143	skip:=0; skipped:=0;
144		if Logic.catchable_exception e then
145		ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
146		raise e
	144	if Logic.catchable_exception reraise then
	145	ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise);
	146	raise reraise
147	147
148	148	(* Prints a constr *)
149	149	let db_constr debug env c =

+6

-7

scripts/coqmktop.ml less more

44	44	[ "Camlp4Top.cmo";
45	45	"Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
46	46	"Camlp4Parsers/Camlp4OCamlParser.cmo";
47		"Camlp4Parsers/Camlp4GrammarParser.cmo";
48		"q_util.cmo"; "q_coqast.cmo" ]
	47	"Camlp4Parsers/Camlp4GrammarParser.cmo" ]
49	48	let topobjs = camlp4topobjs
50	49
51	50	let gramobjs = []

256	255	output_string oc "Coqtop.start();;\n";
257	256	close_out oc;
258	257	main_name
259		with e ->
260		clean main_name; raise e
	258	with reraise ->
	259	clean main_name; raise reraise
261	260
262	261	(* main part *)
263	262	let main () =

310	309	clean main_file;
311	310	(* command gives the exit code in HSB, and signal in LSB !!! *)
312	311	if retcode > 255 then retcode lsr 8 else retcode
313		with e ->
314		clean main_file; raise e
	312	with reraise ->
	313	clean main_file; raise reraise
315	314
316	315	let retcode =
317		try Printexc.print main () with _ -> 1
	316	try Printexc.print main () with any -> 1
318	317
319	318	let _ = exit retcode

+6

-5

tactics/auto.ml less more

828	828
829	829	let path_of_constr_expr c =
830	830	match c with
831		\| Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny)
	831	\| Topconstr.CRef r ->
	832	(try PathHints [global r] with e when Errors.noncritical e -> PathAny)
832	833	\| _ -> PathAny
833	834
834	835	let interp_hints h =

1169	1170	let out = tac gl in
1170	1171	msg_debug (str s ++ spc () ++ pp () ++ str ". (success)");
1171	1172	out
1172		with e ->
	1173	with reraise ->
1173	1174	msg_debug (str s ++ spc () ++ pp () ++ str ". (fail)");
1174		raise e
	1175	raise reraise
1175	1176	end
1176	1177	\| Info ->
1177	1178	(* For "info (trivial/auto)", we store a log trace *)

1180	1181	let out = tac gl in
1181	1182	trace := (depth, Some pp) :: !trace;
1182	1183	out
1183		with e ->
	1184	with reraise ->
1184	1185	trace := (depth, None) :: !trace;
1185		raise e
	1186	raise reraise
1186	1187	end
1187	1188
1188	1189	(** For info, from the linear trace information, we reconstitute the part

+9

-3

tactics/autorewrite.ml less more

207	207
208	208	(* Functions necessary to the library object declaration *)
209	209	let cache_hintrewrite (_,(rbase,lrl)) =
210		let base = try find_base rbase with _ -> HintDN.empty in
211		let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in
	210	let base =
	211	try find_base rbase
	212	with e when Errors.noncritical e -> HintDN.empty
	213	in
	214	let max =
	215	try fst (Util.list_last (HintDN.find_all base))
	216	with e when Errors.noncritical e -> 0
	217	in
212	218	let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
213	219	rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
214	220

247	253	try
248	254	ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true
249	255	(* try ignore(Evarconv.the_conv_x env x y evd); true *)
250		with _ -> false
	256	with e when Errors.noncritical e -> false
251	257
252	258	let decompose_applied_relation metas env sigma c ctype left2right =
253	259	let find_rel ty =

+5

-2

tactics/class_tactics.ml4 less more

684	684	let evd =
685	685	try Evarconv.consider_remaining_unif_problems
686	686	~ts:(Typeclasses.classes_transparent_state ()) env evd
687		with _ -> evd
	687	with e when Errors.noncritical e -> evd
688	688	in
689	689	resolve_all_evars debug m env (initial_select_evars filter) evd split fail
690	690

775	775
776	776	let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
777	777	try
778		let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
	778	let dbs = list_map_filter
	779	(fun db -> try Some (Auto.searchtable_map db)
	780	with e when Errors.noncritical e -> None) dbs
	781	in
779	782	let st = match dbs with x :: _ -> Hint_db.transparent_state x \| _ -> st in
780	783	eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
781	784	with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl

+2

-1

tactics/eauto.ml4 less more

204	204	(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
205	205	(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
206	206	(lgls,pptac) :: aux tacl
207		with e -> Refiner.catch_failerror e; aux tacl
	207	with e when Errors.noncritical e ->
	208	Refiner.catch_failerror e; aux tacl
208	209	in aux l
209	210
210	211	(* Ordering of states is lexicographic on depth (greatest first) then

+3

-2

tactics/equality.ml less more

333	333	try
334	334	rewrite_side_tac (!general_rewrite_clause cls
335	335	lft2rgt occs (c,l) ~new_goals:[]) tac gl
336		with e -> (* Try to see if there's an equality hidden *)
	336	with e when Errors.noncritical e ->
	337	(* Try to see if there's an equality hidden *)
337	338	let env' = push_rel_context rels env in
338	339	let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
339	340	match match_with_equality_type t' with

1155	1156	]
1156	1157	(* not a dep eq or no decidable type found *)
1157	1158	) else (raise Not_dep_pair)
1158		) with _ ->
	1159	) with e when Errors.noncritical e ->
1159	1160	inject_at_positions env sigma u eq_clause posns
1160	1161	(fun _ -> intros_pattern no_move ipats)
1161	1162

+1

-1

tactics/extratactics.ml4 less more

605	605	hResolve id c n t gl
606	606	with
607	607	\| UserError _ as e -> raise e
608		\| _ -> resolve_auto (n+1)
	608	\| e when Errors.noncritical e -> resolve_auto (n+1)
609	609	in
610	610	resolve_auto 1
611	611

+8

-2

tactics/hipattern.ml4 less more

63	63
64	64	(* Test dependencies *)
65	65
	66	(* NB: we consider also the let-in case in the following function,
	67	since they may appear in types of inductive constructors (see #2629) *)
	68
66	69	let rec has_nodep_prod_after n c =
67	70	match kind_of_term c with
68		\| Prod (_,_,b) ->
	71	\| Prod (_,_,b) \| LetIn (_,_,_,b) ->
69	72	( n>0 \|\| not (dependent (mkRel 1) b))
70	73	&& (has_nodep_prod_after (n-1) b)
71	74	\| _ -> true

354	357	let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ]
355	358
356	359	let match_eq eqn eq_pat =
357		let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
	360	let pat =
	361	try Lazy.force eq_pat
	362	with e when Errors.noncritical e -> raise PatternMatchingFailure
	363	in
358	364	match matches pat eqn with
359	365	\| [(m1,t);(m2,x);(m3,y)] ->
360	366	assert (m1 = meta1 & m2 = meta2 & m3 = meta3);

+2

-2

tactics/inv.ml less more

496	496	(* The most general inversion tactic *)
497	497	let inversion inv_kind status names id gls =
498	498	try (raw_inversion inv_kind id status names) gls
499		with e -> wrap_inv_error id e
	499	with e when Errors.noncritical e -> wrap_inv_error id e
500	500
501	501	(* Specializing it... *)
502	502

539	539	inversion (false,k) NoDep names id;
540	540	intros_replace_ids])
541	541	gls
542		with e -> wrap_inv_error id e
	542	with e when Errors.noncritical e -> wrap_inv_error id e
543	543
544	544	let invIn_gen k names idl = try_intros_until (invIn k names idl)
545	545

+15

-10

tactics/rewrite.ml4 less more

120	120	let inst = mkApp (Lazy.force rewrite_relation_class, [\| evar; mkApp (c, params) \|]) in
121	121	let _ = Typeclasses.resolve_one_typeclass env' evd inst in
122	122	Some (it_mkProd_or_LetIn t rels)
123		with _ -> None)
	123	with e when Errors.noncritical e -> None)
124	124	\| _ -> None
125	125
126	126	let _ =

144	144	new_cstr_evar evars env
145	145	(* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
146	146	in
147		let mk_relty evars env ty obj =
	147	let mk_relty evars newenv ty obj =
148	148	match obj with
149	149	\| None \| Some (_, None) ->
150	150	let relty = mk_relation ty in
151		new_evar evars env relty
	151	if closed0 ty then
	152	let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
	153	new_evar evars env' relty
	154	else new_evar evars newenv relty
152	155	\| Some (x, Some rel) -> evars, rel
153	156	in
154	157	let rec aux env evars ty l =

226	229
227	230	let evd_convertible env evd x y =
228	231	try ignore(Evarconv.the_conv_x env x y evd); true
229		with _ -> false
	232	with e when Errors.noncritical e -> false
230	233
231	234	let rec decompose_app_rel env evd t =
232	235	match kind_of_term t with

492	495	\| [] -> rel
493	496
494	497	let pointwise_or_dep_relation n t car rel =
495		if noccurn 1 car then
	498	if noccurn 1 car && noccurn 1 rel then
496	499	mkApp (Lazy.force pointwise_relation, [\| t; lift (-1) car; lift (-1) rel \|])
497	500	else
498	501	mkApp (Lazy.force forall_relation,

1047	1050	let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
1048	1051	let unfolded =
1049	1052	try Tacred.try_red_product env sigma c
1050		with _ -> error "fold: the term is not unfoldable !"
	1053	with e when Errors.noncritical e ->
	1054	error "fold: the term is not unfoldable !"
1051	1055	in
1052	1056	try
1053	1057	let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in

1055	1059	Some (Some { rew_car = ty; rew_from = t; rew_to = c';
1056	1060	rew_prf = RewCast DEFAULTcast;
1057	1061	rew_evars = sigma, cstrevars evars })
1058		with _ -> None
	1062	with e when Errors.noncritical e -> None
1059	1063
1060	1064	let fold_glob c : strategy =
1061	1065	fun env avoid t ty cstr evars ->

1063	1067	let sigma, c = Pretyping.Default.understand_tcc (goalevars evars) env c in
1064	1068	let unfolded =
1065	1069	try Tacred.try_red_product env sigma c
1066		with _ -> error "fold: the term is not unfoldable !"
	1070	with e when Errors.noncritical e ->
	1071	error "fold: the term is not unfoldable !"
1067	1072	in
1068	1073	try
1069	1074	let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in

1071	1076	Some (Some { rew_car = ty; rew_from = t; rew_to = c';
1072	1077	rew_prf = RewCast DEFAULTcast;
1073	1078	rew_evars = sigma, cstrevars evars })
1074		with _ -> None
	1079	with e when Errors.noncritical e -> None
1075	1080
1076	1081
1077	1082	end

1976	1981	let evm = project gl in
1977	1982	let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
1978	1983	fn env evm car rel gl
1979		with e ->
	1984	with e when Errors.noncritical e ->
1980	1985	try fallback gl
1981	1986	with Hipattern.NoEquationFound ->
1982	1987	match e with

+34

-30

tactics/tacinterp.ml less more

49	49	open Evd
50	50
51	51	let safe_msgnl s =
52		try msgnl s with e ->
	52	try msgnl s with e when Errors.noncritical e ->
53	53	msgnl
54	54	(str "bug in the debugger: " ++
55	55	str "an exception is raised while printing debug information")

91	91	if call_trace = [] then tac g else try tac g with
92	92	\| LtacLocated _ as e -> raise e
93	93	\| Loc.Exc_located (_,LtacLocated _) as e -> raise e
94		\| e ->
	94	\| e when Errors.noncritical e ->
95	95	let (nrep,loc',c),tail = list_sep_last call_trace in
96	96	let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e \| _ ->dloc,e in
97	97	if tail = [] then

568	568	try
569	569	Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
570	570	(Smartlocate.smart_global r)
571		with _ -> ()) occs
	571	with e when Errors.noncritical e -> ()) occs
572	572	\| Cbv grf \| Lazy grf ->
573	573	List.iter (fun r ->
574	574	try
575	575	Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
576	576	(Smartlocate.smart_global r)
577		with _ -> ()) grf.rConst
	577	with e when Errors.noncritical e -> ()) grf.rConst
578	578	\| _ -> ()
579	579
580	580	let intern_red_expr ist = function

1411	1411	\| ConstrTerm c ->
1412	1412	try
1413	1413	f ist gl c
1414		with e ->
1415		debugging_exception_step ist false e (fun () ->
	1414	with reraise ->
	1415	debugging_exception_step ist false reraise (fun () ->
1416	1416	str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c));
1417		raise e
	1417	raise reraise
1418	1418
1419	1419	(* Interprets a constr expression possibly to first evaluate *)
1420	1420	let interp_constr_may_eval ist gl c =
1421	1421	let (sigma,csr) =
1422	1422	try
1423	1423	interp_may_eval pf_interp_constr ist gl c
1424		with e ->
1425		debugging_exception_step ist false e (fun () -> str"evaluation of term");
1426		raise e
	1424	with reraise ->
	1425	debugging_exception_step ist false reraise (fun () ->
	1426	str"evaluation of term");
	1427	raise reraise
1427	1428	in
1428	1429	begin
1429	1430	db_constr ist.debug (pf_env gl) csr;

1761	1762	let pack_sigma (sigma,c) = {it=c;sigma=sigma}
1762	1763
1763	1764	let extend_gl_hyps { it=gl ; sigma=sigma } sign =
1764		let hyps = Goal.V82.hyps sigma gl in
1765		let new_hyps = List.fold_right Environ.push_named_context_val sign hyps in
1766		(* spiwack: (2010/01/13) if a bug was reintroduced in [change] in is probably here *)
1767		Goal.V82.new_goal_with sigma gl new_hyps
	1765	Goal.V82.new_goal_with sigma gl sign
1768	1766
1769	1767	(* Interprets an l-tac expression into a value *)
1770	1768	let rec val_interp ist gl (tac:glob_tactic_expr) =

1924	1922	try
1925	1923	catch_error trace
1926	1924	(val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body
1927		with e ->
1928		debugging_exception_step ist false e (fun () -> str "evaluation");
1929		raise e in
	1925	with reraise ->
	1926	debugging_exception_step ist false reraise
	1927	(fun () -> str "evaluation");
	1928	raise reraise
	1929	in
1930	1930	let gl = { gl with sigma=sigma } in
1931	1931	debugging_step ist
1932	1932	(fun () ->

2211	2211	(try
2212	2212	let lmatch =
2213	2213	try extended_matches c csr
2214		with e ->
2215		debugging_exception_step ist false e (fun () ->
	2214	with reraise ->
	2215	debugging_exception_step ist false reraise (fun () ->
2216	2216	str "matching with pattern" ++ fnl () ++
2217	2217	pr_constr_pattern_env (pf_env g) c);
2218		raise e in
	2218	raise reraise
	2219	in
2219	2220	try
2220	2221	let lfun = extend_values_with_bindings lmatch ist.lfun in
2221	2222	eval_with_fail { ist with lfun=lfun } lz g mt
2222		with e ->
2223		debugging_exception_step ist false e (fun () ->
	2223	with reraise ->
	2224	debugging_exception_step ist false reraise (fun () ->
2224	2225	str "rule body for pattern" ++
2225	2226	pr_constr_pattern_env (pf_env g) c);
2226		raise e
	2227	raise reraise
2227	2228	with e when is_match_catchable e ->
2228	2229	debugging_step ist (fun () -> str "switching to the next rule");
2229	2230	apply_match ist sigma csr tl)

2235	2236	errorlabstrm "Tacinterp.apply_match" (str
2236	2237	"No matching clauses for match.") in
2237	2238	let (sigma,csr) =
2238		try interp_ltac_constr ist g constr with e ->
2239		debugging_exception_step ist true e
	2239	try interp_ltac_constr ist g constr with reraise ->
	2240	debugging_exception_step ist true reraise
2240	2241	(fun () -> str "evaluation of the matched expression");
2241		raise e in
	2242	raise reraise in
2242	2243	let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in
2243	2244	let res =
2244		try apply_match ist sigma csr ilr with e ->
2245		debugging_exception_step ist true e (fun () -> str "match expression");
2246		raise e in
	2245	try apply_match ist sigma csr ilr with reraise ->
	2246	debugging_exception_step ist true reraise
	2247	(fun () -> str "match expression");
	2248	raise reraise in
2247	2249	debugging_step ist (fun () ->
2248	2250	str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res));
2249	2251	res

2403	2405	(h_generalize_dep c_interp)
2404	2406	\| TacLetTac (na,c,clp,b,eqpat) ->
2405	2407	let clp = interp_clause ist gl clp in
	2408	let eqpat = Option.map (interp_intro_pattern ist gl) eqpat in
2406	2409	if clp = nowhere then
2407	2410	(* We try to fully-typecheck the term *)
2408	2411	let (sigma,c_interp) = pf_interp_constr ist gl c in

3179	3182	let tacticIn t =
3180	3183	globTacticIn (fun ist ->
3181	3184	try glob_tactic (t ist)
3182		with e -> anomalylabstrm "tacticIn"
	3185	with e when Errors.noncritical e ->
	3186	anomalylabstrm "tacticIn"
3183	3187	(str "Incorrect tactic expression. Received exception is:" ++
3184	3188	Errors.print e))
3185	3189

+10

-5

tactics/tactics.ml less more

1017	1017	let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
1018	1018	let rec aux clause =
1019	1019	try progress_with_clause flags innerclause clause
1020		with err ->
	1020	with err when Errors.noncritical err ->
1021	1021	try aux (clenv_push_prod clause)
1022	1022	with NotExtensibleClause -> raise err in
1023	1023	aux (make_clenv_binding gl (d,thm) lbind)

1707	1707	let flags = default_matching_flags sigma0 in
1708	1708	let matching_fun t =
1709	1709	try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t)
1710		with _ -> raise NotUnifiable in
	1710	with e when Errors.noncritical e -> raise NotUnifiable in
1711	1711	let merge_fun c1 c2 =
1712	1712	match c1, c2 with
1713	1713	\| Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) ->

2553	2553
2554	2554
2555	2555	let specialize_eqs id gl =
2556		if try ignore(clear [id] gl); false with _ -> true then
	2556	if
	2557	(try ignore(clear [id] gl); false
	2558	with e when Errors.noncritical e -> true)
	2559	then
2557	2560	tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl
2558	2561	else specialize_eqs id gl
2559	2562

2715	2718	\| Some ( _,None,ind) ->
2716	2719	let indhd,indargs = decompose_app ind in
2717	2720	try {!res with indref = Some (global_of_constr indhd) }
2718		with _ -> error "Cannot find the inductive type of the inductive scheme.";;
	2721	with e when Errors.noncritical e ->
	2722	error "Cannot find the inductive type of the inductive scheme.";;
2719	2723
2720	2724	let compute_scheme_signature scheme names_info ind_type_guess =
2721	2725	let f,l = decompose_app scheme.concl in

3550	3554	in
3551	3555	let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
3552	3556	in tclEVARS evd gl
3553		with _ -> tclFAIL 0 (str"Not unifiable") gl
	3557	with e when Errors.noncritical e ->
	3558	tclFAIL 0 (str"Not unifiable") gl

+52

-0

test-suite/bugs/closed/2955.v less more

	0	Require Import Coq.Arith.Arith.
	1
	2	Module A.
	3
	4	Fixpoint foo (n:nat) :=
	5	match n with
	6	\| 0 => 0
	7	\| S n => bar n
	8	end
	9
	10	with bar (n:nat) :=
	11	match n with
	12	\| 0 => 0
	13	\| S n => foo n
	14	end.
	15
	16	Lemma using_foo:
	17	forall (n:nat), foo n = 0 /\ bar n = 0.
	18	Proof.
	19	induction n ; split ; auto ;
	20	destruct IHn ; auto.
	21	Qed.
	22
	23	End A.
	24
	25
	26	Module B.
	27
	28	Module A := A.
	29	Import A.
	30
	31	End B.
	32
	33	Module E.
	34
	35	Module B := B.
	36	Import B.A.
	37
	38	(* Bug 1 *)
	39	Lemma test_1:
	40	forall (n:nat), foo n = 0.
	41	Proof.
	42	intros ; destruct n.
	43	reflexivity.
	44	specialize (A.using_foo (S n)) ; intros.
	45	simpl in H.
	46	simpl.
	47	destruct H.
	48	assumption.
	49	Qed.
	50
	51	End E.⏎

+22

-0

test-suite/bugs/closed/shouldsucceed/2629.v less more

	0	Class Join (t: Type) : Type := mkJoin {join: t -> t -> t -> Prop}.
	1
	2	Class sepalg (t: Type) {JOIN: Join t} : Type :=
	3	SepAlg {
	4	join_eq: forall {x y z z'}, join x y z -> join x y z' -> z = z';
	5	join_assoc: forall {a b c d e}, join a b d -> join d c e ->
	6	{f : t & join b c f /\ join a f e};
	7	join_com: forall {a b c}, join a b c -> join b a c;
	8	join_canc: forall {a1 a2 b c}, join a1 b c -> join a2 b c -> a1=a2;
	9
	10	unit_for : t -> t -> Prop := fun e a => join e a a;
	11	join_ex_units: forall a, {e : t & unit_for e a}
	12	}.
	13
	14	Definition joins {A} `{Join A} (a b : A) : Prop :=
	15	exists c, join a b c.
	16
	17	Lemma join_joins {A} `{sepalg A}: forall {a b c},
	18	join a b c -> joins a b.
	19	Proof.
	20	firstorder.
	21	Qed.

+6

-0

test-suite/bugs/closed/shouldsucceed/2668.v less more

	0	Require Import MSetPositive.
	1	Require Import MSetProperties.
	2
	3	Module Pos := MSetPositive.PositiveSet.
	4	Module PPPP := MSetProperties.WPropertiesOn(Pos).
	5	Print Module PPPP.⏎

+15

-0

test-suite/bugs/closed/shouldsucceed/2734.v less more

	0	Require Import Arith List.
	1	Require Import OrderedTypeEx.
	2
	3	Module Adr.
	4	Include Nat_as_OT.
	5	Definition nat2t (i: nat) : t := i.
	6	End Adr.
	7
	8	Inductive expr := Const: Adr.t -> expr.
	9
	10	Inductive control := Go: expr -> control.
	11
	12	Definition program := (Adr.t * (control))%type.
	13
	14	Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ).⏎

+23

-0

test-suite/bugs/closed/shouldsucceed/2750.v less more

	0
	1	Module Type ModWithRecord.
	2
	3	Record foo : Type :=
	4	{ A : nat
	5	; B : nat
	6	}.
	7	End ModWithRecord.
	8
	9	Module Test_ModWithRecord (M : ModWithRecord).
	10
	11	Definition test1 : M.foo :=
	12	{\| M.A := 0
	13	; M.B := 2
	14	\|}.
	15
	16	Module B := M.
	17
	18	Definition test2 : M.foo :=
	19	{\| M.A := 0
	20	; M.B := 2
	21	\|}.
	22	End Test_ModWithRecord.⏎

+11

-0

test-suite/bugs/closed/shouldsucceed/2928.v less more

	0	Class Equiv A := equiv: A -> A -> Prop.
	1	Infix "=" := equiv : type_scope.
	2
	3	Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.
	4
	5	Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.
	6
	7	Class SemiLattice A op `{Equiv A} :=
	8	{ semilattice_sg :>> SemiGroup A op
	9	; redundant : Associative op
	10	}.

+8

-0

test-suite/bugs/closed/shouldsucceed/2983.v less more

	0	Module Type ModA.
	1	End ModA.
	2	Module Type ModB(A : ModA).
	3	End ModB.
	4	Module Foo(A : ModA)(B : ModB A).
	5	End Foo.
	6
	7	Print Module Foo.⏎

+9

-0

test-suite/bugs/closed/shouldsucceed/2995.v less more

	0	Module Type Interface.
	1	Parameter error: nat.
	2	End Interface.
	3
	4	Module Implementation <: Interface.
	5	Definition t := bool.
	6	Definition error: t := false.
	7	Fail End Implementation.
	8	(* A UserError here is expected, not an uncaught Not_found *)⏎

+2

-0

test-suite/bugs/closed/shouldsucceed/3000.v less more

	0	Inductive t (t':Type) : Type := A \| B.
	1	Definition d := match t with _ => 1 end. (* used to fail on list_chop *)

+7

-0

test-suite/bugs/closed/shouldsucceed/3004.v less more

	0	Set Implicit Arguments.
	1	Unset Strict Implicit.
	2	Parameter (M : nat -> Type).
	3	Parameter (mp : forall (T1 T2 : Type) (f : T1 -> T2), list T1 -> list T2).
	4
	5	Definition foo (s : list {n : nat & M n}) :=
	6	let exT := existT in mp (fun x => projT1 x) s.

+29

-0

test-suite/bugs/closed/shouldsucceed/3008.v less more

	0	Module Type Intf1.
	1	Parameter T : Type.
	2	Inductive a := A.
	3	End Intf1.
	4
	5	Module Impl1 <: Intf1.
	6	Definition T := unit.
	7	Inductive a := A.
	8	End Impl1.
	9
	10	Module Type Intf2
	11	(Impl1 : Intf1).
	12	Parameter x : Impl1.A=Impl1.A -> Impl1.T.
	13	End Intf2.
	14
	15	Module Type Intf3
	16	(Impl1 : Intf1)
	17	(Impl2 : Intf2(Impl1)).
	18	End Intf3.
	19
	20	Fail Module Toto
	21	(Impl1' : Intf1)
	22	(Impl2 : Intf2(Impl1'))
	23	(Impl3 : Intf3(Impl1)(Impl2)).
	24	(* A UserError is expected here, not an uncaught Not_found *)
	25
	26	(* NB : the Inductive above and the A=A weren't in the initial test,
	27	they are here only to force an access to the environment
	28	(cf [Printer.qualid_of_global]) and check that this env is ok. *)⏎

+4

-0

test-suite/output/inference.out less more

3	3	\| None => None
4	4	end
5	5	: option L -> option L
	6	fun n : nat => let x := A n in ?12 ?15:T n
	7	: forall n : nat, T n
	8	fun n : nat => ?20 ?23:T n
	9	: forall n : nat, T n

+12

-0

test-suite/output/inference.v less more

11	11	end.
12	12
13	13	Print P.
	14
	15	(* Check that the heuristic to solve constraints is not artificially
	16	dependent on the presence of a let-in, and in particular that the
	17	second [_] below is not inferred to be n, as if obtained by
	18	first-order unification with [T n] of the conclusion [T _] of the
	19	type of the first [_]. *)
	20
	21	(* Note: exact numbers of evars are not important... *)
	22
	23	Inductive T (n:nat) : Type := A : T n.
	24	Check fun n (x:=A n:T n) => _ _ : T n.
	25	Check fun n => _ _ : T n.

+8

-0

test-suite/success/remember.v less more

5	5	Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
6	6	Fail remember nat as X.
7	7	Abort.
	8
	9	(* Testing Ltac interpretation of remember (was not working up to r16181) *)
	10
	11	Goal (1 + 2 + 3 = 6).
	12	let name := fresh "fresh" in
	13	remember (1 + 2) as x eqn:name.
	14	rewrite fresh.
	15	Abort.

+1

-1

theories/Numbers/NatInt/NZOrder.v less more

645	645
646	646	Module NZOrderedType (NZ : NZDecOrdSig')
647	647	<: DecidableTypeFull <: OrderedTypeFull
648		:= NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
	648	:= NZ <+ NZBaseProp <+ NZOrderProp NZ <+ Compare2EqBool <+ HasEqBool2Dec.

+26

-20

toplevel/auto_ind_decl.ml less more

110	110
111	111	let check_bool_is_defined () =
112	112	try let _ = Global.type_of_global Coqlib.glob_bool in ()
113		with _ -> raise (UndefinedCst "bool")
	113	with e when Errors.noncritical e -> raise (UndefinedCst "bool")
114	114
115	115	let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
116	116

303	303	try let u,v = destApp c in
304	304	let indc = destInd u in
305	305	indc,v
306		with _-> let indc = destInd c in
307		indc,[\|\|]
	306	with e when Errors.noncritical e ->
	307	let indc = destInd c in
	308	indc,[\|\|]
308	309
309	310	(*
310	311	In the following, avoid is the list of names to avoid.

328	329	else error ("Var "^(string_of_id s)^" seems unknown.")
329	330	)
330	331	in mkVar (find 1)
331		with _ -> (* if this happen then the args have to be already declared as a
332		Parameter*)
	332	with e when Errors.noncritical e ->
	333	(* if this happen then the args have to be already declared as a
	334	Parameter*)
333	335	(
334	336	let mp,dir,lbl = repr_con (destConst v) in
335	337	mkConst (make_con mp dir (mk_label (

375	377	else error ("Var "^(string_of_id s)^" seems unknown.")
376	378	)
377	379	in mkVar (find 1)
378		with _ -> (* if this happen then the args have to be already declared as a
379		Parameter*)
	380	with e when Errors.noncritical e ->
	381	(* if this happen then the args have to be already declared as a
	382	Parameter*)
380	383	(
381	384	let mp,dir,lbl = repr_con (destConst v) in
382	385	mkConst (make_con mp dir (mk_label (

393	396	else (
394	397	let u,v = try destruct_ind tt1
395	398	(* trick so that the good sequence is returned*)
396		with _ -> ind,[\|\|]
	399	with e when Errors.noncritical e -> ind,[\|\|]
397	400	in if u = ind
398	401	then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
399	402	else (

426	429	\| ([],[]) -> []
427	430	\| _ -> error "Both side of the equality must have the same arity."
428	431	in
429		let (ind1,ca1) = try destApp lft with
430		_ -> error "replace failed."
431		and (ind2,ca2) = try destApp rgt with
432		_ -> error "replace failed."
433		in
434		let (sp1,i1) = try destInd ind1 with
435		_ -> (try fst (destConstruct ind1) with _ ->
436		error "The expected type is an inductive one.")
437		and (sp2,i2) = try destInd ind2 with
438		_ -> (try fst (destConstruct ind2) with _ ->
439		error "The expected type is an inductive one.")
	432	let (ind1,ca1) =
	433	try destApp lft with e when Errors.noncritical e -> error "replace failed."
	434	and (ind2,ca2) =
	435	try destApp rgt with e when Errors.noncritical e -> error "replace failed."
	436	in
	437	let (sp1,i1) =
	438	try destInd ind1 with e when Errors.noncritical e ->
	439	try fst (destConstruct ind1) with e when Errors.noncritical e ->
	440	error "The expected type is an inductive one."
	441	and (sp2,i2) =
	442	try destInd ind2 with e when Errors.noncritical e ->
	443	try fst (destConstruct ind2) with e when Errors.noncritical e ->
	444	error "The expected type is an inductive one."
440	445	in
441	446	if (sp1 <> sp2) \|\| (i1 <> i2)
442	447	then (error "Eq should be on the same type")

713	718	(* Decidable equality *)
714	719
715	720	let check_not_is_defined () =
716		try ignore (Coqlib.build_coq_not ()) with _ -> raise (UndefinedCst "not")
	721	try ignore (Coqlib.build_coq_not ())
	722	with e when Errors.noncritical e -> raise (UndefinedCst "not")
717	723
718	724	(* {n=m}+{n<>m} part *)
719	725	let compute_dec_goal ind lnamesparrec nparrec =

+2

-1

toplevel/autoinstance.ml less more

203	203	(ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
204	204	Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
205	205	new_instance_message ident typ def
206		with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e)
	206	with e when Errors.noncritical e ->
	207	msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e)
207	208
208	209	let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
209	210	match kind_of_term t with

+3

-1

toplevel/backtrack.ml less more

95	95	Stack.push
96	96	{ label = Lib.current_command_label ();
97	97	nproofs = List.length (Pfedit.get_all_proof_names ());
98		prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None);
	98	prfname =
	99	(try Some (Pfedit.get_current_proof_name ())
	100	with Proof_global.NoCurrentProof -> None);
99	101	prfdepth = max 0 (Pfedit.current_proof_depth ());
100	102	reachable = true;
101	103	ngoals = get_ngoals ();

+8

-3

toplevel/classes.ml less more

36	36	let _ =
37	37	Typeclasses.register_add_instance_hint
38	38	(fun inst local pri ->
39		let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in
	39	let path =
	40	try Auto.PathHints [global_of_constr inst]
	41	with e when Errors.noncritical e -> Auto.PathAny
	42	in
40	43	Flags.silently (fun () ->
41	44	Auto.add_hints local [typeclasses_db]
42	45	(Auto.HintsResolveEntry

299	302	let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
300	303	let ce t = Evarutil.check_evars env Evd.empty !evars t in
301	304	List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
302		let ctx = try named_of_rel_context fullctx with _ ->
303		error "Anonymous variables not allowed in contexts."
	305	let ctx =
	306	try named_of_rel_context fullctx
	307	with e when Errors.noncritical e ->
	308	error "Anonymous variables not allowed in contexts."
304	309	in
305	310	let fn (id, _, t) =
306	311	if Lib.is_modtype () && not (Lib.sections_are_opened ()) then

+2

-2

toplevel/coqinit.ml less more

45	45	mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
46	46	" found. Skipping rcfile loading."))
47	47	*)
48		with e ->
	48	with reraise ->
49	49	(msgnl (str"Load of rcfile failed.");
50		raise e)
	50	raise reraise)
51	51	else
52	52	Flags.if_verbose msgnl (str"Skipping rcfile loading.")
53	53

+5

-4

toplevel/coqtop.ml less more

23	23	let ver = input_line ch in
24	24	let rev = input_line ch in
25	25	(ver,rev)
26		with _ -> (Coq_config.version,Coq_config.date)
	26	with e when Errors.noncritical e ->
	27	(Coq_config.version,Coq_config.date)
27	28
28	29	let print_header () =
29	30	let (ver,rev) = (get_version_date ()) in

309	310	with Stream.Failure ->
310	311	msgnl (Errors.print e); exit 1
311	312	end
312		\| e -> begin msgnl (Errors.print e); exit 1 end
	313	\| any -> begin msgnl (Errors.print any); exit 1 end
313	314
314	315	let init arglist =
315	316	Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)

343	344	load_vernacular ();
344	345	compile_files ();
345	346	outputstate ()
346		with e ->
	347	with any ->
347	348	flush_all();
348	349	if not !batch_mode then message "Error during initialization:";
349		msgnl (Toplevel.print_toplevel_error e);
	350	msgnl (Toplevel.print_toplevel_error any);
350	351	exit 1
351	352	end;
352	353	if !batch_mode then

+8

-3

toplevel/himsg.ml less more

27	27	open Printer
28	28	open Glob_term
29	29	open Evd
	30	open Libnames
	31	open Declarations
30	32
31	33	let pr_lconstr c = quote (pr_lconstr c)
32	34	let pr_lconstr_env e c = quote (pr_lconstr_env e c)

306	308	let fixenv = make_all_name_different fixenv in
307	309	let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in
308	310	str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
309		with _ -> mt ())
	311	with e when Errors.noncritical e -> mt ())
310	312
311	313	let explain_ill_typed_rec_body env sigma i names vdefj vargs =
312	314	let vdefj = jv_nf_evar sigma vdefj in

541	543	str "types given to " ++ str (string_of_id id) ++ str " differ"
542	544	\| NotConvertibleBodyField ->
543	545	str "the body of definitions differs"
544		\| NotConvertibleTypeField ->
545		str "types differ"
	546	\| NotConvertibleTypeField (env, typ1, typ2) ->
	547	str "expected type" ++ spc () ++
	548	quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++
	549	str "but found type" ++ spc () ++
	550	quote (Printer.safe_pr_lconstr_env env typ1)
546	551	\| NotSameConstructorNamesField ->
547	552	str "constructor names differ"
548	553	\| NotSameInductiveNameInBlockField ->

+3

-3

toplevel/ide_intf.ml less more

88	88	\| Quit -> Obj.magic (handler.quit () : unit)
89	89	\| About -> Obj.magic (handler.about () : coq_info)
90	90	in Good res
91		with e ->
92		let (l, str) = handler.handle_exn e in
	91	with any ->
	92	let (l, str) = handler.handle_exn any in
93	93	Fail (l,str)
94	94
95	95	(** * XML data marshalling *)

274	274	let loc_s = int_of_string (List.assoc "loc_s" attrs) in
275	275	let loc_e = int_of_string (List.assoc "loc_e" attrs) in
276	276	Some (loc_s, loc_e)
277		with _ -> None
	277	with e when e <> Sys.Break -> None
278	278	in
279	279	let msg = raw_string l in
280	280	Fail (loc, msg)

+6

-5

toplevel/ide_slave.ml less more

236	236	in
237	237	let proof =
238	238	try Some (Names.string_of_id (Proof_global.get_current_proof_name ()))
239		with _ -> None
	239	with Proof_global.NoCurrentProof -> None
240	240	in
241	241	let allproofs =
242	242	let l = Proof_global.get_all_proof_names () in

258	258	\| (Interface.Name_Pattern s, b) :: l ->
259	259	let regexp =
260	260	try Str.regexp s
261		with _ -> Util.error ("Invalid regexp: " ^ s)
	261	with e when Errors.noncritical e ->
	262	Util.error ("Invalid regexp: " ^ s)
262	263	in
263	264	extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
264	265	\| (Interface.Type_Pattern s, b) :: l ->

453	454	Xml_utils.print_xml !orig_stdout xml_answer;
454	455	flush !orig_stdout
455	456	done
456		with e ->
457		let msg = Printexc.to_string e in
	457	with any ->
	458	let msg = Printexc.to_string any in
458	459	let r = "Fatal exception in coqtop:\n" ^ msg in
459	460	pr_debug ("==> " ^ r);
460	461	(try
461	462	Xml_utils.print_xml !orig_stdout (fail r);
462	463	flush !orig_stdout
463		with _ -> ());
	464	with any -> ());
464	465	exit 1

+3

-2

toplevel/ind_tables.ml less more

85	85	(Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
86	86
87	87	let declare_scheme_object s aux f =
88		(try check_ident ("ind"^s) with _ ->
89		error ("Illegal induction scheme suffix: "^s));
	88	(try check_ident ("ind"^s)
	89	with e when Errors.noncritical e ->
	90	error ("Illegal induction scheme suffix: "^s));
90	91	let key = if aux = "" then s else aux in
91	92	try
92	93	let _ = Hashtbl.find scheme_object_table key in

+4

-3

toplevel/indschemes.ml less more

158	158	(strbrk "Required constant " ++ str s ++ str " undefined.")
159	159	\| AlreadyDeclared msg ->
160	160	alarm what internal (msg ++ str ".")
161		\| _ ->
	161	\| e when Errors.noncritical e ->
162	162	alarm what internal
163	163	(str "Unknown exception during scheme creation.")
164	164

244	244
245	245	let declare_eq_decidability = declare_eq_decidability_scheme_with []
246	246
247		let ignore_error f x = try ignore (f x) with _ -> ()
	247	let ignore_error f x =
	248	try ignore (f x) with e when Errors.noncritical e -> ()
248	249
249	250	let declare_rewriting_schemes ind =
250	251	if Hipattern.is_inductive_equality ind then begin

265	266	if Hipattern.is_equality_type (mkInd ind) then begin
266	267	if
267	268	try Coqlib.check_required_library Coqlib.logic_module_name; true
268		with _ -> false
	269	with e when Errors.noncritical e -> false
269	270	then
270	271	ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
271	272	else

+18

-9

toplevel/lemmas.ml less more

228	228	id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
229	229
230	230	let save_named opacity =
231		let id,const,do_guard,persistence,hook = get_proof opacity in
232		save id const do_guard persistence hook
	231	let p = Proof_global.give_me_the_proof () in
	232	Proof.transaction p begin fun () ->
	233	let id,const,do_guard,persistence,hook = get_proof opacity in
	234	save id const do_guard persistence hook
	235	end
233	236
234	237	let check_anonymity id save_ident =
235	238	if atompart_of_id id <> string_of_id (default_thm_id) then
236	239	error "This command can only be used for unnamed theorem."
237	240
238	241	let save_anonymous opacity save_ident =
239		let id,const,do_guard,persistence,hook = get_proof opacity in
240		check_anonymity id save_ident;
241		save save_ident const do_guard persistence hook
	242	let p = Proof_global.give_me_the_proof () in
	243	Proof.transaction p begin fun () ->
	244	let id,const,do_guard,persistence,hook = get_proof opacity in
	245	check_anonymity id save_ident;
	246	save save_ident const do_guard persistence hook
	247	end
242	248
243	249	let save_anonymous_with_strength kind opacity save_ident =
244		let id,const,do_guard,_,hook = get_proof opacity in
245		check_anonymity id save_ident;
246		(* we consider that non opaque behaves as local for discharge *)
247		save save_ident const do_guard (Global, Proof kind) hook
	250	let p = Proof_global.give_me_the_proof () in
	251	Proof.transaction p begin fun () ->
	252	let id,const,do_guard,_,hook = get_proof opacity in
	253	check_anonymity id save_ident;
	254	(* we consider that non opaque behaves as local for discharge *)
	255	save save_ident const do_guard (Global, Proof kind) hook
	256	end
248	257
249	258	(* Starting a goal *)
250	259

+9

-4

toplevel/metasyntax.ml less more

236	236	\| _ -> error "Box closed without being opened in format."
237	237	else
238	238	error "Empty format."
239		with e ->
	239	with e when Errors.noncritical e ->
240	240	Loc.raise loc e
241	241
242	242	(***********************)

276	276
277	277	let out_nt = function NonTerminal x -> x \| _ -> assert false
278	278
	279	let msg_expected_form_of_recursive_notation =
	280	"In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
	281
279	282	let rec find_pattern nt xl = function
280	283	\| Break n as x :: l, Break n' :: l' when n=n' ->
281	284	find_pattern nt (x::xl) (l,l')

288	291	\| _, Break s :: _ \| Break s :: _, _ ->
289	292	error ("A break occurs on one side of \"..\" but not on the other side.")
290	293	\| _, [] ->
291		error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
	294	error msg_expected_form_of_recursive_notation
292	295	\| ((SProdList _ \| NonTerminal _) :: _), _ \| _, (SProdList _ :: _) ->
293	296	anomaly "Only Terminal or Break expected on left, non-SProdList on right"
294	297
295	298	let rec interp_list_parser hd = function
296	299	\| [] -> [], List.rev hd
297	300	\| NonTerminal id :: tl when id = ldots_var ->
	301	if hd = [] then error msg_expected_form_of_recursive_notation;
298	302	let hd = List.rev hd in
299	303	let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
300	304	let xyl,tl'' = interp_list_parser [] tl' in

336	340	let is_numeral symbs =
337	341	match List.filter (function Break _ -> false \| _ -> true) symbs with
338	342	\| ([Terminal "-"; Terminal x] \| [Terminal x]) ->
339		(try let _ = Bigint.of_string x in true with _ -> false)
	343	(try let _ = Bigint.of_string x in true
	344	with e when Errors.noncritical e -> false)
340	345	\| _ ->
341	346	false
342	347

994	999	let with_lib_stk_protection f x =
995	1000	let fs = Lib.freeze () in
996	1001	try let a = f x in Lib.unfreeze fs; a
997		with e -> Lib.unfreeze fs; raise e
	1002	with reraise -> Lib.unfreeze fs; raise reraise
998	1003
999	1004	let with_syntax_protection f x =
1000	1005	with_lib_stk_protection

+6

-5

toplevel/mltop.ml4 less more

91	91	(try t.load_obj s
92	92	with
93	93	\| (UserError _ \| Failure _ \| Anomaly _ \| Not_found as u) -> raise u
94		\| _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
95		str s ++ str" to Coq code."))
	94	\| e when Errors.noncritical e ->
	95	errorlabstrm "Mltop.load_object"
	96	(str"Cannot link ml-object " ++ str s ++ str" to Coq code."))
96	97	(* TO DO: .cma loading without toplevel *)
97	98	\| WithoutTop ->
98	99	IFDEF HasDynlink THEN

141	142
142	143	let convert_string d =
143	144	try Names.id_of_string d
144		with _ ->
	145	with e when Errors.noncritical e ->
145	146	if_warn msg_warning
146	147	(str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
147	148	flush_all ();

268	269	try
269	270	f name fname;
270	271	msgnl (str (info^" done]"));
271		with e ->
	272	with reraise ->
272	273	msgnl (str (info^" failed]"));
273		raise e
	274	raise reraise
274	275
275	276	(** Load a module for the first time (i.e. dynlink it)
276	277	or simulate its reload (i.e. doing nothing except maybe

+1

-1

toplevel/search.ml less more

136	136	try
137	137	try
138	138	is_matching pat (head c)
139		with _ ->
	139	with e when Errors.noncritical e ->
140	140	is_matching
141	141	pat (head (Typing.type_of (Global.env()) Evd.empty c))
142	142	with UserError _ ->

+6

-6

toplevel/toplevel.ml less more

179	179	str", line " ++ int line ++ str", characters " ++
180	180	Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++
181	181	fnl ()
182		with e ->
	182	with e when Errors.noncritical e ->
183	183	(close_in ic;
184	184	hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
185	185

207	207	let make_prompt () =
208	208	try
209	209	(Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < "
210		with _ ->
	210	with Proof_global.NoCurrentProof ->
211	211	"Coq < "
212	212
213	213	(*let build_pending_list l =

339	339	discard_to_dot (); e
340	340	with
341	341	\| End_of_input -> End_of_input
342		\| de -> if is_pervasive_exn de then de else e
	342	\| any -> if is_pervasive_exn any then any else e
343	343
344	344	(* do_vernac reads and executes a toplevel phrase, and print error
345	345	messages when an exception is raised, except for the following:

353	353	begin
354	354	try
355	355	raw_do_vernac top_buffer.tokens
356		with e ->
357		msgnl (print_toplevel_error (process_error e))
	356	with any ->
	357	msgnl (print_toplevel_error (process_error any))
358	358	end;
359	359	flush_all()
360	360

373	373	\| Vernacexpr.Drop -> ()
374	374	\| End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
375	375	\| Vernacexpr.Quit -> exit 0
376		\| e ->
	376	\| any ->
377	377	msgerrnl (str"Anomaly. Please report.");
378	378	loop ()

+12

-12

toplevel/vernac.ml less more

155	155	match verb with
156	156	\| Some verb_ch -> close_in verb_ch
157	157	\| _ -> ()
158		with _ -> ()
	158	with e when Errors.noncritical e -> ()
159	159
160	160	let verbose_phrase verbch loc =
161	161	let loc = unloc loc in

231	231	Lexer.restore_com_state cs;
232	232	Pp.comments := cl;
233	233	Dumpglob.coqdoc_unfreeze cds
234		with e ->
	234	with reraise ->
235	235	if !Flags.beautify_file then close_out !chan_beautify;
236	236	chan_beautify := ch;
237	237	Lexer.restore_com_state cs;
238	238	Pp.comments := cl;
239	239	Dumpglob.coqdoc_unfreeze cds;
240		raise e
	240	raise reraise
241	241	end
242	242
243	243	\| VernacList l -> List.iter (fun (_,v) -> interp v) l

249	249	(* If the command actually works, ignore its effects on the state *)
250	250	States.with_state_protection
251	251	(fun v -> interp v; raise HasNotFailed) v
252		with e -> match real_error e with
	252	with e when Errors.noncritical e -> match real_error e with
253	253	\| HasNotFailed ->
254	254	errorlabstrm "Fail" (str "The command has not failed !")
255	255	\| e ->

277	277	States.with_heavy_rollback interpfun
278	278	Cerrors.process_vernac_interp_error v;
279	279	restore_timeout psh
280		with e -> restore_timeout psh; raise e
	280	with reraise -> restore_timeout psh; raise reraise
281	281	in
282	282	try
283	283	checknav loc com;
284	284	current_timeout := !default_timeout;
285	285	if do_beautify () then pr_new_syntax loc (Some com);
286	286	interp com
287		with e ->
	287	with any ->
288	288	Format.set_formatter_out_channel stdout;
289		raise (DuringCommandInterp (loc, e))
	289	raise (DuringCommandInterp (loc, any))
290	290
291	291	and read_vernac_file verbosely s =
292	292	Flags.make_warn verbosely;

315	315	end_inner_command (snd loc_ast);
316	316	pp_flush ()
317	317	done
318		with e -> (* whatever the exception *)
	318	with reraise -> (* whatever the exception *)
319	319	Format.set_formatter_out_channel stdout;
320	320	close_input in_chan input; (* we must close the file first *)
321		match real_error e with
	321	match real_error reraise with
322	322	\| End_of_input ->
323	323	if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
324		\| _ -> raise_with_file fname e
	324	\| _ -> raise_with_file fname reraise
325	325
326	326	(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit]
327	327	It executes one vernacular command. By default the command is

358	358	Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
359	359	read_vernac_file verb file;
360	360	if !Flags.beautify_file then close_out !chan_beautify;
361		with e ->
	361	with reraise ->
362	362	if !Flags.beautify_file then close_out !chan_beautify;
363		raise_with_file file e
	363	raise_with_file file reraise
364	364
365	365	(* Compile a vernac file (f is assumed without .v suffix) *)
366	366	let compile verbosely f =

+8

-5

toplevel/vernacentries.ml less more

294	294	close ();
295	295	msgnl (str ("Universes written to file \""^s^"\"."))
296	296	with
297		e -> close (); raise e
	297	reraise -> close (); raise reraise
298	298
299	299	let dump_universes sorted s =
300	300	let g = Global.universes () in

330	330	let print_located_library r =
331	331	let (loc,qid) = qualid_of_reference r in
332	332	try msg_found_library (Library.locate_qualified_library false qid)
333		with e -> msg_notfound_library loc qid e
	333	with e when Errors.noncritical e -> msg_notfound_library loc qid e
334	334
335	335	let print_located_module r =
336	336	let (loc,qid) = qualid_of_reference r in

363	363	try
364	364	let gr = Smartlocate.smart_global r in
365	365	Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr
366		with _ -> ()
	366	with e when Errors.noncritical e -> ()
367	367	(**********)
368	368	(* Syntax *)
369	369

387	387	(* Gallina *)
388	388
389	389	let start_proof_and_print k l hook =
	390	check_locality (); (* early check, cf #2975 *)
390	391	start_proof_com k l hook;
391	392	print_subgoals ();
392	393	if !pcoq <> None then (Option.get !pcoq).start_proof ()

909	910	\| None -> None
910	911	\| Some (o, k) ->
911	912	try Some(ignore(Notation.find_scope k); k)
912		with _ -> Some (Notation.find_delimiters_scope o k)) scopes in
	913	with e when Errors.noncritical e ->
	914	Some (Notation.find_delimiters_scope o k)) scopes
	915	in
913	916	let some_scopes_specified = List.exists ((<>) None) scopes in
914	917	let rargs =
915	918	Util.list_map_filter (function (n, true) -> Some n \| _ -> None)

1416	1419	let gr = Smartlocate.global_with_alias (Ident id) in
1417	1420	Dumpglob.add_glob (fst id) gr;
1418	1421	true
1419		with _ -> false in
	1422	with e when Errors.noncritical e -> false in
1420	1423
1421	1424	if not globalized then begin
1422	1425	try begin match Lib.find_opening_node (snd id) with

+2

-2

toplevel/vernacinterp.ml less more

59	59	hunk()
60	60	with
61	61	\| Drop -> raise Drop
62		\| e ->
	62	\| reraise ->
63	63	if !Flags.debug then
64	64	msgnl (str"Vernac Interpreter " ++ str !loc);
65		raise e
	65	raise reraise