aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2014-12-16More printers for ltac signatures.Hugo Herbelin
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-07Removing import of Proofview in debugger because its module Goal hidesHugo Herbelin
2014-12-05More printers in tracer.Hugo Herbelin
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-11-27Reverting the following block of three commits:Hugo Herbelin
2014-11-26Experimenting always forcing convertibility on strict implicit argumentsHugo Herbelin
2014-11-23Add printer for transparent state for ocamldebug.Hugo Herbelin
2014-11-22Specific printer of Evar.Set.t for ocamldebug + more information inHugo Herbelin
2014-11-15Adding a pretty-printing style library.Pierre-Marie Pédrot
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-10-31More "open" by default for trace debugging.Hugo Herbelin
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-15Fix ill-typed debugging functionMatthieu Sozeau
2014-10-13Adding printers for ppproofview.Hugo Herbelin
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-10-09Adding printer for named_context_val and Goal.goal in debugger.Hugo Herbelin
2014-10-07Adding a printer for hints.Hugo Herbelin
2014-10-02Fixing interpretation of constr under binders which was broken afterHugo Herbelin
2014-10-01Fixing nice printing of error reporting with ml tactics bound to ltac names.Hugo Herbelin
2014-10-01Fixing use of arguments renaming in apply which was broken afterHugo Herbelin
2014-09-27Index keys instead of simply global references.Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-19win32: embed NSIS for plugin writersEnrico Tassi
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-17win32: remove outdated splash screenEnrico Tassi
2014-09-17win32: use subsystem windows on windows (and not console)Enrico Tassi
2014-09-12Fix base_include due to change in argument order of env and evar_mapMatthieu Sozeau
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-09-09Merge remote-tracking branch 'jason/win32-improvements' into trunkEnrico Tassi
2014-09-09Bump CoqSDK revision numberJason Gross
2014-09-09Add a VERBOSE flag to make-sdk-win32Jason Gross
2014-09-09Minor code style cleanup in make-sdk-win32Jason Gross
2014-09-09Support 64-bit cygwinJason Gross
2014-09-09Support machines that have a full or nonexistant C driveJason Gross
2014-09-09Support environments where `find` is Windows' findJason Gross
2014-09-09Installer for win improvedEnrico Tassi
2014-09-09Installer for win32Enrico Tassi
2014-08-26Debug RAKAMPierre Boutillier
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Fixing include of debugger.Pierre-Marie Pédrot
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-28Moved code for finding subterms (pattern, induction, set, generalize, ...)Hugo Herbelin
2014-06-28Made the subterm finding function make_abstraction independent of theHugo Herbelin
2014-06-28More open in base_includeHugo Herbelin
2014-06-25all coqide specific files moved into ide/Enrico Tassi