aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Expand)AuthorAge
* Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* [toplevel] Modify printing goal strategy.Gravatar Emilio Jesus Gallego Arias2018-03-05
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
* | [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
* [stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Gravatar Emilio Jesus Gallego Arias2017-10-11
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* Merge PR #1106: Fix beautifierGravatar Maxime Dénès2017-10-05
|\
| * Remove catch-all try with in the beautifier.Gravatar Théo Zimmermann2017-09-27
| * Beautifier gets its own formatter: fixes BZ#5704.Gravatar Théo Zimmermann2017-09-27
* | [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Emilio Jesus Gallego Arias2017-09-27
|/
* Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\
* | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
| * Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
|/
* Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* "There are pending proofs" error message now lists the name of the proofs.Gravatar Théo Zimmermann2017-06-16
* Merge PR#758: [toplevel] Print error header on fatal batch error.Gravatar Maxime Dénès2017-06-14
|\
* | [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| * [toplevel] Print error header on fatal batch error.Gravatar Emilio Jesus Gallego Arias2017-06-10
|/
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Maxime Dénès2017-05-20
| |\
| * \ Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Gravatar Maxime Dénès2017-05-20
| |\ \
| | | * [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Emilio Jesus Gallego Arias2017-05-18
| | |/ | |/|
| | * [toplevel] Restore 8.6 goal printing behavior.Gravatar Emilio Jesus Gallego Arias2017-05-17
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
| |\ \ | | |/ | |/|
| * | [toplevel] Fix a couple of logical errors in error printing.Gravatar Emilio Jesus Gallego Arias2017-05-05
| | * Fix bug #3659: -time should understand multibyte encodings.Gravatar Pierre-Marie Pédrot2017-05-05
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * | [toplevel] Remove unused parameter from `Vernac.process_expr`.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * | [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * | [toplevel] Don't check proofs in -quick mode.Gravatar Emilio Jesus Gallego Arias2017-04-24
| * | [toplevel] Don't mask critical exceptions in vernac interpretation.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/ /
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \
| * | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 19:53:21 +0000