aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Expand)AuthorAge
...
* | | [toplevel] Fix printing of parsing errors + corner case.Gravatar Emilio Jesus Gallego Arias2017-04-19
|/ /
* | [toplevel] Don't print goals if there is no pending proof.Gravatar Emilio Jesus Gallego Arias2017-04-13
* | [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | [stm] remove process_error_hookGravatar Emilio Jesus Gallego Arias2017-04-07
* | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
* | [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/vernacGravatar Emilio Jesus Gallego Arias2017-03-14
* | [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
* | [safe-string] Switch to buffer to `Bytes`Gravatar Emilio Jesus Gallego Arias2017-02-14
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| * Not using style tags when translating/beautifying a file.Gravatar Hugo Herbelin2016-11-05
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\|
| * [toplevel] Remove undocumented "just_parsing" flag.Gravatar Emilio Jesus Gallego Arias2016-10-17
| * [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
| * Vernac.ml: inlining read_vernac_file within load_vernac.Gravatar Hugo Herbelin2016-10-17
| * Grouping checks about commands together.Gravatar Hugo Herbelin2016-10-17
| * Vernac.ml: parenthesizing a side-effect.Gravatar Hugo Herbelin2016-10-17
| * Factorizing two instances of load_vernac.Gravatar Hugo Herbelin2016-10-17
| * Passing chan_beautify functionally rather than by side-effect.Gravatar Hugo Herbelin2016-10-17
| * Applying Emilio's suggestion to simplify type of eval_expr.Gravatar Hugo Herbelin2016-10-17
| * More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
| * Removing export of location_table outside of cLexer.Gravatar Hugo Herbelin2016-10-17
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
| * Attaching all extra imperative components of the lexer/parser state toGravatar Hugo Herbelin2016-10-09
| * Fixing beautification to file.Gravatar Hugo Herbelin2016-10-09
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
| * coqc -o now places .glob file near .vo fileGravatar Enrico Tassi2016-09-22
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ | |/ |/|
* | Fix #4941 - ~/.coqrc file confusing locationsGravatar Maxime Dénès2016-08-30
* | Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
|\ \
| * | [pp] Fix bug 4842 (Time prints in multiple lines)Gravatar Emilio Jesus Gallego Arias2016-08-19
| | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |/
* / [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\
| * Prevent "Load" from displaying all the intermediate subgoals.Gravatar Guillaume Melquiond2016-07-07
| * Do not display goals in -compile-verbose mode (bug #4841).Gravatar Guillaume Melquiond2016-07-07
* | rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* | 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
* | Merge remote-tracking branch 'github/pr/212' into trunkGravatar Maxime Dénès2016-06-20
|\ \
| * | Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:10:19 +0000