aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* Merge PR#583: [toplevel] More work on error handling.Gravatar Maxime Dénès2017-04-27
|\
| * [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | Removing tactic compatibility layer in Command.Gravatar Pierre-Marie Pédrot2017-04-24
|/
* Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\
* \ Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \
* | | [toplevel] [emacs] Don't quote errors in emacs mode.Gravatar Emilio Jesus Gallego Arias2017-04-23
| * | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
|/ /
| * [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* | [toplevel] Fix #5475Gravatar Emilio Jesus Gallego Arias2017-04-18
|/
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
* Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\
| * [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
| * [vernac] vernacentries.mli cleanupGravatar Emilio Jesus Gallego Arias2017-04-12
| * [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \
* \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ | |_|/ |/| |
| * | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \
* | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| |
* | | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ...Gravatar Maxime Dénès2017-04-07
|\ \ \
* \ \ \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \ \
| | * | | [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
| |/ / / |/| | |
* | | | Merge PR#502: [pp] Add anomaly header to error messages.Gravatar Maxime Dénès2017-04-04
|\ \ \ \
| | | * \ Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| | | |\ \ | |_|_|/ / |/| | | |
* | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-03
* | | | | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \ \ \ \
| | | | * | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | * | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* | | | | | Merge PR#511: [stm] Remove some obsolete vernacs/classification.Gravatar Maxime Dénès2017-03-30
|\ \ \ \ \ \
| | | | | * | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| * | | | | | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| | |_|_|/ / | |/| | | |
* / | | | | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
|/ / / / /
| * | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * | | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | | | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/ / / /
| | | * Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
| |_|/ |/| |
| | * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| |/ |/|
| * [pp] Add anomaly header to anomaly error messages.Gravatar Emilio Jesus Gallego Arias2017-03-22
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
* [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [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
* Merge PR#479: [future] Remove unused parameter greedy.Gravatar Maxime Dénès2017-03-20
|\
* | Merge PR#412: Remove outdated comment from 2002.Gravatar Maxime Dénès2017-03-14
| * [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 10:27:44 +0000