aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/toplevel.mllib
Commit message (Expand)AuthorAge
* [toplevel] Refactor command line argument handling.Gravatar Emilio Jesus Gallego Arias2018-02-09
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
* rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Remove Whelp commands.Gravatar Maxime Dénès2015-02-17
* cut toploop(s) out of coqtop: now they are loaded dynamicallyGravatar Enrico Tassi2014-06-25
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
* Removing Autoinstance once and for all.Gravatar Pierre-Marie Pédrot2014-04-25
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* coqtop: -check-vi-tasks and -schedule-vi-checkingGravatar Enrico Tassi2014-01-05
* A few fixes to the build system (mostly for ocamlbuild)Gravatar Pierre Letouzey2013-12-16
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?Gravatar ppedrot2013-03-19
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
* migrate g_obligations.ml4 in parsingGravatar letouzey2012-04-26
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Integrated obligations/eterm and program well-founded fixpoint building to to...Gravatar msozeau2012-03-14
* Pure interfaces shouldn't be mentionned in .mllibGravatar letouzey2011-12-21
* Separated the toplevel interface into a purely declarative module with associ...Gravatar ppedrot2011-11-25
* Moving XML handling to lib directoryGravatar ppedrot2011-11-24
* Added XML manipulation tools to compilation chainGravatar ppedrot2011-11-06
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
* Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...Gravatar letouzey2009-12-08
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20