index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernac.ml
Commit message (
Expand
)
Author
Age
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
*
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-27
*
[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
*
[toplevel] Don't check proofs in -quick mode.
Emilio Jesus Gallego Arias
2017-04-24
*
[toplevel] Don't mask critical exceptions in vernac interpretation.
Emilio Jesus Gallego Arias
2017-04-24
*
Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.
Maxime Dénès
2017-04-24
|
\
|
*
[flags] Deprecate is_silent/is_verbose in favor of single flag.
Emilio Jesus Gallego Arias
2017-04-21
*
|
[toplevel] Fix printing of parsing errors + corner case.
Emilio Jesus Gallego Arias
2017-04-19
|
/
*
[toplevel] Don't print goals if there is no pending proof.
Emilio Jesus Gallego Arias
2017-04-13
*
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-04-12
*
[stm] remove process_error_hook
Emilio Jesus Gallego Arias
2017-04-07
*
[nit] Fix a couple incorrect uses of msg_error.
Emilio Jesus Gallego Arias
2017-03-24
*
[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-21
*
[safe_string] toplevel/vernac
Emilio Jesus Gallego Arias
2017-03-14
*
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
2017-02-15
*
[safe-string] Switch to buffer to `Bytes`
Emilio Jesus Gallego Arias
2017-02-14
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
\
|
*
Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"
Maxime Dénès
2016-11-18
|
*
[stm] Remove STM-related vernaculars
Emilio Jesus Gallego Arias
2016-11-17
|
*
Not using style tags when translating/beautifying a file.
Hugo Herbelin
2016-11-05
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
*
[pp] Add tagging function to all low-level printing calls.
Emilio Jesus Gallego Arias
2016-10-18
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-18
|
\
|
|
*
[toplevel] Remove undocumented "just_parsing" flag.
Emilio Jesus Gallego Arias
2016-10-17
|
*
[toplevel] Remove duplicate beautify flags.
Emilio Jesus Gallego Arias
2016-10-17
|
*
Vernac.ml: inlining read_vernac_file within load_vernac.
Hugo Herbelin
2016-10-17
|
*
Grouping checks about commands together.
Hugo Herbelin
2016-10-17
|
*
Vernac.ml: parenthesizing a side-effect.
Hugo Herbelin
2016-10-17
|
*
Factorizing two instances of load_vernac.
Hugo Herbelin
2016-10-17
|
*
Passing chan_beautify functionally rather than by side-effect.
Hugo Herbelin
2016-10-17
|
*
Applying Emilio's suggestion to simplify type of eval_expr.
Hugo Herbelin
2016-10-17
|
*
More on making the lexer more functional (continuing b8ae2de5 and
Hugo Herbelin
2016-10-17
|
*
Removing export of location_table outside of cLexer.
Hugo Herbelin
2016-10-17
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
|
\
|
|
*
Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
Hugo Herbelin
2016-10-09
|
*
Attaching all extra imperative components of the lexer/parser state to
Hugo Herbelin
2016-10-09
|
*
Fixing beautification to file.
Hugo Herbelin
2016-10-09
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
|
*
coqc -o now places .glob file near .vo file
Enrico Tassi
2016-09-22
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
|
|
/
|
/
|
*
|
Fix #4941 - ~/.coqrc file confusing locations
Maxime Dénès
2016-08-30
*
|
Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6
Pierre-Marie Pédrot
2016-08-24
|
\
\
|
*
|
[pp] Fix bug 4842 (Time prints in multiple lines)
Emilio Jesus Gallego Arias
2016-08-19
|
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
|
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
|
/
*
/
[pp] Fix newline issues.
Emilio Jesus Gallego Arias
2016-08-19
|
/
[next]