| Age | Commit message (Expand) | Author |
|---|
| 2014-03-05 | Adding a canary library. This canary is imperfect. It allows serialization | Pierre-Marie Pédrot |
| 2014-03-05 | Added a new module HMap. It works (almost) like Map, except that it expects | Pierre-Marie Pédrot |
| 2014-03-05 | Adding a CSet module in Coq lib. | Pierre-Marie Pédrot |
| 2014-03-02 | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey |
| 2014-03-02 | Set officially the minimal OCaml requirement to 3.12.1 | Pierre Letouzey |
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey |
| 2014-02-27 | Makefile: re-introduce 2 phases to avoid make strange -include's | Pierre Letouzey |
| 2014-02-27 | Code refactoring thanks to the new Monad module. | Arnaud Spiwack |
| 2014-02-27 | Remove unsafe code (Obj.magic) in Tacinterp. | Arnaud Spiwack |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-24 | app_node, stack, state printers | Pierre Boutillier |
| 2014-01-11 | 'Pretty' printer for wf_paths | Pierre |
| 2014-01-08 | Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd | Pierre Letouzey |
| 2014-01-04 | Aux_file: cache information at compile time for later (re)use | Enrico Tassi |
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès |
| 2013-12-22 | Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at | Pierre-Marie Pédrot |
| 2013-12-20 | configure.ml: our configure script is now written in ML :-) | Pierre Letouzey |
| 2013-11-30 | Adding printing of ltac envs to debugger. | Pierre-Marie Pédrot |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-11-25 | Remove the Hiddentac module. | Arnaud Spiwack |
| 2013-11-18 | A file listing old svn branches and tags | letouzey |
| 2013-11-02 | Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by... | aspiwack |
| 2013-11-02 | Removes Refine from the dev tools now that the module has been deleted. | aspiwack |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-29 | - install evar printer for debugging | msozeau |
| 2013-10-18 | Ephemeron: marshaling friendly keys | gareuselesinge |
| 2013-09-24 | Adding evar printing to debugger. | ppedrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-09-06 | Moving Searchstack to CStack, and normalizing names a bit. | ppedrot |
| 2013-08-25 | Added a more efficient way to recover the domain of a map. | ppedrot |
| 2013-08-20 | Fix compilation of dev/printres.cma | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-08-08 | Future library to represent pure computations | gareuselesinge |
| 2013-08-04 | Small cleaning of printing coercion failures in Ltac interpretation. | ppedrot |
| 2013-07-05 | Removing SortArgType. | ppedrot |
| 2013-07-05 | Expurgating the useless difference between List0 and List1 at the | ppedrot |
| 2013-07-02 | Removing the use of leveled tactics wit_tacticn. It is now handled | ppedrot |
| 2013-06-27 | Getting rid of IntroPatternArgType. | ppedrot |
| 2013-06-21 | Splitted up Genarg in four different levels: | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-19 | Adding genarg printer to debugger. | ppedrot |
| 2013-06-18 | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot |
| 2013-06-12 | Added Genarg as generic argument type. | ppedrot |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-05-28 | Adding a persistent stream data structure. | ppedrot |
| 2013-05-14 | Gmap is now useless, hail to Map! | ppedrot |
| 2013-05-14 | Removing useless uses of Gmap. | ppedrot |
| 2013-05-14 | Removing Fmap from libraries, it is not used anymore. | ppedrot |
| 2013-05-12 | Removing Fset, since it is not used anymore. | ppedrot |
| 2013-05-12 | Added a generic notion of hook. Hooks are functions to be set | ppedrot |
