coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	More monomorphization.	ppedrot	2013-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
*	use List.rev_map whenever possible	letouzey	2013-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
\| \| \| \| \| \| \| \|	error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
*	No reason a priori for using unfiltered env for printing	herbelin	2013-01-29
\| \| \| \| \| \|	goal. Filtered env is intended to be type-safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16177 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
\| \| \| \| \| \|	for better uniformity of naming policy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16172 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of Label	ppedrot	2012-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Print univ constraints generated by a constant or inductive (when flag is set)	barras	2012-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning and small optimization in CList.	ppedrot	2012-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed #2926:	ppedrot	2012-10-29
\| \| \| \| \| \| \|	Extend "Print Opaque Dependencies" for transparent dependencies as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15935 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
\| \| \| \| \| \| \| \| \|	List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
\| \| \| \| \| \| \| \| \| \|	compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Slight modification to the printing of goals when in emacs mode.	courtieu	2012-07-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing test-suite	pboutill	2012-07-20
\| \| \| \| \| \| \| \|	- bug in r15614: hnf was identity - fix Print Assumptions - bug in r15624: Dump glob of Print About only for Glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15630 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A friendlier printing of remaining goals when no goal is focused.	aspiwack	2012-07-11
\| \| \| \| \| \| \|	Only their conclusion is printed (with a "subgoal n" header) like every goal but the first in the usual case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing Print Assumption display	ppedrot	2012-07-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15590 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Small change in the printing of proofs for use by coqide.	aspiwack	2012-07-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15577 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Another correction to the dependent existential variable printing	aspiwack	2012-07-10
\| \| \| \| \| \| \| \|	for emacs mode. Hopefully fixes Bug 2678 this time. Much saner and more compact code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15573 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Change how the number of open goals is printed.	aspiwack	2012-07-04
\| \| \| \| \| \| \| \| \| \|	If you are focused on 3 subgoals, and unfocusing would reveal 2 extra subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop will tell you: 3 focused subgoals (unfocused: 2-4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	When focused on an empty list of goal (after finishing a subproof introduced	aspiwack	2012-07-04
\| \| \| \| \| \| \|	by a bullet or a brace, for instance), the message "This subproof is complete […]" is now rendered before the list of goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15507 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing test-suite after last storm in Pp.	pboutill	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Replacing some str with strbrk	ppedrot	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7