aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
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
2014-06-17Dummy commit to test the new setup of coq-commits mailinglist (bis)Pierre Letouzey
2014-06-17Dummy commit to test the new setup of coq-commits mailinglistPierre Letouzey
2014-06-15Change Ltac constr matching semantics to consider universes when merging twoMatthieu Sozeau
2014-06-11- Fix bug #3368, due to wrong use of the Cst_stack for projections.Matthieu Sozeau
2014-06-10Fix module order in printers.mllibMatthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-07Moving a Thread.yield in check_interrupt.Pierre-Marie Pédrot
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-06-01A little bit of documentation about V5.10 and V6.3 and V7.Hugo Herbelin
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-08Isolating a function "make_abstraction", new name of "letin_abstract",Hugo Herbelin
2014-05-08Renaming new_induct -> induction; new_destruct -> destruct.Hugo Herbelin
2014-05-08Moving Dnet-related code to tactics/.Pierre-Marie Pédrot
2014-05-06Remove Lemmas from base_include, it's not linked in dev/printers anymoreMatthieu Sozeau
2014-05-06Cleanup before merge with the trunkMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:12:54 +0000