| Commit message (Expand) | Author | Age |
|---|
| * | STM: encapsulate Pp.message in Feedback.feedback |  Carst Tankink | 2014-08-04 |
| * | A tentative uniform naming policy in module Inductiveops. |  Hugo Herbelin | 2014-08-01 |
| * | 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-28 |
| * | all coqide specific files moved into ide/ |  Enrico Tassi | 2014-06-25 |
| * | 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-17 |
| * | 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 |
Carst Tankink
Hugo Herbelin
Enrico Tassi
Pierre Letouzey
Matthieu Sozeau
Pierre-Marie Pédrot
Pierre
Maxime Dénès
Arnaud Spiwack