aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqloop.ml
AgeCommit message (Expand)Author
2018-04-11[warnings] Remove `set_current_loc` hack.Emilio Jesus Gallego Arias
2018-04-04Merge 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-05Merge 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-27Update 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 APIEmilio Jesus Gallego Arias
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01[emacs] [toplevel] Make emacs flag local to the toplevel.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio 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.locatedEmilio Jesus Gallego Arias
2017-04-12[toplevel] [stm] cleanup in module openEmilio Jesus Gallego Arias
2017-04-12[vernac] vernacentries.mli cleanupEmilio 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/coqloopEmilio Jesus Gallego Arias
2016-10-18[pp] Add tagging function to all low-level printing calls.Emilio Jesus Gallego Arias
2016-10-17Vernac.ml: inlining read_vernac_file within load_vernac.Hugo Herbelin
2016-10-17Vernac.ml: parenthesizing a side-effect.Hugo Herbelin
2016-10-17Applying Emilio's suggestion to simplify type of eval_expr.Hugo Herbelin
2016-10-10Fixing #5133 (error reporting delayed).Hugo Herbelin
2016-10-09Attaching all extra imperative components of the lexer/parser state toHugo Herbelin
2016-09-29fix bug 3683 : adds references to the web site for the bug trackerYves Bertot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-20Add file name, line number and beginning of line position to locations.Maxime Dénès
2016-06-14Preventive compatibility fixes for flushing.Emilio Jesus Gallego Arias
2016-06-14Fix for bug #4784Emilio Jesus Gallego Arias
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-09Rename Lexer -> CLexer.Pierre-Marie Pédrot