| Age | Commit message (Expand) | Author |
|---|
| 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-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot |
| 2014-06-11 | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 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 bug preventing apply from unfolding Fixpoints. | 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-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-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-02-08 | Less dependencies in Omega. | Pierre-Marie Pédrot |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi |
| 2013-11-21 | Field_theory: nicer notations for constants 0 1 ... | Pierre Letouzey |
| 2013-11-02 | More Proofview.Goal.enter. | aspiwack |
| 2013-11-02 | Removed spurious try/with in Proofview.Notation.(>>=) and (>>==). | aspiwack |
| 2013-11-02 | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-30 | add "Print Ring" and "Print Field" vernacular commands | gareuselesinge |
| 2013-08-30 | Fixing the code of field_simplify_eq. | amahboub |
| 2013-08-25 | Added a more efficient way to recover the domain of a map. | ppedrot |
| 2013-08-23 | Fixing an incompleteness of the ring/field tactics | amahboub |
| 2013-08-22 | Correcting misplaced Proof command. | amahboub |
| 2013-08-22 | Fixing a significant efficiency leak in the code of the field tactic. | amahboub |
| 2013-08-22 | Field_theory : faster and nicer proofs + nice notations. | letouzey |
| 2013-08-22 | Ring_polynom : shorter proof for Psub_ok | letouzey |
| 2013-08-08 | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-07-05 | Expurgating the useless difference between List0 and List1 at the | ppedrot |
| 2013-06-22 | Now, idtac closures use maps instead of association list. | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-10 | Hiding tactic value representations. | ppedrot |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-05-29 | newring.ml4: interp constr arg at interp time (not parse time) | gareuselesinge |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-22 | code simplifications concerning Summary | letouzey |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-12 | Allowing different types of, not to be mixed, generic Stores through | ppedrot |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-18 | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey |
