aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Maxime Dénès2017-06-01
* Fix bug #3659: -time should understand multibyte encodings.Gravatar Pierre-Marie Pédrot2017-05-05
* 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
* [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-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
* 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
* coqc -o now places .glob file near .vo fileGravatar Enrico Tassi2016-09-22
* 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
* | [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
* | | Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2016-06-19
|/ /
* | Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-06-16
* | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \
| | * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\|
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Revert "Protect the beautifier from change in the lexer state (typically by"Gravatar Hugo Herbelin2016-04-27
* | Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-04-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
|/
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 11:01:14 +0000