coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	BigQ : setting correct arguments scopes	letouzey	2011-02-23
*	Try to fix the behavior of clenv_missing used when declaring hints	letouzey	2011-02-22
*	syntax for exponents	pottier	2011-02-22
*	anneaux commutatifs ou non, reification sans ml	pottier	2011-02-22
*	Some fixes of the test-suite scripts	letouzey	2011-02-21
*	Fix test-suite script.	msozeau	2011-02-21
*	In Program obligation, do not use auto on non-proposition goals by	msozeau	2011-02-17
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Fix compilation issues.	msozeau	2011-02-16
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	fix last commit about modules (subst_cl_typ may raise Not_found)	letouzey	2011-02-12
*	An automatic substitution of scope at functor application	letouzey	2011-02-11
*	Annotations at functor applications:	letouzey	2011-02-11
*	Mod_typing: some refactoring (common parts about MSEapply and co)	letouzey	2011-02-11
*	Safe_typing: some refactoring (avoiding copy-paste of record definitions)	letouzey	2011-02-11
*	Mod_subt: some more refactoring, substitution is also separated in two tables	letouzey	2011-02-11
*	Mod_subst: split delta_resolver in two tables (mp / kn)	letouzey	2011-02-11