coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Fix semantics of change p with c to typecheck c at each specific occurrence o...	Matthieu Sozeau	2014-06-23
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	- Fix xml plugin treatment of inductives.	Matthieu Sozeau	2014-06-15
*	Deprecate options -dont, -lazy, -force-load-proofs.	Guillaume Melquiond	2014-06-13
*	Passing some tactics to the new monad type.	Pierre-Marie Pédrot	2014-06-12
*	In generalized rewrite, avoid retyping completely and constantly the conclusi...	Matthieu Sozeau	2014-06-11
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	Dead code.	Hugo Herbelin	2014-06-06
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	poly: remove unused attribute to STM nodes and vernac classificaiton	Enrico Tassi	2014-05-15
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau	2014-05-09
*	Renaming new_induct -> induction; new_destruct -> destruct.	Hugo Herbelin	2014-05-08
*	Fix extraction taking a type in the wrong environment.	Matthieu Sozeau	2014-05-06
*	Fix Field_tac to get fast reification again, with the fix on template univers...	Matthieu Sozeau	2014-05-06
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	Fix funind w.r.t. universes	Matthieu Sozeau	2014-05-06
*	Fix a pervasive equality use.	Matthieu Sozeau	2014-05-06
*	Fix derive plugin to properly treat universes	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	- Fix abstract forgetting about new constraints.	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
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-02
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
*	Remove unused lookup table.	Guillaume Melquiond	2014-04-28
*	Removing useless try-with clauses in Goal.enter variants.	Pierre-Marie Pédrot	2014-04-25
*	closing bug 3037	Julien Forest	2014-04-05
*	Using HMaps in global references.	Pierre-Marie Pédrot	2014-03-08
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Fixing some generic equalities in Micromega.	Pierre-Marie Pédrot	2014-03-03
*	Fixing Pervasives.equality in extraction.	Pierre-Marie Pédrot	2014-03-03
*	Getting rid of generic hashes in cc plugin.	Pierre-Marie Pédrot	2014-03-03
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Removing generic equality in Syntax plugin.	Pierre-Marie Pédrot	2014-03-02
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26