aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Expand)AuthorAge
* coqc -o now places .glob file near .vo fileGravatar Enrico Tassi2016-09-22
* Fix #4941 - ~/.coqrc file confusing locationsGravatar Maxime Dénès2016-08-30
* Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
|\
| * [pp] Fix bug 4842 (Time prints in multiple lines)Gravatar Emilio Jesus Gallego Arias2016-08-19
* | [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\
| * Prevent "Load" from displaying all the intermediate subgoals.Gravatar Guillaume Melquiond2016-07-07
| * Do not display goals in -compile-verbose mode (bug #4841).Gravatar Guillaume Melquiond2016-07-07
* | rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Merge remote-tracking branch 'github/pr/212' into trunkGravatar Maxime Dénès2016-06-20
|\ \
| * | Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
* | | Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2016-06-19
|/ /
* | Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-06-16
* | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \
| | * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\|
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Revert "Protect the beautifier from change in the lexer state (typically by"Gravatar Hugo Herbelin2016-04-27
* | Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-04-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
|/
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
* Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
* Fixing "Load" without "Verbose" in coqtop, after vernac_com lost itsGravatar Hugo Herbelin2015-07-07
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* coqtop: reset the current file name after a load-vernac-sourceGravatar Enrico Tassi2015-05-29
* make Unset Silent work in coqcGravatar Enrico Tassi2015-05-29
* Adding an option -w to control Coq warning output.Gravatar Pierre-Marie Pédrot2015-05-14
* STM: process_error_hook set in Vernac where fname is known (fix #4229)Gravatar Enrico Tassi2015-05-12
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Update headers.Gravatar Maxime Dénès2015-01-12
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Removing a pperrnl.Gravatar Pierre-Marie Pédrot2014-11-15
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 13:38:23 +0000