aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
...
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* More open in base_includeGravatar Hugo Herbelin2014-06-28
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Dummy commit to test the new setup of coq-commits mailinglist (bis)Gravatar Pierre Letouzey2014-06-17
* Dummy commit to test the new setup of coq-commits mailinglistGravatar Pierre Letouzey2014-06-17
* Change Ltac constr matching semantics to consider universes when merging twoGravatar Matthieu Sozeau2014-06-15
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* Fix module order in printers.mllibGravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* A little bit of documentation about V5.10 and V6.3 and V7.Gravatar Hugo Herbelin2014-06-01
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* Remove Lemmas from base_include, it's not linked in dev/printers anymoreGravatar Matthieu Sozeau2014-05-06
* Cleanup before merge with the trunkGravatar Matthieu Sozeau2014-05-06
* Add incompatibilities paragraph in doc about universe polymorphism.Gravatar Matthieu Sozeau2014-05-06
* Add doc on the new API for universe polymorphism and primitive projectionsGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* 'Pretty' printer for wf_pathsGravatar Pierre2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* print futures in caml toplevel tooGravatar Enrico Tassi2014-04-25
* Adding a debug printer for futures.Gravatar Pierre-Marie Pédrot2014-04-25
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
* Uint31 support.Gravatar Maxime Dénès2014-04-09
* Printers for ltac environments.Gravatar Hugo Herbelin2014-04-05
* A debug printer for Evd.Filter.tGravatar Pierre Boutillier2014-04-02
* Updated debugging printersGravatar Hugo Herbelin2014-04-01
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Makefile: re-introduce 2 phases to avoid make strange -include'sGravatar Pierre Letouzey2014-02-27
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
* 'Pretty' printer for wf_pathsGravatar Pierre2014-01-11
* Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evdGravatar Pierre Letouzey2014-01-08
* Aux_file: cache information at compile time for later (re)useGravatar Enrico Tassi2014-01-04
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 15:24:44 +0000