coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Fix a pervasive equality use.	Matthieu Sozeau	2014-05-06
*	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing Pervasives.equality in extraction.	Pierre-Marie Pédrot	2014-03-03
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 6)	letouzey	2013-03-13
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Extraction: same as commit 16203, hopefully without NotASort exns	letouzey	2013-02-18
*	Fix extraction of inductive types that Coq auto-detects to be in Prop	letouzey	2013-02-14
*	Modulification of Label	ppedrot	2012-12-18
*	Extraction of projections: restrict a hack to ocaml only (fix #2941)	letouzey	2012-12-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Extraction Implicit: consider the parameters of a constructor (fix #2905)	letouzey	2012-10-30
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Fix Extraction Implicit on axioms.	aspiwack	2012-08-24
*	Updating headers.	herbelin	2012-08-08
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10
*	Extraction: avoid internal eta-reduction (fix #2570)	letouzey	2011-12-08
*	Extraction: try to avoid issues with an Include directly inside a .v	letouzey	2011-11-30
*	Extraction: Richer patterns in matchs as proposed by P.N. Tollitte	letouzey	2011-11-28
*	Extraction Implicit: fix the numbering of constructor arguments	letouzey	2011-09-05
*	Extraction: allow extraction of records with anonymous fields (fix #2555)	letouzey	2011-08-25
*	Extraction: replace generic = on mutual_inductive_body by mib_equal	puech	2011-07-29
*	Set Extraction KeepSingleton: an option for not decapsulating singleton types	letouzey	2011-07-04
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Extraction: opaque terms are not traversed anymore by default	letouzey	2011-04-13
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Extraction: customized inductives are always standard	glondu	2011-03-31
*	Extraction: a warning when an opaque constant is enterred	letouzey	2011-03-07
*	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey	2010-12-21
*	Dead code in extraction	letouzey	2010-09-24
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24