aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Expand)AuthorAge
...
| * 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
* | | 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
* Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
* Fixing "Load" without "Verbose" in coqtop, after vernac_com lost itsGravatar Hugo Herbelin2015-07-07
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* coqtop: reset the current file name after a load-vernac-sourceGravatar Enrico Tassi2015-05-29
* make Unset Silent work in coqcGravatar Enrico Tassi2015-05-29
* Adding an option -w to control Coq warning output.Gravatar Pierre-Marie Pédrot2015-05-14
* STM: process_error_hook set in Vernac where fname is known (fix #4229)Gravatar Enrico Tassi2015-05-12