Commit 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 - coq

+2

-0

.gitignore less more

72	72	coqdoc.sty
73	73	ide/index_urls.txt
74	74	doc/faq/html/
	75	doc/refman/csdp.cache
	76	doc/refman/trace
75	77	doc/refman/Reference-Manual.pdf
76	78	doc/refman/Reference-Manual.ps
77	79	doc/refman/cover.html

+44

-0

CHANGES less more

	0	Changes from V8.3pl1 to V8.3pl2
	1	===============================
	2
	3	Coqdoc and documentation bugs
	4
	5	- #2470 (use "membership" instead of "appartness")
	6	- #2475 (documentation of the "f binders := t" notation for record fields)
	7	- Documentation of module String on coq.inria.fr/stdlib
	8
	9	Tactics
	10
	11	- #2493 (dependent pairs injection failing because of Type cumulativity missing)
	12	- Reduction "simpl" sometimes failing in presence of names redefined in modules
	13
	14	Extraction
	15
	16	- #2359 (Some unnecessary unsafe casts are now avoided (bug in the type checker)).
	17	- #2469 (fix Extract Inlined Constant for Haskell and Scheme)
	18	- #2476 (Fix indentation of default pattern in haskell case)
	19	- #2477 (Avoid printing unused mutual fix components)
	20	- #2478 (Add missing parenthesis around emulated pattern-match)
	21	- #2482 (Extract Inductive on singleton inductives)
	22	- #2484 (Avoid an assert failure with -dont-load-proofs)
	23	- #2497 (malformed Haskell extraction of deeply-nested match expressions)
	24	- #2515 (Allow extracting Ascii.ascii to native Char in Haskell)
	25	- #2525 (Nicer error when a toplevel module has no body)
	26	- Fix printing of haskell modular names
	27
	28	Miscellaneous bug fixes
	29
	30	- #2487 (compilation with camlp5 in strict mode)
	31	- #2283, #2460 (new option "Set Default Timeout n / Unset Default Timeout")
	32	- #2524 (In win32, the exit code of coqc should be correct now)
	33	- Now, vm_compute is responsive to Ctrl-C interruption, as the rest of coqtop
	34	- Fixed uncaught exception when vmcast used in Check
	35	- coqdep complies with the -R visibility discipline
	36	- Fixing printing of f when defined using "Notation f x := ..."
	37	- Fixing Unset for options setting integer values
	38	- Excluding admitted subgoals from Search/SearchAbout
	39
0	40	Changes from V8.3 to V8.3pl1
1	41	============================
2	42

47	87	- #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes)
48	88	- a few improvements in efficiency
49	89
	90
	91	Extraction
	92
	93	- The pretty-printer for Haskell now produces layout-independant code
50	94
51	95	Changes from V8.2 to V8.3
52	96	=========================

+0

-8

~~Coq.bat~~ less more

0		@echo off
1		set COQBIN=%~0\..\bin
2		set COQLIB=%~0\..\lib
3		echo Using COQBIN= %COQBIN%
4		echo and COQLIB= %COQLIB%
5		echo Starting Coq
6		%~0\..\bin\coqtop.opt.exe
7		pause⏎

+0

-7

~~Coqide.bat~~ less more

0		@echo off
1		set COQBIN=%~0\..\bin
2		set COQLIB=%~0\..\lib
3		echo Using COQBIN= %COQBIN%
4		echo and COQLIB= %COQLIB%
5		echo Starting Coqide
6		%~0\..\bin\coqide.opt.exe⏎

+2

-2

INSTALL less more

40	40
41	41	Should you need or prefer to compile Coq V8.3 yourself, you need:
42	42
43		- Objective Caml version 3.09.3 or later
	43	- Objective Caml version 3.10.2 or later
44	44	(available at http://caml.inria.fr/)
45	45
46	46	For Objective Caml version >= 3.10.0, you also need to install

87	87	INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
88	88	=================================================
89	89
90		1- Check that you have the Objective Caml compiler version 3.09.3 (or later)
	90	1- Check that you have the Objective Caml compiler version 3.10.2 (or later)
91	91	installed on your computer and that "ocamlmktop" and "ocamlc" (or
92	92	its native code version "ocamlc.opt") lie in a directory which is present
93	93	in your $PATH environment variable.

+1

-1

INSTALL.ide less more

22	22	Else, read the rest of this document to compile your own CoqIde.
23	23
24	24	REQUIREMENT:
25		- OCaml >= 3.09.3 with native threads support.
	25	- OCaml >= 3.10.2 with native threads support.
26	26	- make world must succeed.
27	27	- The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
28	28	The official supported version is at least 2.10.x.

+8

-4

README.win less more

8	8	The Coq package for Windows comes with an auto-installer. It will
9	9	install Coq binaries and libraries under any directory you specify
10	10	(C:\Program Files\Coq is the default path). It also creates shortcuts
11		in the Windows menus. Alternatively, you can launch Coq using Coq.bat
12		and Coqide.bat in the installation directory (C:\Program Files\Coq by
13		default).
	11	in the Windows menus. Alternatively, you can launch Coq using coqide.exe
	12	or coqtop.exe in the bin sub-directory of the installation
	13	(C:\Program Files\Coq\bin by default).
14	14
15	15	COMPILATION.
16	16	============

19	19	distribution. If you really need to recompile under Windows, here
20	20	are some indications:
21	21
22		1- Install ocaml for Windows (MinGW port), at least version 3.09.3.
	22	1- Install ocaml for Windows (MinGW port), at least version 3.10.2.
23	23	See: http://caml.inria.fr
24	24
25	25	2- Install a shell environment with at least:

51	51
52	52	Good luck :-)
53	53
	54	Alternatively, it is now possible (and even recommended ...) to build
	55	Windows executables of coq from Linux thanks to a mingw cross-compiler.
	56	If interested, please contact us for more details.
	57
54	58	The Coq Team.

+1

-0

_tags less more

9	9	<tools/coqdoc/main.{native,byte}> : use_str
10	10	<checker/main.{native,byte}> : use_str, use_unix, use_gramlib
11	11	<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
	12	<tools/mkwinapp.{native,byte}> : use_unix
12	13
13	14	## tags for ide
14	15

+4

-14

configure less more

5	5	#
6	6	##################################
7	7
8		VERSION=8.3pl1
	8	VERSION=8.3pl2
9	9	VOMAGIC=08300
10	10	STATEMAGIC=58300
11	11	DATE=`LANG=C date +"%B %Y"`

410	410	CAMLVERSION=`"$bytecamlc" -version`
411	411
412	412	case $CAMLVERSION in
413		1.\|2.\|3.00\|3.01\|3.02\|3.03\|3.03alpha\|3.04\|3.05beta\|3.05\|3.06\|3.07\|3.08\|3.09.[012])
	413	1.\|2.\|3.00\|3.01\|3.02\|3.03\|3.03alpha\|3.04\|3.05beta\|3.05\|3.06\|3.07\|3.08\|3.09*)
414	414	echo "Your version of Objective-Caml is $CAMLVERSION."
415	415	if [ "$force_caml_version" = "yes" ]; then
416	416	echo "Warning You are compiling Coq with an outdated version of Objective-Caml."
417	417	else
418		echo " You need Objective-Caml 3.09.3 or later."
	418	echo " You need Objective-Caml 3.10.2 or later."
419	419	echo " Configuration script failed!"
420	420	exit 1
421	421	fi;;

490	490	exit 1
491	491	fi
492	492	camlp4oexec=`echo $camlp4oexec \| sed -e 's/4/5/'`
493		if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
494		echo "Error: Camlp5 found, but in strict mode!"
495		echo "Please compile Camlp5 in transitional mode."
496		exit 1
497		fi
498	493	else
499	494	case $CAMLTAG in
500	495	OCAML31*)

509	504	fi
510	505	CAMLP4=camlp5
511	506	camlp4oexec=`echo $camlp4oexec \| sed -e 's/4/5/'`
512		if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
513		echo "Error: Camlp5 found, but in strict mode!"
514		echo "Please compile Camlp5 in transitional mode."
515		exit 1
516		fi
517	507	;;
518	508	*)
519	509	CAMLP4=camlp4

1093	1083	echo "Warning To compile the system for a new architecture"
1094	1084	echo " don't forget to do a 'make archclean' before './configure'."
1095	1085
1096		# $Id: configure 13740 2010-12-23 12:37:18Z notin $
	1086	# $Id: configure 14025 2011-04-19 07:19:00Z notin $

+5

-5

doc/refman/RefMan-ext.tex less more

23	23	&& ~~~~\zeroone{\ident}
24	24	\verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
25	25	& & \\
26		{\field} & ::= & {\name} : {\type} [ {\tt where} {\it notation} ] \\
27		& $\|$ & {\name} {\typecstr} := {\term}
	26	{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\
	27	& $\|$ & {\name} \zeroone{\binders} {\typecstr} := {\term}
28	28	\end{tabular}
29	29	\end{centerframe}
30	30	\caption{Syntax for the definition of {\tt Record}}

36	36	\smallskip
37	37	{\tt Record} {\ident} {\params} \texttt{:}
38	38	{\sort} := {\ident$_0$} \verb+{+
39		{\ident$_1$} \texttt{:} {\term$_1$};
	39	{\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$};
40	40	\dots
41		{\ident$_n$} \texttt{:} {\term$_n$} \verb+}+.
	41	{\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+.
42	42	\smallskip
43	43
44	44	\noindent the identifier {\ident} is the name of the defined record

46	46	its constructor. If {\ident$_0$} is omitted, the default name {\tt
47	47	Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''.
48	48	The identifiers {\ident$_1$}, ..,
49		{\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$}
	49	{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$}
50	50	their respective types. Remark that the type of {\ident$_i$} may
51	51	depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the
52	52	fields is important. Finally, {\params} are the parameters of the

+16

-1

doc/refman/RefMan-oth.tex less more

928	928	(time expressed in seconds), then it is interrupted and an error message
929	929	is displayed.
930	930
	931	\subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set
	932	Default Timeout \textrm{\textsl{int}}.\comindex{Set Default Timeout}}
	933
	934	After using this command, all subsequent commands behave as if they
	935	were passed to a {\tt Timeout} command. Commands already starting by
	936	a {\tt Timeout} are unaffected.
	937
	938	\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
	939
	940	This command turns off the use of a defaut timeout.
	941
	942	\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
	943
	944	This command displays whether some default timeout has be set or not.
	945
931	946	\section{Controlling display}
932	947
933	948	\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}

1172	1187	\end{itemize}
1173	1188
1174	1189
1175		% $Id: RefMan-oth.tex 13454 2010-09-23 17:00:29Z aspiwack $
	1190	% $Id: RefMan-oth.tex 13923 2011-03-21 16:25:20Z letouzey $
1176	1191
1177	1192	%%% Local Variables:
1178	1193	%%% mode: latex

+2

-2

doc/stdlib/index-list.html.template less more

451	451	theories/FSets/FMapFullAVL.v
452	452	</dd>
453	453
454		<!-- <dt> <b>Strings</b>
	454	<dt> <b>Strings</b>
455	455	Implementation of string as list of ascii characters
456	456	</dt>
457	457	<dd>
458	458	theories/Strings/Ascii.v
459	459	theories/Strings/String.v
460		</dd> -->
	460	</dd>
461	461
462	462	<dt> <b>Reals</b>:
463	463	Formalization of real numbers

+3

-7

ide/coq.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: coq.ml 13431 2010-09-18 08:15:29Z herbelin $ *)
	8	(* $Id: coq.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
9	9
10	10	open Vernac
11	11	open Vernacexpr

26	26	open Namegen
27	27	open Ideutils
28	28
29		let prerr_endline s = if !debug then prerr_endline s else ()
30
31		let output = ref (Format.formatter_of_out_channel stdout)
32
33	29	let msg m =
34	30	let b = Buffer.create 103 in
35	31	Pp.msg_with (Format.formatter_of_buffer b) m;

393	389	}
394	390
395	391	let reset_initial () =
396		prerr_endline "Reset initial called"; flush stderr;
	392	prerr_endline "Reset initial called";
397	393	Vernacentries.abort_refine Lib.reset_initial ()
398	394
399	395	let reset_to sp =

411	407	let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
412	408	(* Temporary hack to make coqide.byte work (WTF???) - now with less screen
413	409	* pollution *)
414		Pervasives.prerr_string " \r"; Pervasives.flush stderr;
	410	(try Pervasives.prerr_string " \r"; Pervasives.flush stderr with _ -> ());
415	411	match pe with
416	412	\| None -> assert false
417	413	\| Some((loc,vernac) as last) ->

+1

-0

ide/coq_icon.rc less more

0

large ICON ide/coq.ico

+10

-10

ide/coqide.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: coqide.ml 13708 2010-12-13 14:49:29Z gmelquio $ *)
	8	(* $Id: coqide.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
9	9
10	10	open Preferences
11	11	open Vernacexpr

199	199
200	200	let crash_save i =
201	201	(* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
202		Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
	202	safe_prerr_endline "Trying to save all buffers in .crashcoqide files";
203	203	let count = ref 0 in
204	204	List.iter
205	205	(function {script=view; analyzed_view = av } ->

211	211	in
212	212	try
213	213	if try_export filename (view#buffer#get_text ()) then
214		Pervasives.prerr_endline ("Saved "^filename)
215		else Pervasives.prerr_endline ("Could not save "^filename)
216		with _ -> Pervasives.prerr_endline ("Could not save "^filename))
	214	safe_prerr_endline ("Saved "^filename)
	215	else safe_prerr_endline ("Could not save "^filename)
	216	with _ -> safe_prerr_endline ("Could not save "^filename))
217	217	)
218	218	session_notebook#pages;
219		Pervasives.prerr_endline "Done. Please report.";
	219	safe_prerr_endline "Done. Please report.";
220	220	if i <> 127 then exit i
221	221
222	222	let ignore_break () =

3201	3201	"\nCoq is developed by the Coq Development Team\
3202	3202	\n(INRIA - CNRS - University Paris 11 and partners)\
3203	3203	\nWeb site: " ^ Coq_config.wwwcoq ^
3204		"\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
	3204	"\nFeature wish or bug report: http://coq.inria.fr/bugs\
3205	3205	\n\
3206	3206	\nCredits for CoqIDE, the Integrated Development Environment for Coq:\
3207	3207	\n\

3331	3331	try
3332	3332	GtkThread.main ()
3333	3333	with
3334		\| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
	3334	\| Sys.Break -> prerr_endline "Interrupted."
3335	3335	\| e ->
3336		Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
3337		flush stderr;
	3336	safe_prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
	3337	flush_all ();
3338	3338	crash_save 127
3339	3339	done
3340	3340

+7

-3

ide/ideutils.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: ideutils.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: ideutils.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
9	9
10	10
11	11	open Preferences

30	30
31	31	let pbar = GRange.progress_bar ~pulse_step:0.2 ()
32	32
	33	(* On a Win32 application with no console, writing to stderr raise
	34	a Sys_error "bad file descriptor" *)
	35	let safe_prerr_endline msg = try prerr_endline msg with _ -> ()
	36
33	37	let debug = Flags.debug
34	38
35	39	let prerr_endline s =
36		if !debug then (prerr_endline s;flush stderr)
	40	if !debug then try (prerr_endline s;flush stderr) with _ -> ()
37	41	let prerr_string s =
38		if !debug then (prerr_string s;flush stderr)
	42	if !debug then try (prerr_string s;flush stderr) with _ -> ()
39	43
40	44	let lib_ide_file f =
41	45	let coqlib = Envars.coqlib () in

+2

-1

ide/ideutils.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: ideutils.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: ideutils.mli 13751 2010-12-24 09:56:05Z letouzey $ i)
9	9
10	10	val async : ('a -> unit) -> 'a -> unit
11	11	val sync : ('a -> 'b) -> 'a -> 'b

33	33	val lib_ide_file : string -> string
34	34	val my_stat : string -> Unix.stats option
35	35
	36	val safe_prerr_endline : string -> unit
36	37	val prerr_endline : string -> unit
37	38	val prerr_string : string -> unit
38	39	val print_id : 'a -> unit

+1

-3

ide/utils/configwin_messages.ml less more

29	29
30	30	let html_config = "Configwin bindings configurator for html parameters"
31	31
32		let home =
33		try Sys.getenv "HOME"
34		with Not_found -> ""
	32	let home = System.home
35	33
36	34	let mCapture = "Capture";;
37	35	let mType_key = "Type key" ;;

+15

-12

interp/constrextern.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
	8	(* $Id: constrextern.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
9	9
10	10	(i)
11	11	open Pp

342	342	(fun (loc,p) -> CPatPrim (loc,p))
343	343	destPatPrim terms
344	344
	345	let mkPat loc qid l =
	346	(* Normally irrelevant test with v8 syntax, but let's do it anyway *)
	347	if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l)
	348
345	349	(* Better to use extern_rawconstr composed with injection/retraction ?? *)
346	350	let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
347	351	try

396	400	(match keyrule with
397	401	\| NotationRule (sc,ntn) -> raise No_match
398	402	\| SynDefRule kn ->
399		let p =
400		let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
401		if l = [] then
402		CPatAtom (loc,Some qid)
403		else
404		let l =
405		List.map (extern_cases_pattern_in_scope allscopes vars) l in
406		CPatCstr (loc,qid,l) in
407		insert_pat_alias loc p na)
	403	let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
	404	let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in
	405	insert_pat_alias loc (mkPat loc qid l) na)
408	406	\| PatCstr (_,f,l,_), Some n when List.length l > n ->
409	407	raise No_match
410	408	\| PatCstr (loc,_,_,na),_ ->

431	429	insert_pat_delimiters loc
432	430	(make_pat_notation loc ntn (l,ll)) key)
433	431	\| SynDefRule kn ->
434		let qid = shortest_qualid_of_syndef vars kn in
435		CPatAtom (loc,Some (Qualid (loc, qid))) in
	432	let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
	433	let l =
	434	List.map (fun (c,(scopt,scl)) ->
	435	extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
	436	subst in
	437	assert (substlist = []);
	438	mkPat loc qid l in
436	439	insert_pat_alias loc p na
437	440	\| PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
438	441	\| PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))

+13

-1

kernel/byterun/coq_interp.c less more

13	13	for fast computation of bounded (31bits) integers */
14	14
15	15	#include <stdio.h>
	16	#include <signal.h>
16	17	#include "coq_gc.h"
17	18	#include "coq_instruct.h"
18	19	#include "coq_fix_code.h"

156	157	#endif
157	158	#endif
158	159
	160	/* For signal handling, we highjack some code from the caml runtime */
	161
	162	extern intnat caml_signals_are_pending;
	163	extern intnat caml_pending_signals[];
	164	extern void caml_process_pending_signals(void);
	165
159	166	/* The interpreter itself */
160	167
161	168	value coq_interprete

413	420	realloc_coq_stack(Coq_stack_threshold);
414	421	sp = coq_sp;
415	422	}
	423	/* We also check for signals */
	424	if (caml_signals_are_pending) {
	425	/* If there's a Ctrl-C, we reset the vm */
	426	if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
	427	caml_process_pending_signals();
	428	}
416	429	Next;
417		/* Fall through CHECK_SIGNALS */
418	430
419	431	Instruct(APPTERM) {
420	432	int nargs = *pc++;

+6

-2

kernel/names.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: names.ml 13486 2010-10-03 17:01:43Z herbelin $ *)
	8	(* $Id: names.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
9	9
10	10	open Pp
11	11	open Util

222	222
223	223	let constant_of_kn kn = (kn,kn)
224	224	let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
225		let make_con mp dir l = ((mp,dir,l),(mp,dir,l))
	225	let make_con mp dir l = constant_of_kn (mp,dir,l)
226	226	let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
227	227	let canonical_con con = snd con
228	228	let user_con con = fst con

233	233	let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++ str ")"
234	234	let eq_constant (_,kn1) (_,kn2) = kn1=kn2
235	235	let debug_string_of_con con = string_of_kn (fst con)^"'"^string_of_kn (snd con)
	236
	237	let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
	238	if lbl = l1 && lbl = l2 then con
	239	else ((mp1,dp1,lbl),(mp2,dp2,lbl))
236	240
237	241	let con_modpath con = modpath (fst con)
238	242

+2

-1

kernel/names.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: names.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: names.mli 13804 2011-01-27 00:41:34Z letouzey $ i)
9	9
10	10	(s Identifiers )
11	11

138	138	val canonical_con : constant -> kernel_name
139	139	val repr_con : constant -> module_path * dir_path * label
140	140	val eq_constant : constant -> constant -> bool
	141	val con_with_label : constant -> label -> constant
141	142
142	143	val string_of_con : constant -> string
143	144	val con_label : constant -> label

+7

-0

lib/envars.ml less more

12	12	if !Flags.boot \|\| Coq_config.local
13	13	then Filename.concat Coq_config.coqsrc "bin"
14	14	else System.canonical_path_name (Filename.dirname Sys.executable_name)
	15
	16	(* On win32, we add coqbin to the PATH at launch-time (this used to be
	17	done in a .bat script). *)
	18
	19	let _ =
	20	if Coq_config.arch = "win32" then
	21	Unix.putenv "PATH" (coqbin() ^ ";" ^ System.getenv_else "PATH" "")
15	22
16	23	let guess_coqlib () =
17	24	let file = "states/initial.coq" in

+12

-3

lib/system.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: system.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: system.ml 13750 2010-12-24 09:55:54Z letouzey $ *)
9	9
10	10	open Pp
11	11	open Util

18	18	Sys.getenv var
19	19	with Not_found ->
20	20	warning ("Environment variable "^var^" not found: using '"^def^"' .");
21		flush Pervasives.stdout;
	21	flush_all ();
22	22	def
23	23
24	24	let getenv_else s dft = try Sys.getenv s with Not_found -> dft
25	25
26		let home = (safe_getenv_def "HOME" ".")
	26	(* On win32, the home directory is probably not in $HOME, but in
	27	some other environment variable *)
	28
	29	let home =
	30	try Sys.getenv "HOME" with Not_found ->
	31	try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
	32	try Sys.getenv "USERPROFILE" with Not_found ->
	33	warning ("Cannot determine user home directory, using '.' .");
	34	flush_all ();
	35	"."
27	36
28	37	let safe_getenv n = safe_getenv_def n ("$"^n)
29	38

+30

-12

library/goptions.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: goptions.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: goptions.ml 13922 2011-03-21 16:25:18Z letouzey $ *)
9	9
10	10	(* This module manages customization parameters at the vernacular level *)
11	11

304	304
305	305	let bad_type_error () = error "Bad type of value for this option."
306	306
307		let set_int_option_value_gen locality = set_option_value locality
308		(fun v -> function
309		\| (IntValue _) -> IntValue v
310		\| _ -> bad_type_error ())
	307	let check_int_value v = function
	308	\| IntValue _ -> IntValue v
	309	\| _ -> bad_type_error ()
	310
	311	let check_bool_value v = function
	312	\| BoolValue _ -> BoolValue v
	313	\| _ -> bad_type_error ()
	314
	315	let check_string_value v = function
	316	\| StringValue _ -> StringValue v
	317	\| _ -> bad_type_error ()
	318
	319	let check_unset_value v = function
	320	\| BoolValue _ -> BoolValue false
	321	\| IntValue _ -> IntValue None
	322	\| _ -> bad_type_error ()
	323
	324	(* Nota: For compatibility reasons, some errors are treated as
	325	warning. This allows a script to refer to an option that doesn't
	326	exist anymore *)
	327
	328	let set_int_option_value_gen locality =
	329	set_option_value locality check_int_value
311	330	let set_bool_option_value_gen locality key v =
312		try set_option_value locality (fun v -> function
313		\| (BoolValue _) -> BoolValue v
314		\| _ -> bad_type_error ()) key v
	331	try set_option_value locality check_bool_value key v
315	332	with UserError (_,s) -> Flags.if_verbose msg_warning s
316		let set_string_option_value_gen locality = set_option_value locality
317		(fun v -> function
318		\| (StringValue _) -> StringValue v
319		\| _ -> bad_type_error ())
	333	let set_string_option_value_gen locality =
	334	set_option_value locality check_string_value
	335	let unset_option_value_gen locality key =
	336	try set_option_value locality check_unset_value key ()
	337	with UserError (_,s) -> Flags.if_verbose msg_warning s
320	338
321	339	let set_int_option_value = set_int_option_value_gen None
322	340	let set_bool_option_value = set_bool_option_value_gen None

+2

-1

library/goptions.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: goptions.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: goptions.mli 13922 2011-03-21 16:25:18Z letouzey $ i)
9	9
10	10	(* This module manages customization parameters at the vernacular level *)
11	11

156	156	val set_int_option_value_gen : bool option -> option_name -> int option -> unit
157	157	val set_bool_option_value_gen : bool option -> option_name -> bool -> unit
158	158	val set_string_option_value_gen : bool option -> option_name -> string -> unit
	159	val unset_option_value_gen : bool option -> option_name -> unit
159	160
160	161	val set_int_option_value : option_name -> int option -> unit
161	162	val set_bool_option_value : option_name -> bool -> unit

+22

-2

myocamlbuild.ml less more

63	63	let w32ocamlc = w32pref^"-ocamlc"
64	64	let w32ocamlopt = w32pref^"-ocamlopt"
65	65	let w32ocamlmklib = w32pref^"-ocamlmklib"
	66	let w32res = w32pref^"-windres"
66	67	let w32lib = "/usr/"^w32pref^"/lib/"
67	68	let w32bin = "/usr/"^w32pref^"/bin/"
	69	let w32ico = "ide/coq_icon.o"
68	70
69	71	let _ = if w32 then begin
70	72	Options.ocamlopt := A w32ocamlopt;

166	168	type links = Both \| Best \| BestInPlace \| Ide
167	169
168	170	let all_binaries =
	171	(if w32 then [ "mkwinapp", "tools/mkwinapp", Best ] else []) @
169	172	[ "coqtop", coqtop, Both;
170	173	"coqide", coqide, Ide;
171	174	"coqmktop", coqmktop, Both;

364	367	"let ide = \""^ide_mods^"\"\n"],
365	368	tolink));
366	369
	370	(** For windows, building coff object file from a .rc (for the icon) *)
	371
	372	if w32 then rule ".rc.o" ~deps:["%.rc";"ide/coq.ico"] ~prod:"%.o"
	373	(fun env _ ->
	374	let rc = env "%.rc" and o = env "%.o" in
	375	Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc;
	376	A "--output-format";A "coff";A "--output"; Px o]));
	377
367	378	(** Coqtop and coqide *)
368	379
369	380	let mktop_rule f is_ide =
370	381	let fo = f^".native" and fb = f^".byte" in
371	382	let ideflag = if is_ide then A"-ide" else N in
372	383	let depsall = [coqmktopbest;libcoqrun] in
	384	let depsall = if w32 then w32ico::depsall else depsall in
373	385	let depso = "coq_config.cmx" :: core_cmxa in
374	386	let depsb = "coq_config.cmo" :: core_cma in
375	387	let depideo = if is_ide then [ide_cmxa] else [] in
376	388	let depideb = if is_ide then [ide_cma] else [] in
377		let w32ideflag = (if is_ide then [A"-ccopt";A"\"-link -mwindows\""] else) [] in
378		let w32flag = if not w32 then N else S ([A"-camlbin";A w32bin]@w32ideflag) in
	389	let w32ideflag =
	390	(* Uncomment the following line to make coqide a console-free win32 app.
	391	For the moment we don't, some issue remain to be investigated.
	392	In the meantime, coqide can be made console-free a posteriori via
	393	the mkwinapp tool. *)
	394	(if is_ide then [A"-ccopt";A"\"-link -Wl,-subsystem,windows\""] else) [] in
	395	let w32flag =
	396	if not w32 then N
	397	else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]@w32ideflag)
	398	in
379	399	if opt then rule fo ~prod:fo ~deps:(depsall@depso@depideo) ~insert:`top
380	400	(cmd [P coqmktopbest;w32flag;A"-boot";A"-opt";ideflag;incl fo;A"-o";Px fo]);
381	401	rule fb ~prod:fb ~deps:(depsall@depsb@depideb) ~insert:`top

+8

-6

parsing/prettyp.ml less more

9	9	* on May-June 2006 for implementation of abstraction of pretty-printing of objects.
10	10	*)
11	11
12		(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
	12	(* $Id: prettyp.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
13	13
14	14	open Pp
15	15	open Util

459	459	with_line_skip (print_name_infos (ConstRef sp))
460	460
461	461	let gallina_print_syntactic_def kn =
462		let sep = " := "
463		and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
	462	let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
464	463	and (vars,a) = Syntax_def.search_syntactic_definition kn in
465	464	let c = Topconstr.rawconstr_of_aconstr dummy_loc a in
466		str "Notation " ++ pr_qualid qid ++
467		prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
468		Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
	465	hov 2
	466	(hov 4
	467	(str "Notation " ++ pr_qualid qid ++
	468	prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
	469	spc () ++ str ":=") ++
	470	spc () ++ Constrextern.without_symbols pr_rawconstr c) ++ fnl ()
469	471
470	472	let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
471	473	let sep = if with_values then " = " else " : "

+4

-3

parsing/tacextend.ml4 less more

7	7
8	8	(i camlp4use: "pa_extend.cmo q_MLast.cmo" i)
9	9
10		(* $Id: tacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
	10	(* $Id: tacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
11	11
12	12	open Util
13	13	open Genarg

54	54	let add_clause s (pt,e) l =
55	55	let p = make_patt pt in
56	56	let w = Some (make_when (MLast.loc_of_expr e) pt) in
57		(p, w, make_let e pt)::l
	57	(p, <:vala< w >>, make_let e pt)::l
58	58
59	59	let rec extract_signature = function
60	60	\| [] -> []

71	71	let make_clauses s l =
72	72	check_unicity s l;
73	73	let default =
74		(<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
	74	(<:patt< _ >>,<:vala<None>>,
	75	<:expr< failwith "Tactic extension: cannot occur" >>) in
75	76	List.fold_right (add_clause s) l [default]
76	77
77	78	let rec make_args = function

+4

-3

parsing/vernacextend.ml4 less more

7	7
8	8	(i camlp4use: "pa_extend.cmo q_MLast.cmo" i)
9	9
10		(* $Id: vernacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
	10	(* $Id: vernacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
11	11
12	12	open Util
13	13	open Genarg

30	30	let add_clause s (_,pt,e) l =
31	31	let p = make_patt pt in
32	32	let w = Some (make_when (MLast.loc_of_expr e) pt) in
33		(p, w, make_let e pt)::l
	33	(p, <:vala<w>>, make_let e pt)::l
34	34
35	35	let check_unicity s l =
36	36	let l' = List.map (fun (_,l,_) -> extract_signature l) l in

42	42	let make_clauses s l =
43	43	check_unicity s l;
44	44	let default =
45		(<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in
	45	(<:patt< _ >>,<:vala<None>>,
	46	<:expr< failwith "Vernac extension: cannot occur" >>) in
46	47	List.fold_right (add_clause s) l [default]
47	48
48	49	let mlexpr_of_clause =

+0

-1

plugins/dp/dp_why.ml less more

180	180	let output_file f q =
181	181	let c = open_out f in
182	182	let fmt = formatter_of_out_channel c in
183		fprintf fmt "include \"real.why\"@.";
184	183	fprintf fmt "@[%a@]@." print_query q;
185	184	close_out c

+47

-4

plugins/extraction/common.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: common.ml 13420 2010-09-16 15:47:08Z letouzey $ i)
	8	(i $Id: common.ml 14010 2011-04-15 16:05:07Z letouzey $ i)
9	9
10	10	open Pp
11	11	open Util

41	41	let pr_binding = function
42	42	\| [] -> mt ()
43	43	\| l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
	44
	45	(** By default, in module Format, you can do horizontal placing of blocks
	46	even if they include newlines, as long as the number of chars in the
	47	blocks are less that a line length. To avoid this awkward situation,
	48	we attach a big virtual size to [fnl] newlines. *)
	49
	50	let fnl () = stras (1000000,"") ++ fnl ()
44	51
45	52	let fnl2 () = fnl () ++ fnl ()
46	53

508	515	let pp_haskell_gen k mp rls = match rls with
509	516	\| [] -> assert false
510	517	\| s::rls' ->
511		(if base_mp mp <> top_visible_mp () then s ^ "." else "") ^
512		(if upperkind k then "" else "_") ^ pseudo_qualify rls'
	518	let str = pseudo_qualify rls' in
	519	let str = if is_upper str && not (upperkind k) then ("_"^str) else str in
	520	let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in
	521	prf ^ str
513	522
514	523	(* Main name printing function for a reference *)
515	524

541	550	add_visible (Mod,s) l; s
542	551	\| _ -> pp_ocaml_gen Mod mp (List.rev ls) None
543	552
544
	553	(** Special hack for constants of type Ascii.ascii : if an
	554	[Extract Inductive ascii => char] has been declared, then
	555	the constants are directly turned into chars *)
	556
	557	let mk_ind path s =
	558	make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
	559
	560	let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
	561
	562	let check_extract_ascii () =
	563	try
	564	let char_type = match lang () with
	565	\| Ocaml -> "char"
	566	\| Haskell -> "Char"
	567	\| _ -> raise Not_found
	568	in
	569	find_custom (IndRef (ind_ascii,0)) = char_type
	570	with Not_found -> false
	571
	572	let is_list_cons l =
	573	List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true \| _ -> false) l
	574
	575	let is_native_char = function
	576	\| MLcons(_,ConstructRef ((kn,0),1),l) ->
	577	kn = ind_ascii && check_extract_ascii () && is_list_cons l
	578	\| _ -> false
	579
	580	let pp_native_char c =
	581	let rec cumul = function
	582	\| [] -> 0
	583	\| MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
	584	\| _ -> assert false
	585	in
	586	let l = match c with MLcons(_,_,l) -> l \| _ -> assert false in
	587	str ("'"^Char.escaped (Char.chr (cumul l))^"'")

+18

-1

plugins/extraction/common.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: common.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: common.mli 14010 2011-04-15 16:05:07Z letouzey $ i)
9	9
10	10	open Names
11	11	open Libnames

13	13	open Mlutil
14	14	open Pp
15	15
	16	(** By default, in module Format, you can do horizontal placing of blocks
	17	even if they include newlines, as long as the number of chars in the
	18	blocks are less that a line length. To avoid this awkward situation,
	19	we attach a big virtual size to [fnl] newlines. *)
	20
	21	val fnl : unit -> std_ppcmds
16	22	val fnl2 : unit -> std_ppcmds
17	23	val space_if : bool -> std_ppcmds
18	24	val sec_space_if : bool -> std_ppcmds

56	62	val reset_renaming_tables : reset_kind -> unit
57	63
58	64	val set_keywords : Idset.t -> unit
	65
	66	(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
	67
	68	val mk_ind : string -> string -> mutual_inductive
	69
	70	(** Special hack for constants of type Ascii.ascii : if an
	71	[Extract Inductive ascii => char] has been declared, then
	72	the constants are directly turned into chars *)
	73
	74	val is_native_char : ml_ast -> bool
	75	val pp_native_char : ml_ast -> std_ppcmds

+32

-17

plugins/extraction/extract_env.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: extract_env.ml 13420 2010-09-16 15:47:08Z letouzey $ i)
	8	(i $Id: extract_env.ml 14012 2011-04-15 16:45:27Z letouzey $ i)
9	9
10	10	open Term
11	11	open Declarations

48	48	\| [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
49	49	\| [] -> []
50	50	\| d :: l ->
51		match (Global.lookup_module (MPfile d)).mod_expr with
52		\| Some meb ->
53		if dir_opt = Some d then [MPfile d, meb]
54		else (MPfile d, meb) :: (parse l)
55		\| _ -> assert false
	51	let mb = Global.lookup_module (MPfile d) in
	52	(* If -dont-load-proof has been used, mod_expr is None,
	53	we try with mod_type *)
	54	let meb = Option.default mb.mod_type mb.mod_expr in
	55	if dir_opt = Some d then [MPfile d, meb]
	56	else (MPfile d, meb) :: (parse l)
56	57	in parse (Library.loaded_libraries ())
57	58
58	59

326	327	\| SEBwith (_,_) -> anomaly "Not available yet"
327	328
328	329	and extract_module env mp all mb =
329		(* [mb.mod_expr <> None ], since we look at modules from outside. *)
330		(* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
331		{ ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr);
332		ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
	330	(* A module has an empty [mod_expr] when :
	331	- it is a module variable (for instance X inside a Module F [X:SIG])
	332	- it is a module assumption (Declare Module).
	333	Since we look at modules from outside, we shouldn't have variables.
	334	But a Declare Module at toplevel seems legal (cf #2525). For the
	335	moment we don't support this situation. *)
	336	match mb.mod_expr with
	337	\| None -> error_no_module_expr mp
	338	\| Some me ->
	339	{ ml_mod_expr = extract_seb env mp all me;
	340	ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
333	341
334	342
335	343	let unpack = function MEstruct (_,sel) -> sel \| _ -> assert false

396	404	(s Extraction of a ml struct to a file. )
397	405
398	406	let formatter dry file =
399		if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
400		else match file with
401		\| None -> !Pp_control.std_ft
402		\| Some cout ->
403		let ft = Pp_control.with_output_to cout in
404		Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ());
405		ft
	407	let ft =
	408	if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
	409	else Pp_control.with_output_to (Option.default stdout file)
	410	in
	411	(* We never want to see ellipsis ... in extracted code *)
	412	Format.pp_set_max_boxes ft max_int;
	413	(* We reuse the width information given via "Set Printing Width" *)
	414	(match Pp_control.get_margin () with
	415	\| None -> ()
	416	\| Some i ->
	417	Format.pp_set_margin ft i;
	418	Format.pp_set_max_indent ft (i-10));
	419	(* note: max_indent should be < margin above, otherwise it's ignored *)
	420	ft
406	421
407	422	let print_structure_to_file (fn,si,mo) dry struc =
408	423	let d = descr () in

+4

-4

plugins/extraction/extraction.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
	8	(i $Id: extraction.ml 13795 2011-01-22 14:43:06Z glondu $ i)
9	9
10	10	(i)
11	11	open Util

393	393	(* Third pass: we determine special cases. *)
394	394	let ind_info =
395	395	try
	396	let ip = (kn, 0) in
	397	let r = IndRef ip in
	398	if is_custom r then raise (I Standard);
396	399	if not mib.mind_finite then raise (I Coinductive);
397	400	if mib.mind_ntypes <> 1 then raise (I Standard);
398	401	let p = packets.(0) in

404	407	then raise (I Singleton);
405	408	if l = [] then raise (I Standard);
406	409	if not mib.mind_record then raise (I Standard);
407		let ip = (kn, 0) in
408		let r = IndRef ip in
409		if is_custom r then raise (I Standard);
410	410	(* Now we're sure it's a record. *)
411	411	(* First, we find its field names. *)
412	412	let rec names_prod t = match kind_of_term t with

+52

-41

plugins/extraction/haskell.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: haskell.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
	8	(i $Id: haskell.ml 14010 2011-04-15 16:05:07Z letouzey $ i)
9	9
10	10	(s Production of Haskell syntax. )
11	11

105	105
106	106	let expr_needs_par = function
107	107	\| MLlam _ -> true
108		\| MLcase _ -> true
	108	\| MLcase _ -> false (* now that we use the case ... of { ... } syntax *)
109	109	\| _ -> false
110	110
111	111

128	128	let pp_id = pr_id (List.hd i)
129	129	and pp_a1 = pp_expr false env [] a1
130	130	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
131		hv 0
132		(apply
133		(pp_par par'
134		(hv 0
135		(hov 5
136		(str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++
137		spc () ++ str "in") ++
138		spc () ++ hov 0 pp_a2)))
	131	let pp_def =
	132	str "let {" ++ cut () ++
	133	hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}")
	134	in
	135	apply
	136	(pp_par par'
	137	(hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
	138	spc () ++ hov 0 pp_a2)))
139	139	\| MLglob r ->
140	140	apply (pp_global Term r)
	141	\| MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
141	142	\| MLcons (_,r,[]) ->
142	143	assert (args=[]); pp_global Cons r
143	144	\| MLcons (_,r,[a]) ->

152	153	if ids <> [] then named_lams (List.rev ids) e
153	154	else dummy_lams (ast_lift 1 e) 1
154	155	in
155		hov 2 (str (find_custom_match pv) ++ fnl () ++
	156	apply
	157	(pp_par par'
	158	(hov 2
	159	(str (find_custom_match pv) ++ fnl () ++
156	160	prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
157		++ pp_expr true env [] t)
	161	++ pp_expr true env [] t)))
158	162	\| MLcase (info,t, pv) ->
159	163	apply (pp_par par'
160		(v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
161		fnl () ++ str " " ++ pp_pat env info pv)))
	164	(v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
	165	fnl () ++ pp_pat env info pv)))
162	166	\| MLfix (i,ids,defs) ->
163	167	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
164	168	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args

175	179	let pp_one_pat (name,ids,t) =
176	180	let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
177	181	let par = expr_needs_par t in
178		hov 2 (pp_global Cons name ++
	182	hov 2 (str " " ++ pp_global Cons name ++
179	183	(match ids with
180	184	\| [] -> mt ()
181	185	\| _ -> (str " " ++
182		prlist_with_sep
183		(fun () -> (spc ())) pr_id (List.rev ids))) ++
	186	prlist_with_sep spc pr_id (List.rev ids))) ++
184	187	str " ->" ++ spc () ++ pp_expr par env' [] t)
185	188	in
186	189	let factor_br, factor_set = try match info.m_same with

197	200	prvecti
198	201	(fun i x -> if Intset.mem i factor_set then mt () else
199	202	(pp_one_pat pv.(i) ++
200		if i = last && Intset.is_empty factor_set then mt () else
201		fnl () ++ str " ")) pv
	203	if i = last && Intset.is_empty factor_set then str "}" else
	204	(str ";" ++ fnl ()))) pv
202	205	++
203	206	if Intset.is_empty factor_set then mt () else
204	207	let par = expr_needs_par factor_br in
205	208	match info.m_same with
206	209	\| BranchFun _ ->
207	210	let ids, env' = push_vars [anonymous_name] env in
208		pr_id (List.hd ids) ++ str " ->" ++ spc () ++
209		pp_expr par env' [] factor_br
	211	hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
	212	pp_expr par env' [] factor_br ++ str "}")
210	213	\| BranchCst _ ->
211		str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
	214	hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}")
212	215	\| BranchNone -> mt ()
213	216
214	217	(*s names of the functions ([ids]) are already pushed in [env],

217	220	and pp_fix par env i (ids,bl) args =
218	221	pp_par par
219	222	(v 0
220		(v 2 (str "let" ++ fnl () ++
221		prvect_with_sep fnl
	223	(v 1 (str "let {" ++ fnl () ++
	224	prvect_with_sep (fun () -> str ";" ++ fnl ())
222	225	(fun (fi,ti) -> pp_function env (pr_id fi) ti)
223		(array_map2 (fun a b -> a,b) ids bl)) ++
224		fnl () ++
225		hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
	226	(array_map2 (fun a b -> a,b) ids bl) ++
	227	str "}") ++
	228	fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args))
226	229
227	230	and pp_function env f t =
228	231	let bl,t' = collect_lams t in

261	264	(fun () -> (str " ")) (pp_type true pl) l))
262	265	in
263	266	str (if Array.length cv = 0 then "type " else "data ") ++
264		pp_global Type (IndRef ip) ++ str " " ++
265		prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
266		(if pl = [] then mt () else str " ") ++
267		if Array.length cv = 0 then str "= () -- empty inductive"
	267	pp_global Type (IndRef ip) ++
	268	prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++
	269	if Array.length cv = 0 then str " () -- empty inductive"
268	270	else
269		(v 0 (str "= " ++
	271	(fnl () ++ str " " ++
	272	v 0 (str " " ++
270	273	prvect_with_sep (fun () -> fnl () ++ str "\| ") pp_constructor
271	274	(Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
272	275

308	311	in
309	312	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
310	313	\| Dfix (rv, defs, typs) ->
311		let max = Array.length rv in
312		let rec iter i =
313		if i = max then mt ()
314		else
315		let e = pp_global Term rv.(i) in
316		e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl ()
317		++ pp_function (empty_env ()) e defs.(i) ++ fnl2 ()
318		++ iter (i+1)
319		in iter 0
	314	let names = Array.map
	315	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
	316	in
	317	prvecti
	318	(fun i r ->
	319	let void = is_inline_custom r \|\|
	320	(not (is_custom r) && defs.(i) = MLexn "UNUSED")
	321	in
	322	if void then mt ()
	323	else
	324	names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++
	325	(if is_custom r then
	326	(names.(i) ++ str " = " ++ str (find_custom r))
	327	else
	328	(pp_function (empty_env ()) names.(i) defs.(i)))
	329	++ fnl2 ())
	330	rv
320	331	\| Dterm (r, a, t) ->
321	332	if is_inline_custom r then mt ()
322	333	else

+25

-13

plugins/extraction/mlutil.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: mlutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
	8	(i $Id: mlutil.ml 14003 2011-04-14 23:09:41Z letouzey $ i)
9	9
10	10	(i)
11	11	open Pp

109	109
110	110	let rec mgu = function
111	111	\| Tmeta m, Tmeta m' when m.id = m'.id -> ()
112		\| Tmeta m, t when m.contents=None ->
113		if type_occurs m.id t then raise Impossible
114		else m.contents <- Some t
115		\| t, Tmeta m when m.contents=None ->
116		if type_occurs m.id t then raise Impossible
117		else m.contents <- Some t
118		\| Tmeta {contents=Some u}, t -> mgu (u, t)
119		\| t, Tmeta {contents=Some u} -> mgu (t, u)
	112	\| Tmeta m, t \| t, Tmeta m ->
	113	(match m.contents with
	114	\| Some u -> mgu (u, t)
	115	\| None when type_occurs m.id t -> raise Impossible
	116	\| None -> m.contents <- Some t)
120	117	\| Tarr(a, b), Tarr(a', b') ->
121	118	mgu (a, a'); mgu (b, b')
122	119	\| Tglob (r,l), Tglob (r',l') when r = r' ->
123	120	List.iter mgu (List.combine l l')
124		\| Tvar i, Tvar j when i = j -> ()
125		\| Tvar' i, Tvar' j when i = j -> ()
126	121	\| Tdummy _, Tdummy _ -> ()
127		\| Tunknown, Tunknown -> ()
	122	\| t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
128	123	\| _ -> raise Impossible
129	124
130	125	let needs_magic p = try mgu p; false with Impossible -> true

827	822
828	823	let is_imm_apply = function MLapp (MLrel 1, _) -> true \| _ -> false
829	824
	825	(** Program creates a let-in named "program_branch_NN" for each branch of match.
	826	Unfolding them leads to more natural code (and more dummy removal) *)
	827
	828	let is_program_branch = function
	829	\| Id id ->
	830	let s = string_of_id id in
	831	let br = "program_branch_" in
	832	let n = String.length br in
	833	(try
	834	ignore (int_of_string (String.sub s n (String.length s - n)));
	835	String.sub s 0 n = br
	836	with _ -> false)
	837	\| Tmp _ \| Dummy -> false
	838
	839	let expand_linear_let o id e =
	840	o.opt_lin_let \|\| is_tmp id \|\| is_program_branch id \|\| is_imm_apply e
	841
830	842	(S The main simplification function. )
831	843
832	844	(* Some beta-iota reductions + simplifications. *)

843	855	if
844	856	(is_atomic c) \|\| (is_atomic e) \|\|
845	857	(let n = nb_occur_match e in
846		(n = 0 \|\| (n=1 && (is_tmp id \|\| is_imm_apply e \|\| o.opt_lin_let))))
	858	(n = 0 \|\| (n=1 && expand_linear_let o id e)))
847	859	then
848	860	simpl o (ast_subst c e)
849	861	else

+20

-13

plugins/extraction/modutil.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: modutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
	8	(i $Id: modutil.ml 14006 2011-04-14 23:09:56Z letouzey $ i)
9	9
10	10	open Names
11	11	open Declarations

288	288	(fun r -> Refset'.mem (base_r r) !needed))
289	289
290	290	let declared_refs = function
291		\| Dind (kn,_) -> [\|IndRef (mind_of_kn kn,0)\|]
292		\| Dtype (r,_,_) -> [\|r\|]
293		\| Dterm (r,_,_) -> [\|r\|]
294		\| Dfix (rv,_,_) -> rv
	291	\| Dind (kn,_) -> [IndRef (mind_of_kn kn,0)]
	292	\| Dtype (r,_,_) -> [r]
	293	\| Dterm (r,_,_) -> [r]
	294	\| Dfix (rv,_,_) -> Array.to_list rv
295	295
296	296	(* Computes the dependencies of a declaration, except in case
297	297	of custom extraction. *)

307	307	if not (is_custom r) then
308	308	ast_iter_references add_needed add_needed add_needed u
309	309	\| Dfix _ as d ->
310		(* Todo Later : avoid dependencies when Extract Constant *)
311	310	decl_iter_references add_needed add_needed add_needed d
312	311
313	312	let rec depcheck_se = function
314	313	\| [] -> []
315		\| ((l,SEdecl d) as t)::se ->
316		let se' = depcheck_se se in
317		let rv = declared_refs d in
318		if not (array_exists is_needed rv) then
319		(Array.iter remove_info_axiom rv; se')
320		else
321		(Array.iter found_needed rv; compute_deps_decl d; t::se')
	314	\| ((l,SEdecl d) as t) :: se ->
	315	let se' = depcheck_se se in
	316	let refs = declared_refs d in
	317	let refs' = List.filter is_needed refs in
	318	if refs' = [] then
	319	(List.iter remove_info_axiom refs; se')
	320	else begin
	321	List.iter found_needed refs';
	322	(* Hack to avoid extracting unused part of a Dfix *)
	323	match d with
	324	\| Dfix (rv,trms,tys) when (List.for_all is_custom refs') ->
	325	let trms' = Array.create (Array.length rv) (MLexn "UNUSED") in
	326	((l,SEdecl (Dfix (rv,trms',tys))) :: se')
	327	\| _ -> (compute_deps_decl d; t::se')
	328	end
322	329	\| _ -> raise NoDepCheck
323	330
324	331	let rec depcheck_struct = function

+33

-49

plugins/extraction/ocaml.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: ocaml.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
	8	(i $Id: ocaml.ml 14010 2011-04-15 16:05:07Z letouzey $ i)
9	9
10	10	(s Production of Ocaml syntax. )
11	11

118	118
119	119	(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
120	120	are needed or not. *)
121
122		let mk_ind path s =
123		make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
124	121
125	122	let rec pp_type par vl t =
126	123	let rec pp_rec par = function

158	155	\| MLcase (_,_,[\|_\|]) -> false
159	156	\| MLcase (_,_,pv) -> not (is_ifthenelse pv)
160	157	\| _ -> false
161
162
163		(** Special hack for constants of type Ascii.ascii : if an
164		[Extract Inductive ascii => char] has been declared, then
165		the constants are directly turned into chars *)
166
167		let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
168
169		let check_extract_ascii () =
170		try find_custom (IndRef (ind_ascii,0)) = "char" with Not_found -> false
171
172		let is_list_cons l =
173		List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true \| _ -> false) l
174
175		let pp_char l =
176		let rec cumul = function
177		\| [] -> 0
178		\| MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
179		\| _ -> assert false
180		in str ("'"^Char.escaped (Char.chr (cumul l))^"'")
181	158
182	159	let rec pp_expr par env args =
183	160	let par' = args <> [] \|\| par

213	190	let record = List.hd args in
214	191	pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
215	192	with _ -> apply (pp_global Term r))
216		\| MLcons(_,ConstructRef ((kn,0),1),l)
217		when kn = ind_ascii && check_extract_ascii () & is_list_cons l ->
218		assert (args=[]);
219		pp_char l
	193	\| MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
220	194	\| MLcons ({c_kind = Coinductive},r,[]) ->
221	195	assert (args=[]);
222	196	pp_par par (str "lazy " ++ pp_global Cons r)

246	220	if ids <> [] then named_lams (List.rev ids) e
247	221	else dummy_lams (ast_lift 1 e) 1
248	222	in
249		hov 2 (str (find_custom_match pv) ++ fnl () ++
	223	apply
	224	(pp_par par'
	225	(hov 2
	226	(str (find_custom_match pv) ++ fnl () ++
250	227	prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
251		++ pp_expr true env [] t)
	228	++ pp_expr true env [] t)))
252	229	\| MLcase (info, t, pv) ->
253	230	let expr = if info.m_kind = Coinductive then
254	231	(str "Lazy.force" ++ spc () ++ pp_expr true env [] t)

290	267	(try pp_ifthenelse par' env expr pv
291	268	with Not_found ->
292	269	v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
293		str " \| " ++ pp_pat env info pv))))
	270	pp_pat env info pv))))
294	271	\| MLfix (i,ids,defs) ->
295	272	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
296	273	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args

354	331	prvecti
355	332	(fun i x -> if Intset.mem i factor_set then mt () else
356	333	let s1,s2 = pp_one_pat env info x in
357		hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
358		if i = last && Intset.is_empty factor_set then mt () else
359		fnl () ++ str " \| ") pv
	334	hv 2 (hov 4 (str "\| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
	335	if i = last && Intset.is_empty factor_set then mt () else fnl ())
	336	pv
360	337	++
361	338	if Intset.is_empty factor_set then mt () else
362	339	let par = expr_needs_par factor_br in
363	340	match info.m_same with
364	341	\| BranchFun _ ->
365	342	let ids, env' = push_vars [anonymous_name] env in
366		hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
367		pp_expr par env' [] factor_br)
	343	hv 2 (str "\| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
	344	hov 2 (pp_expr par env' [] factor_br))
368	345	\| BranchCst _ ->
369		hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
	346	hv 2 (str "\| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br))
370	347	\| BranchNone -> mt ()
371	348
372	349	and pp_function env t =

378	355	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
379	356	pr_binding (List.rev (List.tl bl)) ++
380	357	str " = function" ++ fnl () ++
381		v 0 (str " \| " ++ pp_pat env' i pv)
	358	v 0 (pp_pat env' i pv)
382	359	else
383	360	pr_binding (List.rev bl) ++
384	361	str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
385		v 0 (str " \| " ++ pp_pat env' i pv)
	362	v 0 (pp_pat env' i pv)
386	363	\| _ ->
387	364	pr_binding (List.rev bl) ++
388	365	str " =" ++ fnl () ++ str " " ++

411	388	let names = Array.map
412	389	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
413	390	in
414		let rec pp sep letand i =
415		if i >= Array.length rv then mt ()
416		else if is_inline_custom rv.(i) then pp sep letand (i+1)
	391	let rec pp init i =
	392	if i >= Array.length rv then
	393	(if init then failwith "empty phrase" else mt ())
417	394	else
418		let def =
419		if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
420		else pp_function (empty_env ()) c.(i)
	395	let void = is_inline_custom rv.(i) \|\|
	396	(not (is_custom rv.(i)) && c.(i) = MLexn "UNUSED")
421	397	in
422		sep () ++ pp_val names.(i) t.(i) ++
423		str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1)
424		in pp mt "let rec " 0
	398	if void then pp init (i+1)
	399	else
	400	let def =
	401	if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
	402	else pp_function (empty_env ()) c.(i)
	403	in
	404	(if init then mt () else fnl2 ()) ++
	405	pp_val names.(i) t.(i) ++
	406	str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
	407	pp false (i+1)
	408	in pp true 0
425	409
426	410	(s Pretty-printing of inductive types declaration. )
427	411

438	422	let pl = rename_tvars keywords pl in
439	423	let pp_constructor i typs =
440	424	(if i=0 then mt () else fnl ()) ++
441		hov 5 (str " \| " ++ cnames.(i) ++
	425	hov 3 (str "\| " ++ cnames.(i) ++
442	426	(if typs = [] then mt () else str " of ") ++
443	427	prlist_with_sep
444	428	(fun () -> spc () ++ str "* ") (pp_type true pl) typs)

+26

-18

plugins/extraction/scheme.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: scheme.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
	8	(i $Id: scheme.ml 14006 2011-04-14 23:09:56Z letouzey $ i)
9	9
10	10	(s Production of Scheme syntax. )
11	11

100	100	if ids <> [] then named_lams (List.rev ids) e
101	101	else dummy_lams (ast_lift 1 e) 1
102	102	in
103		hov 2 (str (find_custom_match pv) ++ fnl () ++
	103	apply
	104	(paren
	105	(hov 2
	106	(str (find_custom_match pv) ++ fnl () ++
104	107	prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
105		++ pp_expr env [] t)
	108	++ pp_expr env [] t)))
106	109	\| MLcase (info,t, pv) ->
107	110	let e =
108	111	if info.m_kind <> Coinductive then pp_expr env [] t

162	165	\| Dind _ -> mt ()
163	166	\| Dtype _ -> mt ()
164	167	\| Dfix (rv, defs,_) ->
165		let ppv = Array.map (pp_global Term) rv in
166		prvect_with_sep fnl
167		(fun (pi,ti) ->
168		hov 2
169		(paren (str "define " ++ pi ++ spc () ++
170		(pp_expr (empty_env ()) [] ti))
171		++ fnl ()))
172		(array_map2 (fun p b -> (p,b)) ppv defs) ++
173		fnl ()
	168	let names = Array.map
	169	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
	170	in
	171	prvecti
	172	(fun i r ->
	173	let void = is_inline_custom r \|\|
	174	(not (is_custom r) && defs.(i) = MLexn "UNUSED")
	175	in
	176	if void then mt ()
	177	else
	178	hov 2
	179	(paren (str "define " ++ names.(i) ++ spc () ++
	180	(if is_custom r then str (find_custom r)
	181	else pp_expr (empty_env ()) [] defs.(i)))
	182	++ fnl ()) ++ fnl ())
	183	rv
174	184	\| Dterm (r, a, _) ->
175	185	if is_inline_custom r then mt ()
176	186	else
177		if is_custom r then
178		hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
179		str (find_custom r))) ++ fnl () ++ fnl ()
180		else
181		hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
182		pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
	187	hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
	188	(if is_custom r then str (find_custom r)
	189	else pp_expr (empty_env ()) [] a)))
	190	++ fnl2 ()
183	191
184	192	let rec pp_structure_elem = function
185	193	\| (l,SEdecl d) -> pp_decl d

+7

-1

plugins/extraction/table.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: table.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
	8	(i $Id: table.ml 14012 2011-04-15 16:45:27Z letouzey $ i)
9	9
10	10	open Names
11	11	open Term

309	309	pr_long_mp mp2 ++ str " have the same ML name.\n" ++
310	310	str "This is not supported yet. Please do some renaming first.")
311	311
	312	let error_no_module_expr mp =
	313	err (str "The module " ++ pr_long_mp mp
	314	++ str " has no body, it probably comes from\n"
	315	++ str "some Declare Module outside any Module Type.\n"
	316	++ str "This situation is currently unsupported by the extraction.")
	317
312	318	let error_unknown_module m =
313	319	err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
314	320

+2

-1

plugins/extraction/table.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: table.mli 13420 2010-09-16 15:47:08Z letouzey $ i)
	8	(i $Id: table.mli 14012 2011-04-15 16:45:27Z letouzey $ i)
9	9
10	10	open Names
11	11	open Libnames

28	28	val error_inductive : global_reference -> 'a
29	29	val error_nb_cons : unit -> 'a
30	30	val error_module_clash : module_path -> module_path -> 'a
	31	val error_no_module_expr : module_path -> 'a
31	32	val error_unknown_module : qualid -> 'a
32	33	val error_scheme : unit -> 'a
33	34	val error_not_visible : global_reference -> 'a

+2

-2

plugins/subtac/subtac_cases.ml less more

6	6	(* * GNU Lesser General Public License Version 2.1 *)
7	7	(************************************************************************)
8	8
9		(* $Id: subtac_cases.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
	9	(* $Id: subtac_cases.ml 14003 2011-04-14 23:09:41Z letouzey $ *)
10	10
11	11	open Cases
12	12	open Util

1740	1740	let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
1741	1741	let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
1742	1742	and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
1743		let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
	1743	let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
1744	1744	let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
1745	1745	let branch =
1746	1746	let bref = RVar (dummy_loc, branch_name) in

+2

-2

pretyping/cases.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *)
	8	(* $Id: cases.ml 13962 2011-04-06 17:00:45Z herbelin $ *)
9	9
10	10	open Util
11	11	open Names

1202	1202	let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
1203	1203	let inst = List.map mkRel deps in
1204	1204	{ uj_val = applist (case, inst);
1205		uj_type = substl inst typ }
	1205	uj_type = prod_applist typ inst }
1206	1206
1207	1207	and compile_branch current names deps pb arsign eqn cstr =
1208	1208	let sign, pb = build_branch current deps names pb arsign eqn cstr in

+2

-2

pretyping/clenv.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: clenv.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
	8	(* $Id: clenv.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
9	9
10	10	open Pp
11	11	open Util

304	304
305	305	let connect_clenv gls clenv =
306	306	{ clenv with
307		evd = evars_reset_evd gls.sigma clenv.evd;
	307	evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd;
308	308	env = Global.env_of_context gls.it.evar_hyps }
309	309
310	310	(* [clenv_fchain mv clenv clenv']

+4

-2

pretyping/evd.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: evd.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
	8	(* $Id: evd.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
9	9
10	10	open Pp
11	11	open Util

506	506	metas=Metamap.empty
507	507	}
508	508
509		let evars_reset_evd evd d = {d with evars = evd.evars}
	509	let evars_reset_evd ?(with_conv_pbs=false) evd d =
	510	{d with evars = evd.evars;
	511	conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs}
510	512	let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
511	513	let evar_source evk d = (EvarMap.find d.evars evk).evar_source
512	514

+2

-2

pretyping/evd.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: evd.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i)
9	9
10	10	(i)
11	11	open Util

176	176	val subst_evar_defs_light : substitution -> evar_map -> evar_map
177	177
178	178	(* spiwack: this function seems to somewhat break the abstraction. *)
179		val evars_reset_evd : evar_map -> evar_map -> evar_map
	179	val evars_reset_evd : ?with_conv_pbs:bool -> evar_map -> evar_map -> evar_map
180	180
181	181
182	182	(* spiwack: [is_undefined_evar] should be considered a candidate

+5

-2

pretyping/pretyping.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *)
	8	(* $Id: pretyping.ml 13780 2011-01-07 16:37:57Z herbelin $ *)
9	9
10	10	open Pp
11	11	open Util

633	633	let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
634	634	let cj = match k with
635	635	\| VMcast when not (occur_existential cty \|\| occur_existential tval) ->
636		ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
	636	(try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
	637	with Reduction.NotConvertible ->
	638	error_actual_type_loc loc env !evdref cj tval)
	639
637	640	\| _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
638	641	in
639	642	let v = mkCast (cj.uj_val, k, tval) in

+4

-5

pretyping/tacred.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: tacred.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
9	9
10	10	open Pp
11	11	open Util

215	215	\| EvalRel _ \| EvalEvar _ -> None
216	216	\| EvalVar id' -> Some (EvalVar id)
217	217	\| EvalConst kn ->
218		let (mp,dp,_) = repr_con kn in
219		Some (EvalConst (make_con mp dp (label_of_id id))) in
	218	Some (EvalConst (con_with_label kn (label_of_id id))) in
220	219	match refi with
221	220	\| None -> None
222	221	\| Some ref ->

480	479	\| CoFix (bodynum,(names,_,_) as cofix) ->
481	480	let build_cofix_name =
482	481	if isConst func then
483		let (mp,dp,_) = repr_con (destConst func) in
484	482	let minargs = List.length mia.mcargs in
485	483	fun i ->
486	484	if i = bodynum then Some (minargs,func)

491	489	mutual inductive, try to reuse the global name if
492	490	the block was indeed initially built as a global
493	491	definition *)
494		let kn = make_con mp dp (label_of_id id) in
	492	let kn = con_with_label (destConst func) (label_of_id id)
	493	in
495	494	try match constant_opt_value env kn with
496	495	\| None -> None
497	496	(* TODO: check kn is correct *)

+4

-4

proofs/pfedit.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: pfedit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: pfedit.ml 13981 2011-04-08 16:59:26Z herbelin $ *)
9	9
10	10	open Pp
11	11	open Util

343	343
344	344	let next = let n = ref 0 in fun () -> incr n; !n
345	345
346		let build_constant_by_tactic sign typ tac =
347		let id = id_of_string ("temporary_proof"^string_of_int (next())) in
	346	let build_constant_by_tactic id sign typ tac =
348	347	start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
349	348	try
350	349	by tac;

356	355	raise e
357	356
358	357	let build_by_tactic typ tac =
	358	let id = id_of_string ("temporary_proof"^string_of_int (next())) in
359	359	let sign = Decls.clear_proofs (Global.named_context ()) in
360		(build_constant_by_tactic sign typ tac).const_entry_body
	360	(build_constant_by_tactic id sign typ tac).const_entry_body

+2

-2

proofs/pfedit.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: pfedit.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: pfedit.mli 13981 2011-04-08 16:59:26Z herbelin $ i)
9	9
10	10	(i)
11	11	open Util

201	201
202	202	(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
203	203
204		val build_constant_by_tactic : named_context_val -> types -> tactic ->
	204	val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
205	205	Entries.definition_entry
206	206	val build_by_tactic : types -> tactic -> constr

+7

-3

scripts/coqc.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: coqc.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: coqc.ml 14015 2011-04-15 17:48:45Z letouzey $ *)
9	9
10	10	(* Afin de rendre Coq plus portable, ce programme Caml remplace le script
11	11	coqc.

83	83	Unix.create_process_env command (Array.of_list args') environment
84	84	Unix.stdin Unix.stdout Unix.stderr
85	85	in
86		ignore (Unix.waitpid [] pid)
	86	let status = snd (Unix.waitpid [] pid) in
	87	let errcode =
	88	match status with Unix.WEXITED c\|Unix.WSTOPPED c\|Unix.WSIGNALED c -> c
	89	in
	90	exit errcode
87	91	\| _ ->
88	92	Unix.execvpe command (Array.of_list args') environment
89	93

195	199	(* List.iter (compile coqtopname args) cfiles*)
196	200	Unix.handle_unix_error (compile coqtopname args) cfiles
197	201
198		let _ = Printexc.print main (); exit 0
	202	let _ = Printexc.print main ()

+2

-2

tactics/class_tactics.ml4 less more

7	7
8	8	(i camlp4deps: "parsing/grammar.cma" i)
9	9
10		(* $Id: class_tactics.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
	10	(* $Id: class_tactics.ml4 13902 2011-03-10 15:50:24Z msozeau $ *)
11	11
12	12	open Pp
13	13	open Util

84	84	if goals = [] then None
85	85	else
86	86	let goals = List.rev goals in
87		let evm' = evars_reset_evd evm' evm in
	87	let evm' = evars_reset_evd ~with_conv_pbs:false evm' evm in
88	88	Some (goals, evm')
89	89
90	90	(** Typeclasses instance search tactic / eauto *)

+3

-3

tactics/equality.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *)
	8	(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *)
9	9
10	10	open Pp
11	11	open Util

887	887	with
888	888	\| Some w ->
889	889	let w_type = type_of env sigma w in
890		if Evarconv.e_conv env evdref w_type a then
891		applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
	890	if Evarconv.e_cumul env evdref w_type a then
	891	applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail])
892	892	else
893	893	error "Cannot solve a unification problem."
894	894	\| None -> anomaly "Not enough components to build the dependent tuple"

+2

-2

tactics/tactics.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *)
	8	(* $Id: tactics.ml 13981 2011-04-08 16:59:26Z herbelin $ *)
9	9
10	10	open Pp
11	11	open Util

3468	3468	try flush_and_check_evars (project gl) concl
3469	3469	with Uninstantiated_evar _ ->
3470	3470	error "\"abstract\" cannot handle existentials." in
3471		let const = Pfedit.build_constant_by_tactic secsign concl
	3471	let const = Pfedit.build_constant_by_tactic id secsign concl
3472	3472	(tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
3473	3473	let cd = Entries.DefinitionEntry const in
3474	3474	let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in

+19

-19

test-suite/output/Extraction_matchs_2413.out less more

8	8	( val wrong_id : 'a1 hole -> 'a2 hole )
9	9
10	10	let wrong_id = function
11		\| Hole -> Hole
12		\| Hole2 -> Hole2
	11	\| Hole -> Hole
	12	\| Hole2 -> Hole2
13	13	( val test3 : 'a1 option -> 'a1 option )
14	14
15	15	let test3 o =

17	17	( val test4 : indu -> indu )
18	18
19	19	let test4 = function
20		\| A m -> A (S m)
21		\| x -> x
	20	\| A m -> A (S m)
	21	\| x -> x
22	22	( val test5 : indu -> indu )
23	23
24	24	let test5 = function
25		\| A m -> A (S m)
26		\| _ -> B
	25	\| A m -> A (S m)
	26	\| _ -> B
27	27	( val test6 : indu' -> indu' )
28	28
29	29	let test6 = function
30		\| A' m -> A' (S m)
31		\| E' -> B'
32		\| F' -> B'
33		\| _ -> C'
	30	\| A' m -> A' (S m)
	31	\| E' -> B'
	32	\| F' -> B'
	33	\| _ -> C'
34	34	( val test7 : indu -> nat option )
35	35
36	36	let test7 = function
37		\| A m -> Some m
38		\| _ -> None
	37	\| A m -> Some m
	38	\| _ -> None
39	39	(** val decode_cond_mode :
40	40	(word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1
41	41	-> opcode -> 'a2) -> 'a2 decoder_result **)
42	42
43	43	let decode_cond_mode condition f w g =
44	44	match condition w with
45		\| Some oc ->
46		(match f w with
47		\| DecUndefined -> DecUndefined
48		\| DecUnpredictable -> DecUnpredictable
49		\| DecInst i -> DecInst (g i oc)
50		\| DecError m -> DecError m)
51		\| None -> DecUndefined
	45	\| Some oc ->
	46	(match f w with
	47	\| DecUndefined -> DecUndefined
	48	\| DecUnpredictable -> DecUnpredictable
	49	\| DecInst i -> DecInst (g i oc)
	50	\| DecError m -> DecError m)
	51	\| None -> DecUndefined

+5

-5

theories/FSets/FMapAVL.v less more

7	7
8	8	(* Finite map library. *)
9	9
10		(* $Id: FMapAVL.v 13427 2010-09-17 17:37:52Z letouzey $ *)
	10	(* $Id: FMapAVL.v 13768 2011-01-06 13:55:35Z glondu $ *)
11	11
12	12	(** * FMapAVL *)
13	13

77	77
78	78	Definition is_empty m := match m with Leaf => true \| _ => false end.
79	79
80		(** * Appartness *)
81
82		(** The [mem] function is deciding appartness. It exploits the [bst] property
	80	(** * Membership *)
	81
	82	(** The [mem] function is deciding membership. It exploits the [bst] property
83	83	to achieve logarithmic complexity. *)
84	84
85	85	Fixpoint mem x m : bool :=

704	704	destruct m; simpl; intros; try discriminate; red; intuition_in.
705	705	Qed.
706	706
707		(** * Appartness *)
	707	(** * Membership *)
708	708
709	709	Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.
710	710	Proof.

+4

-4

theories/MSets/MSetAVL.v less more

81	81	Definition is_empty s :=
82	82	match s with Leaf => true \| _ => false end.
83	83
84		( Appartness *)
85
86		(** The [mem] function is deciding appartness. It exploits the
	84	( Membership *)
	85
	86	(** The [mem] function is deciding membership. It exploits the
87	87	binary search tree invariant to achieve logarithmic complexity. *)
88	88
89	89	Fixpoint mem x s :=

791	791	split; auto. try discriminate. intro H; elim (H x); auto.
792	792	Qed.
793	793
794		(** * Appartness *)
	794	(** * Membership *)
795	795
796	796	Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.
797	797	Proof.

+5

-4

tools/coqdep.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: coqdep.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: coqdep.ml 13983 2011-04-08 17:57:56Z herbelin $ *)
9	9
10	10	open Printf
11	11	open Coqdep_lexer

40	40	match get_extension f [".vo"] with
41	41	\| (basename,".vo") ->
42	42	let name = log_dir@[basename] in
43		Hashtbl.add coqlibKnown [basename] ();
44		Hashtbl.add coqlibKnown name ()
	43	let paths = suffixes name in
	44	List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
45	45	\| _ -> ()
46	46
47	47	let sort () =

198	198	let coqlib = Envars.coqlib () in
199	199	add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
200	200	add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
201		add_dir add_coqlib_known (coqlib//"user-contrib") []
	201	let user = coqlib//"user-contrib" in
	202	if Sys.file_exists user then add_rec_dir add_coqlib_known user []
202	203	end;
203	204	List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
204	205	List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;

+1

-2

tools/coqdep_common.ml less more

396	396	\| S_DIR when recur ->
397	397	if List.mem phys_f !norecdir_list then ()
398	398	else
399		let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in
400		add_directory recur add_file phys_f log_dir'
	399	add_directory recur add_file phys_f (log_dir@[f])
401	400	\| S_REG -> add_file phys_dir log_dir f
402	401	\| _ -> ()
403	402	done

+92

-0

tools/mkwinapp.ml less more

	0	(* OCaml-Win32
	1	* mkwinapp.ml
	2	* Copyright (c) 2002-2004 by Harry Chomsky
	3	*
	4	* This library is free software; you can redistribute it and/or
	5	* modify it under the terms of the GNU Library General Public
	6	* License as published by the Free Software Foundation; either
	7	* version 2 of the License, or (at your option) any later version.
	8	*
	9	* This library is distributed in the hope that it will be useful,
	10	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	11	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
	12	* Library General Public License for more details.
	13	*
	14	* You should have received a copy of the GNU Library General Public
	15	* License along with this library; if not, write to the Free
	16	* Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
	17	*)
	18
	19	(*********************************************************************
	20	* This program alters an .exe file to make it use the "windows subsystem"
	21	* instead of the "console subsystem". In other words, when Windows runs
	22	* the program, it will not create a console for it.
	23	*)
	24
	25	(* Pierre Letouzey 23/12/2010 : modification to allow selecting the
	26	subsystem to use instead of just setting the windows subsystem *)
	27
	28	(* This tool can be run directly via :
	29	ocaml unix.cma mkwinapp.ml [-set\|-unset] <filename>
	30	*)
	31
	32	exception Invalid_file_format
	33
	34	let input_word ic =
	35	let lo = input_byte ic in
	36	let hi = input_byte ic in
	37	(hi lsl 8) + lo
	38
	39	let find_pe_header ic =
	40	seek_in ic 0x3C;
	41	let peheader = input_word ic in
	42	seek_in ic peheader;
	43	if input_char ic <> 'P' then
	44	raise Invalid_file_format;
	45	if input_char ic <> 'E' then
	46	raise Invalid_file_format;
	47	peheader
	48
	49	let find_optional_header ic =
	50	let peheader = find_pe_header ic in
	51	let coffheader = peheader + 4 in
	52	seek_in ic (coffheader + 16);
	53	let optsize = input_word ic in
	54	if optsize < 96 then
	55	raise Invalid_file_format;
	56	let optheader = coffheader + 20 in
	57	seek_in ic optheader;
	58	let magic = input_word ic in
	59	if magic <> 0x010B && magic <> 0x020B then
	60	raise Invalid_file_format;
	61	optheader
	62
	63	let change flag ic oc =
	64	let optheader = find_optional_header ic in
	65	seek_out oc (optheader + 64);
	66	for i = 1 to 4 do
	67	output_byte oc 0
	68	done;
	69	output_byte oc (if flag then 2 else 3)
	70
	71	let usage () =
	72	print_endline "Alters a Win32 executable file to use the Windows subsystem or not.";
	73	print_endline "Usage: mkwinapp [-set\|-unset] <filename>";
	74	print_endline "Giving no option is equivalent to -set";
	75	exit 1
	76
	77	let main () =
	78	let n = Array.length Sys.argv - 1 in
	79	if not (n = 1 \|\| n = 2) then usage ();
	80	let flag =
	81	if n = 1 then true
	82	else if Sys.argv.(1) = "-set" then true
	83	else if Sys.argv.(1) = "-unset" then false
	84	else usage ()
	85	in
	86	let filename = Sys.argv.(n) in
	87	let f = Unix.openfile filename [Unix.O_RDWR] 0 in
	88	let ic = Unix.in_channel_of_descr f and oc = Unix.out_channel_of_descr f in
	89	change flag ic oc
	90
	91	let _ = main ()

+3

-2

toplevel/search.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: search.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: search.ml 13853 2011-02-24 07:57:31Z glondu $ *)
9	9
10	10	open Pp
11	11	open Util

196	196	\| l, outside -> filter_by_module l (not outside)
197	197
198	198	let filter_subproof gr _ _ =
199		not (string_string_contains (name_of_reference gr) "_subproof")
	199	not (string_string_contains (name_of_reference gr) "_subproof") &&
	200	not (string_string_contains (name_of_reference gr) "_admitted")
200	201
201	202	let (&&&&&) f g x y z = f x y z && g x y z
202	203

+53

-14

toplevel/vernac.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
	8	(* $Id: vernac.ml 13923 2011-03-21 16:25:20Z letouzey $ *)
9	9
10	10	(* Parsing of vernacular. *)
11	11

51	51	\| Error_in_file (_, _, e) -> e
52	52	\| e -> e
53	53
	54	(** Timeout handling *)
	55
	56	(** A global default timeout, controled by option "Set Default Timeout n".
	57	Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
	58
	59	let default_timeout = ref None
	60
	61	let _ =
	62	Goptions.declare_int_option
	63	{ Goptions.optsync = true;
	64	Goptions.optname = "the default timeout";
	65	Goptions.optkey = ["Default";"Timeout"];
	66	Goptions.optread = (fun () -> !default_timeout);
	67	Goptions.optwrite = ((:=) default_timeout) }
	68
	69	(** When interpreting a command, the current timeout is initially
	70	the default one, but may be modified locally by a Timeout command. *)
	71
	72	let current_timeout = ref None
	73
	74	(** Installing and de-installing a timer.
	75	Note: according to ocaml documentation, Unix.alarm isn't available
	76	for native win32. *)
	77
54	78	let timeout_handler _ = raise Timeout
	79
	80	let set_timeout n =
	81	let psh =
	82	Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
	83	ignore (Unix.alarm n);
	84	Some psh
	85
	86	let default_set_timeout () =
	87	match !current_timeout with
	88	\| Some n -> set_timeout n
	89	\| None -> None
	90
	91	let restore_timeout = function
	92	\| None -> ()
	93	\| Some psh ->
	94	(* stop alarm *)
	95	ignore(Unix.alarm 0);
	96	(* restore handler *)
	97	Sys.set_signal Sys.sigalrm psh
55	98
56	99	(* Opening and closing a channel. Open it twice when verbose: the first
57	100	channel is used to read the commands, and the second one to print them.

184	227
185	228	\| VernacTimeout(n,v) ->
186	229	if not !just_parsing then begin
187		let psh =
188		Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
189		ignore (Unix.alarm n);
190		let stop() =
191		(* stop alarm *)
192		ignore(Unix.alarm 0);
193		(* restore handler *)
194		Sys.set_signal Sys.sigalrm psh in
195		try interp v; stop()
196		with e -> stop(); raise e
	230	current_timeout := Some n;
	231	interp v
197	232	end
198	233
199	234	\| v ->
200	235	if not !just_parsing then
201		States.with_heavy_rollback interpfun
202		Cerrors.process_vernac_interp_error v
203
	236	let psh = default_set_timeout () in
	237	try
	238	States.with_heavy_rollback interpfun
	239	Cerrors.process_vernac_interp_error v;
	240	restore_timeout psh
	241	with e -> restore_timeout psh; raise e
204	242	in
205	243	try
	244	current_timeout := !default_timeout;
206	245	if do_beautify () then pr_new_syntax loc (Some com);
207	246	interp com
208	247	with e ->

+2

-4

toplevel/vernacentries.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: vernacentries.ml 13492 2010-10-04 21:20:01Z herbelin $ i)
	8	(i $Id: vernacentries.ml 13922 2011-03-21 16:25:18Z letouzey $ i)
9	9
10	10	(* Concrete syntax of the mathematical vernacular MV V2.6 *)
11	11

1012	1012	\| BoolValue b -> set_bool_option_value_gen locality key b
1013	1013
1014	1014	let vernac_unset_option locality key =
1015		try set_bool_option_value_gen locality key false
1016		with _ ->
1017		set_int_option_value_gen locality key None
	1015	unset_option_value_gen locality key
1018	1016
1019	1017	let vernac_add_option key lv =
1020	1018	let f = function