aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
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
2014-05-06Add incompatibilities paragraph in doc about universe polymorphism.Matthieu Sozeau
2014-05-06Add doc on the new API for universe polymorphism and primitive projectionsMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06'Pretty' printer for wf_pathsPierre
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25print futures in caml toplevel tooEnrico Tassi
2014-04-25Adding a debug printer for futures.Pierre-Marie Pédrot
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-04-09Machine arithmetic operations for native compiler.Maxime Dénès
2014-04-09Had to split Nativelambda in two files because of RetroknowledgeMaxime Dénès
2014-04-09Uint31 support.Maxime Dénès
2014-04-05Printers for ltac environments.Hugo Herbelin
2014-04-02A debug printer for Evd.Filter.tPierre Boutillier
2014-04-01Updated debugging printersHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:32:48 +0000