aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/printers.mllib
Commit message (Expand)AuthorAge
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving Tacenv to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tactic_debug to Hightactic.Gravatar Pierre-Marie Pédrot2016-03-20
* Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* Pushing Proofview further down the dependency alley.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
* Putting Tactic_debug just below Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
* Moving Tactic_debug to tactics/ folder.Gravatar Pierre-Marie Pédrot2016-03-06
* Moving Ltac traces to Tacexpr and Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
* Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Gravatar Pierre-Marie Pédrot2016-03-06
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\
| * Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\|
| * Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
* | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
* | Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
* | Adding a notion of monotonous evarmap.Gravatar Pierre-Marie Pédrot2015-10-18
* | Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* 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
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
* 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
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* 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
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Fix module order in printers.mllibGravatar Matthieu Sozeau2014-06-10
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
* Uint31 support.Gravatar Maxime Dénès2014-04-09
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 13:26:41 +0000