aboutsummaryrefslogtreecommitdiff
path: root/dev/printers.mllib
AgeCommit message (Expand)Author
2016-03-06Putting Tactic_debug just below Tacinterp.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2016-03-06Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-05Fix order of files in mllib.Maxime Dénès
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-18Adding a notion of monotonous evarmap.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-01-08Avoiding introducing yet another convention in naming files.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-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-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-07Adding a printer for hints.Hugo 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-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
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-25all coqide specific files moved into ide/Enrico Tassi
2014-06-10Fix module order in printers.mllibMatthieu 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-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-08Moving Dnet-related code to tactics/.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
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-03-05Adding a canary library. This canary is imperfect. It allows serializationPierre-Marie Pédrot
2014-03-05Added a new module HMap. It works (almost) like Map, except that it expectsPierre-Marie Pédrot
2014-03-05Adding a CSet module in Coq lib.Pierre-Marie Pédrot
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-02-27Remove unsafe code (Obj.magic) in Tacinterp.Arnaud Spiwack
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 01:30:57 +0000