| Age | Commit message (Expand) | Author |
|---|
| 2014-08-04 | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 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-28 | More open in base_include | Hugo Herbelin |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi |
| 2014-06-17 | Dummy commit to test the new setup of coq-commits mailinglist (bis) | Pierre Letouzey |
| 2014-06-17 | Dummy commit to test the new setup of coq-commits mailinglist | Pierre Letouzey |
| 2014-06-15 | Change Ltac constr matching semantics to consider universes when merging two | Matthieu Sozeau |
| 2014-06-11 | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau |
| 2014-06-10 | 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-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-06-01 | A little bit of documentation about V5.10 and V6.3 and V7. | Hugo Herbelin |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-08 | 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-06 | 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-04-25 | print futures in caml toplevel too | Enrico Tassi |
| 2014-04-25 | Adding a debug printer for futures. | Pierre-Marie Pédrot |
| 2014-04-23 | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot |
| 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-04-05 | Printers for ltac environments. | Hugo Herbelin |
| 2014-04-02 | A debug printer for Evd.Filter.t | Pierre Boutillier |
| 2014-04-01 | Updated debugging printers | Hugo Herbelin |
| 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 |
