index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernac.mli
Commit message (
Expand
)
Author
Age
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Fix coqc -time (Closes: 3201)
Enrico Tassi
2014-01-05
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
raise UnsafeSuccess -> feedback AddedAxiom
gareuselesinge
2013-04-25
*
Vernac+Toplevel: get rid of Error_in_file
letouzey
2013-03-13
*
Vernac+Toplevel: get rid of DuringVernacInterp
letouzey
2013-03-13
*
coqtop -time : display per-command timings
letouzey
2012-10-05
*
Updating headers.
herbelin
2012-08-08
*
A new status Unsafe in Interface. Meant for commands such as Admitted.
aspiwack
2012-07-12
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
*
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
*
Noise for nothing
pboutill
2012-03-02
*
Fixing bugs #2347 (part 2) and #2388: error message printing was done
herbelin
2010-09-18
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Delineating a API for Coq inside toplevel/vernac.ml
vgross
2010-02-12
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
Ajout entree pour exporter les debuts et fins de compilation en mode -xml
herbelin
2004-03-26
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
Undo dans Coq IDE
filliatr
2003-02-11
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Ajout d'une option et d'une fonction compile pour fabriquer les .vo
herbelin
2001-09-18
*
entetes
filliatr
2001-03-15
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
corrections pour ocamlweb
filliatr
1999-09-28
*
retablissement du toplevel
filliatr
1999-09-28