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