| Age | Commit message (Expand) | Author |
|---|
| 2014-11-27 | Reverting the following block of three commits: | Hugo Herbelin |
| 2014-11-26 | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin |
| 2014-11-15 | Adding a pretty-printing style library. | Pierre-Marie Pédrot |
| 2014-11-10 | Plug the dynamic tags in the Richpp mechanism. | Pierre-Marie Pédrot |
| 2014-10-22 | Split [Proofview] into a file where the basic operations on the state are def... | Arnaud Spiwack |
| 2014-10-07 | Adding a printer for hints. | Hugo Herbelin |
| 2014-10-01 | Fixing nice printing of error reporting with ml tactics bound to ltac names. | Hugo Herbelin |
| 2014-10-01 | Fixing use of arguments renaming in apply which was broken after | Hugo Herbelin |
| 2014-09-27 | Index keys instead of simply global references. | Matthieu Sozeau |
| 2014-08-04 | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi |
| 2014-06-10 | Fix module order in printers.mllib | Matthieu Sozeau |
| 2014-06-07 | Moving a Thread.yield in check_interrupt. | Pierre-Marie Pédrot |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-09 | Machine arithmetic operations for native compiler. | Maxime Dénès |
| 2014-04-09 | Had to split Nativelambda in two files because of Retroknowledge | Maxime Dénès |
| 2014-04-09 | Uint31 support. | Maxime Dénès |
| 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 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | 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-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-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-11-02 | Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by... | aspiwack |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-18 | Ephemeron: marshaling friendly keys | gareuselesinge |
| 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-07-02 | Removing the use of leveled tactics wit_tacticn. It is now handled | 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-18 | Proof-of-concept: moved four easy-to-handle generic arguments to | 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 Fmap from libraries, it is not used anymore. | ppedrot |
