aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* win32: embed NSIS for plugin writersGravatar Enrico Tassi2014-09-19
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* win32: remove outdated splash screenGravatar Enrico Tassi2014-09-17
* win32: use subsystem windows on windows (and not console)Gravatar Enrico Tassi2014-09-17
* Fix base_include due to change in argument order of env and evar_mapGravatar Matthieu Sozeau2014-09-12
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Merge remote-tracking branch 'jason/win32-improvements' into trunkGravatar Enrico Tassi2014-09-09
|\
| * Bump CoqSDK revision numberGravatar Jason Gross2014-09-09
| * Add a VERBOSE flag to make-sdk-win32Gravatar Jason Gross2014-09-09
| * Minor code style cleanup in make-sdk-win32Gravatar Jason Gross2014-09-09
| * Support 64-bit cygwinGravatar Jason Gross2014-09-09
| * Support machines that have a full or nonexistant C driveGravatar Jason Gross2014-09-09
| * Support environments where `find` is Windows' findGravatar Jason Gross2014-09-09
* | Installer for win improvedGravatar Enrico Tassi2014-09-09
|/
* Installer for win32Gravatar Enrico Tassi2014-09-09
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Fixing include of debugger.Gravatar Pierre-Marie Pédrot2014-08-18
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 17:30:41 +0000