| Age | Commit message (Expand) | Author |
|---|
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross |
| 2014-08-25 | Clean up a comment in plugins/romega/ReflOmegaCore | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-08-25 | Correct a spelling mistake | Jason Gross |
| 2014-08-18 | Lazy interpretation of patterns so that expressions such as "intros H H'/H" | Hugo Herbelin |
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin |
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin |
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-08-18 | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot |
| 2014-08-12 | A couple of fixes/improvements in -beautify, but backtracking on | Hugo Herbelin |
| 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 |
