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
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
2016-01-20
Update copyright headers.
Maxime Dénès
2015-04-23
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-01-12
Update headers.
Maxime Dénès
2015-01-06
Fix some documentation typos.
Guillaume Melquiond
2014-12-16
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-11-24
Plugging console highlighting in for toplevel and compilation error messages.
Pierre-Marie Pédrot
2014-10-22
Make rint_location_in_file resilient to Cd (close 3630)
Enrico Tassi
2014-09-09
Undo: if the ui is coqtop (command line) then Undo is not part of the doc.
Enrico Tassi
2014-08-12
Fixing parsing of bullets after a "...".
Hugo Herbelin
2014-04-25
Fixing various backtrace recordings.
Pierre-Marie Pédrot
2014-03-05
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
[next]