| Age | Commit message (Expand) | Author |
|---|
| 2014-10-31 | Feedback message: hold extra info to help routing | Enrico Tassi |
| 2014-10-27 | Removing an Evd.merge in Newring. | Pierre-Marie Pédrot |
| 2014-10-22 | Proofview: split [V82] module into [Unsafe] and [V82]. | Arnaud Spiwack |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-06 | Renaming goal-entering functions. | Pierre-Marie Pédrot |
| 2014-08-18 | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot |
| 2014-08-04 | STM: VtQuery holds the id of the state it refers to | Carst Tankink |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 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 |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi |
| 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-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-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 |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Stringset and Stringmap to String namespace. | ppedrot |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
