| Age | Commit message (Expand) | Author |
|---|
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin |
| 2014-08-05 | More proofs independent of the names generated by induction/elim over | Hugo Herbelin |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-08-05 | Ring: prevent an error message to show in case of success. | Arnaud Spiwack |
| 2014-08-05 | Better fix of e5c025 | Pierre Boutillier |
| 2014-08-04 | STM: VtQuery holds the id of the state it refers to | Carst Tankink |
| 2014-08-03 | Fix to make Coq compile, I think this should still be accepted. | Matthieu Sozeau |
| 2014-08-02 | Better struture for Ltac internalization environments in Constrintern. | Pierre-Marie Pédrot |
| 2014-08-01 | micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true) | Frédéric Besson |
| 2014-08-01 | Compatibility for compilation with ocaml 3.12 (at least). | Hugo Herbelin |
| 2014-08-01 | micromega : improve efficiency/termination of type-checking | Frédéric Besson |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-08-01 | Removing some tactic compatibility layer. | Pierre-Marie Pédrot |
| 2014-07-31 | micromega : refification recognises @eq T for T convertible with Z or R | Frédéric Besson |
| 2014-07-29 | Add a type of untyped term to Ltac's value. | Arnaud Spiwack |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot |
| 2014-07-23 | Derive plugin: add some comments. | Arnaud Spiwack |
| 2014-07-23 | Derive plugin: code reorganisation for clarity. | Arnaud Spiwack |
| 2014-07-23 | Derive plugin: small refactoring. | Arnaud Spiwack |
| 2014-07-23 | Derive plugin: a more general interface. | Arnaud Spiwack |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 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 |
