coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Propagate recent kernel changes to the checker	letouzey	2011-03-03
*	- Allow rewriting under abitrary products, not just those in Prop.	msozeau	2011-02-28
*	Add a flag to hide obligations in Program-generated terms under an	msozeau	2011-02-28
*	Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)	letouzey	2011-02-25
*	Fix indentation of default pattern in haskell case (bug #2476)	letouzey	2011-02-25
*	Filter out admitted subgoals from search results	glondu	2011-02-25
*	Ocamlbuild needs OCAML_LD_LIBRARY_PATH (bug #2502)	glondu	2011-02-25
*	Revert "syntax for exponents"	glondu	2011-02-25
*	Mod_subst: improving sharing of subst_mps	letouzey	2011-02-24
*	Some more simplification in Mod_subst	letouzey	2011-02-23