aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
Commit message (Expand)AuthorAge
* Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
* [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
* Making explicit that errors happen in one of five executation phases.Gravatar Hugo Herbelin2018-05-02
* [warnings] Remove `set_current_loc` hack.Gravatar Emilio Jesus Gallego Arias2018-04-11
* Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps with...Gravatar Enrico Tassi2018-04-04
|\
| * [toplevel] Protect goal printing better wrt Break [fixes #7142]Gravatar Emilio Jesus Gallego Arias2018-04-01
* | [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
|/
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* [toplevel] Modify printing goal strategy.Gravatar Emilio Jesus Gallego Arias2018-03-05
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
* [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
* [toplevel] Export the last document seen after `Drop`.Gravatar Emilio Jesus Gallego Arias2017-10-28
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
* Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * [toplevel] Fix a couple of logical errors in error printing.Gravatar Emilio Jesus Gallego Arias2017-05-05
| * [toplevel] Remove unused parameter from `Vernac.process_expr`.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [toplevel] [stm] cleanup in module openGravatar Emilio Jesus Gallego Arias2017-04-12
* [vernac] vernacentries.mli cleanupGravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
* [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
* [pp] Add anomaly header to anomaly error messages.Gravatar Emilio Jesus Gallego Arias2017-03-22
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
* [safe_string] toplevel/coqloopGravatar Emilio Jesus Gallego Arias2017-03-14
* [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
* Vernac.ml: inlining read_vernac_file within load_vernac.Gravatar Hugo Herbelin2016-10-17
* Vernac.ml: parenthesizing a side-effect.Gravatar Hugo Herbelin2016-10-17
* Applying Emilio's suggestion to simplify type of eval_expr.Gravatar Hugo Herbelin2016-10-17
* Fixing #5133 (error reporting delayed).Gravatar Hugo Herbelin2016-10-10
* Attaching all extra imperative components of the lexer/parser state toGravatar Hugo Herbelin2016-10-09
* fix bug 3683 : adds references to the web site for the bug trackerGravatar Yves Bertot2016-09-29
* 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
* Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
* Preventive compatibility fixes for flushing.Gravatar Emilio Jesus Gallego Arias2016-06-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 18:50:35 +0000