aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/printers.mllib
Commit message (Expand)AuthorAge
* No more dev/printers.cmaGravatar Pierre Letouzey2016-07-26
* rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* proofs/proofs.mllib: no more proof_errors !Gravatar Pierre Letouzey2016-06-08
* Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
|\
| * Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 14:05:54 +0000