aboutsummaryrefslogtreecommitdiff
path: root/toplevel/toplevel.mllib
AgeCommit message (Expand)Author
2021-01-27[sysinit] new component for system initializationEnrico Tassi
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2018-11-24[toplevel] Move compilation-related functions to their own module.Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-02-09[toplevel] Refactor command line argument handling.Emilio Jesus Gallego Arias
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-02-17Remove Whelp commands.Maxime Dénès
2014-06-25cut toploop(s) out of coqtop: now they are loaded dynamicallyEnrico Tassi
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
2014-04-25Removing Autoinstance once and for all.Pierre-Marie Pédrot
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-03-19Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?ppedrot
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-04-26migrate g_obligations.ml4 in parsingletouzey
2012-04-12lib directory is cut in 2 cma.pboutill
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2011-12-21Pure interfaces shouldn't be mentionned in .mllibletouzey
2011-11-25Separated the toplevel interface into a purely declarative module with associ...ppedrot
2011-11-24Moving XML handling to lib directoryppedrot
2011-11-06Added XML manipulation tools to compilation chainppedrot
2011-03-23Ide: stronger separation from coqtopletouzey
2010-05-31deporting Coq specific code from ide to toplevel.vgross
2009-12-08Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...letouzey
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-04Changed the way to support compatibility with previous versions.herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:04:46 +0000