aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernac.mli
AgeCommit message (Expand)Author
2016-10-17[toplevel] Remove undocumented "just_parsing" flag.Emilio Jesus Gallego Arias
2016-10-17Vernac.ml: inlining read_vernac_file within load_vernac.Hugo Herbelin
2016-10-17Applying Emilio's suggestion to simplify type of eval_expr.Hugo Herbelin
2016-10-09Attaching all extra imperative components of the lexer/parser state toHugo Herbelin
2016-06-20Add file name, line number and beginning of line position to locations.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-01-05Fix coqc -time (Closes: 3201)Enrico Tassi
2013-08-08State Transaction Machinegareuselesinge
2013-05-12Use the Hook module here and there.ppedrot
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
2013-03-13Vernac+Toplevel: get rid of DuringVernacInterpletouzey
2012-10-05coqtop -time : display per-command timingsletouzey
2012-08-08Updating headers.herbelin
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
2012-03-02Noise for nothingpboutill
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2004-07-16Nouvelle en-têteherbelin
2004-03-26Ajout entree pour exporter les debuts et fins de compilation en mode -xmlherbelin
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
2003-02-11Undo dans Coq IDEfilliatr
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-09-18Ajout d'une option et d'une fonction compile pour fabriquer les .voherbelin
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
1999-09-28corrections pour ocamlwebfilliatr
1999-09-28retablissement du toplevelfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 18:23:50 +0000