| Commit message (Expand) | Author | Age |
* | Change Ltac constr matching semantics to consider universes when merging two | Matthieu Sozeau | 2014-06-15 |
* | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau | 2014-06-11 |
* | Fix module order in printers.mllib | Matthieu Sozeau | 2014-06-10 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | 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-06-07 |
* | A little bit of documentation about V5.10 and V6.3 and V7. | Hugo Herbelin | 2014-06-01 |
* | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
* | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin | 2014-05-08 |
* | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin | 2014-05-08 |
* | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot | 2014-05-08 |
* | Remove Lemmas from base_include, it's not linked in dev/printers anymore | Matthieu Sozeau | 2014-05-06 |
* | Cleanup before merge with the trunk | Matthieu Sozeau | 2014-05-06 |
* | Add incompatibilities paragraph in doc about universe polymorphism. | Matthieu Sozeau | 2014-05-06 |
* | Add doc on the new API for universe polymorphism and primitive projections | Matthieu Sozeau | 2014-05-06 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau | 2014-05-06 |
* | 'Pretty' printer for wf_paths | Pierre | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | print futures in caml toplevel too | Enrico Tassi | 2014-04-25 |
* | Adding a debug printer for futures. | Pierre-Marie Pédrot | 2014-04-25 |
* | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot | 2014-04-23 |
* | 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-04-09 |
* | Printers for ltac environments. | Hugo Herbelin | 2014-04-05 |
* | A debug printer for Evd.Filter.t | Pierre Boutillier | 2014-04-02 |
* | Updated debugging printers | Hugo Herbelin | 2014-04-01 |
* | 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-05 |
* | 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-03-02 |
* | 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-27 |
* | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
* | app_node, stack, state printers | Pierre Boutillier | 2014-02-24 |
* | 'Pretty' printer for wf_paths | Pierre | 2014-01-11 |
* | Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd | Pierre Letouzey | 2014-01-08 |
* | Aux_file: cache information at compile time for later (re)use | Enrico Tassi | 2014-01-04 |
* | Support for evars and metas in native compiler. | Maxime Dénès | 2013-12-30 |
* | Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at | Pierre-Marie Pédrot | 2013-12-22 |
* | configure.ml: our configure script is now written in ML :-) | Pierre Letouzey | 2013-12-20 |
* | Adding printing of ltac envs to debugger. | Pierre-Marie Pédrot | 2013-11-30 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | Remove the Hiddentac module. | Arnaud Spiwack | 2013-11-25 |
* | A file listing old svn branches and tags | letouzey | 2013-11-18 |
* | Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by... | aspiwack | 2013-11-02 |