index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
toplevel.mllib
Commit message (
Expand
)
Author
Age
*
cut toploop(s) out of coqtop: now they are loaded dynamically
Enrico Tassi
2014-06-25
*
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
Pierre-Marie Pédrot
2014-04-25
*
Removing Autoinstance once and for all.
Pierre-Marie Pédrot
2014-04-25
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
coqtop: -check-vi-tasks and -schedule-vi-checking
Enrico Tassi
2014-01-05
*
A few fixes to the build system (mostly for ocamlbuild)
Pierre Letouzey
2013-12-16
*
Vernac classification streamlined (handles VERNAC EXTEND)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-07-02
*
Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?
ppedrot
2013-03-19
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29
*
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
*
migrate g_obligations.ml4 in parsing
letouzey
2012-04-26
*
lib directory is cut in 2 cma.
pboutill
2012-04-12
*
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
*
Final part of moving Program code inside the main code. Adapted add_definitio...
msozeau
2012-03-14
*
Integrated obligations/eterm and program well-founded fixpoint building to to...
msozeau
2012-03-14
*
Pure interfaces shouldn't be mentionned in .mllib
letouzey
2011-12-21
*
Separated the toplevel interface into a purely declarative module with associ...
ppedrot
2011-11-25
*
Moving XML handling to lib directory
ppedrot
2011-11-24
*
Added XML manipulation tools to compilation chain
ppedrot
2011-11-06
*
Ide: stronger separation from coqtop
letouzey
2011-03-23
*
deporting Coq specific code from ide to toplevel.
vgross
2010-05-31
*
Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...
letouzey
2009-12-08
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Changed the way to support compatibility with previous versions.
herbelin
2009-10-04
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20