aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* More printers for ltac signatures.Gravatar Hugo Herbelin2014-12-16
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Removing import of Proofview in debugger because its module Goal hidesGravatar Hugo Herbelin2014-12-07
* More printers in tracer.Gravatar Hugo Herbelin2014-12-05
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* Add printer for transparent state for ocamldebug.Gravatar Hugo Herbelin2014-11-23
* Specific printer of Evar.Set.t for ocamldebug + more information inGravatar Hugo Herbelin2014-11-22
* Adding a pretty-printing style library.Gravatar Pierre-Marie Pédrot2014-11-15
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
* More "open" by default for trace debugging.Gravatar Hugo Herbelin2014-10-31
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Fix ill-typed debugging functionGravatar Matthieu Sozeau2014-10-15
* Adding printers for ppproofview.Gravatar Hugo Herbelin2014-10-13
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Adding printer for named_context_val and Goal.goal in debugger.Gravatar Hugo Herbelin2014-10-09
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 01:17:39 +0000