| Age | Commit message (Expand) | Author |
|---|
| 2014-06-23 | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-15 | - Fix xml plugin treatment of inductives. | Matthieu Sozeau |
| 2014-06-13 | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond |
| 2014-06-12 | Passing some tactics to the new monad type. | Pierre-Marie Pédrot |
| 2014-06-11 | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau |
| 2014-06-08 | 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-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-06-06 | Dead code. | Hugo Herbelin |
| 2014-06-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin |
| 2014-05-06 | 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-02 | Eta contractions to please cbn | Pierre Boutillier |
| 2014-05-01 | Fixing ml-doc. | Pierre-Marie Pédrot |
| 2014-04-28 | Remove unused lookup table. | Guillaume Melquiond |
| 2014-04-25 | Removing useless try-with clauses in Goal.enter variants. | Pierre-Marie Pédrot |
| 2014-04-05 | closing bug 3037 | Julien Forest |
| 2014-03-08 | Using HMaps in global references. | Pierre-Marie Pédrot |
| 2014-03-05 | 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-03 | 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-02 | 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-01 | Fixing pervasive comparisons | Pierre-Marie Pédrot |
| 2014-02-27 | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-26 | New compilation mode -vi2vo | Enrico Tassi |
| 2014-02-24 | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier |
