| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2013-01-18 | Unset Asymmetric Patterns | pboutill |
| 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-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 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 |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-19 | Getting rid of the undocumented [complete] tactic, which was | ppedrot |
| 2012-07-07 | Ring_polynom : a restricted simpl instead of a unfold;fold | letouzey |
| 2012-07-05 | Legacy Ring and Legacy Field migrated to contribs | letouzey |
| 2012-07-05 | rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite | letouzey |
| 2012-07-05 | More cleanup in Ring_polynom and EnvRing | letouzey |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
