index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
/
coqloop.ml
Age
Commit message (
Expand
)
Author
2018-04-11
[warnings] Remove `set_current_loc` hack.
Emilio Jesus Gallego Arias
2018-04-04
Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps with...
Enrico Tassi
2018-04-01
[toplevel] Protect goal printing better wrt Break [fixes #7142]
Emilio Jesus Gallego Arias
2018-04-01
[stm] Move VernacBacktrack to the toplevel.
Emilio Jesus Gallego Arias
2018-03-11
[vernac] Move `Quit` and `Drop` to the toplevel layer.
Emilio Jesus Gallego Arias
2018-03-05
[toplevel] Modify printing goal strategy.
Emilio Jesus Gallego Arias
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-02-28
[toplevel] Update state when `Drop` exception is thrown [#6872]
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-15
[toplevel] Make toplevel state into a record.
Emilio Jesus Gallego Arias
2018-02-09
[error] Replace msg_error by a proper exception.
Emilio Jesus Gallego Arias
2017-12-23
[flags] Move global time flag into an attribute.
Emilio Jesus Gallego Arias
2017-10-28
[toplevel] Export the last document seen after `Drop`.
Emilio Jesus Gallego Arias
2017-10-06
[stm] Switch to a functional API
Emilio Jesus Gallego Arias
2017-09-14
Using an algebraic type for distinguishing toplevel input from location in file.
Hugo Herbelin
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-11
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-01
[emacs] [toplevel] Make emacs flag local to the toplevel.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-05
[toplevel] Fix a couple of logical errors in error printing.
Emilio Jesus Gallego Arias
2017-04-25
[toplevel] Remove unused parameter from `Vernac.process_expr`.
Emilio Jesus Gallego Arias
2017-04-25
[toplevel] Use exception information for error printing.
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-12
[toplevel] [stm] cleanup in module open
Emilio Jesus Gallego Arias
2017-04-12
[vernac] vernacentries.mli cleanup
Emilio Jesus Gallego Arias
2017-04-12
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-04-07
[camlpX] Remove camlp4 compat layer.
Emilio Jesus Gallego Arias
2017-04-05
[toplevel] Remove exception error printer in favor of feedback printer.
Emilio Jesus Gallego Arias
2017-03-22
[pp] Add anomaly header to anomaly error messages.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Move terminal-specific tagging to the toplevel.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Remove special tag type and handler from Pp.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Prepare for serialization, remove opaque glue.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`
Emilio Jesus Gallego Arias
2017-03-14
[safe_string] toplevel/coqloop
Emilio Jesus Gallego Arias
2016-10-18
[pp] Add tagging function to all low-level printing calls.
Emilio Jesus Gallego Arias
2016-10-17
Vernac.ml: inlining read_vernac_file within load_vernac.
Hugo Herbelin
2016-10-17
Vernac.ml: parenthesizing a side-effect.
Hugo Herbelin
2016-10-17
Applying Emilio's suggestion to simplify type of eval_expr.
Hugo Herbelin
2016-10-10
Fixing #5133 (error reporting delayed).
Hugo Herbelin
2016-10-09
Attaching all extra imperative components of the lexer/parser state to
Hugo Herbelin
2016-09-29
fix bug 3683 : adds references to the web site for the bug tracker
Yves Bertot
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-06-29
A new infrastructure for warnings.
Maxime Dénès
2016-06-20
Add file name, line number and beginning of line position to locations.
Maxime Dénès
2016-06-14
Preventive compatibility fixes for flushing.
Emilio Jesus Gallego Arias
2016-06-14
Fix for bug #4784
Emilio Jesus Gallego Arias
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-09
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
[prev]
[next]