aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/printers.mllib
Commit message (Expand)AuthorAge
* 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
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Aux_file: cache information at compile time for later (re)useGravatar Enrico Tassi2014-01-04
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...Gravatar aspiwack2013-11-02
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Ephemeron: marshaling friendly keysGravatar gareuselesinge2013-10-18
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Fix compilation of dev/printres.cmaGravatar gareuselesinge2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Future library to represent pure computationsGravatar gareuselesinge2013-08-08
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18