coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Init: some results in Type should rather be Defined than Qed	letouzey	2011-03-21
*	Makefile.build: states/initial.coq was wrongly done with -dont-load-proofs	letouzey	2011-03-21
*	Makefile.build: compile the stdlib with -dont-load-proofs by default	letouzey	2011-03-18
*	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey	2011-03-18
*	An option "Set Default Timeout n."	letouzey	2011-03-17
*	Goptions: repair Unset for int options	letouzey	2011-03-17
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	Adapt printers.mllib after my last commit	letouzey	2011-03-16
*	Finish branching functions handling module errors (cf. r13886)	letouzey	2011-03-16
*	Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)	letouzey	2011-03-16
*	Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extraction	letouzey	2011-03-16
*	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau	2011-03-13
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Keep information on which fields are subclasses in class declarations,	msozeau	2011-03-11
*	Inference of match predicate produces ill-typed unification problem,	msozeau	2011-03-11
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	- Better error messages taking unif. constraints into account.	msozeau	2011-03-11
*	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau	2011-03-10
*	Do not forget conv_pbs when resetting an evm:	msozeau	2011-03-10
*	ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditions	letouzey	2011-03-10
*	Solve evar instantiations in the right environment.	msozeau	2011-03-08
*	Fix declarations of [Add Setoid/Morphism...] in sections to not export	msozeau	2011-03-08
*	syntax for exponents	pottier	2011-03-08
*	adding eta in the vm	bgregoir	2011-03-08
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Revert commit r13883: instantiating ?n by a lambda when "?n a" has to	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	CHANGES: mentionning quickly Separate Extraction	letouzey	2011-03-07
*	Extraction: a warning when an opaque constant is enterred	letouzey	2011-03-07
*	Extraction: fix printing of haskell modular names	letouzey	2011-03-07
*	Extraction: avoid printing unused mutual fix components (fix #2477)	letouzey	2011-03-07
*	A new command "Separate Extraction"	letouzey	2011-03-07
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin	2011-03-05
*	Starting being more explicit on the reasons why module subtyping fails.	herbelin	2011-03-05
*	A few more betaiota on environments and types of error messages. Seems to	herbelin	2011-03-05
*	Added support for instantiation of ?n by a lambda when "?n a" has to	herbelin	2011-03-05
*	Reorganized a bit evarconv.ml:	herbelin	2011-03-05
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Instantiate evar by a lambda when "?n args" has to unify with Prod	herbelin	2011-03-05
*	Fixed a "feature" about subtyping records: one was expected not only	herbelin	2011-03-05
*	Restore documentation of library String which was removed in 2007 (r10049)	herbelin	2011-03-05
*	Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notation	herbelin	2011-03-05
*	Fixing injection bug #2493 (regression introduced by fixing injection	herbelin	2011-03-05
*	CHANGES: update of syntax for annotations of functor application	letouzey	2011-03-04
*	Extraction: improved indentation of extracted code (fix #2497)	letouzey	2011-03-04
*	Simplify proofs in Permutation using generalized rewriting.	msozeau	2011-03-04
*	- Allow to set a particular transparent_state for the local hint	msozeau	2011-03-04
*	checker: cleanup	glondu	2011-03-04
*	checker: add eta-expansion	glondu	2011-03-04