aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* Merge PR#627: Obligations shrinking: shrink abstraction tooGravatar Maxime Dénès2017-05-20
|\
* \ Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\ \
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
* | | Uniformity of style for selecting plural or not; spacing for comma.Gravatar Hugo Herbelin2017-05-13
| | * Obligations shrinking: shrink abstraction tooGravatar Matthieu Sozeau2017-05-11
| |/ |/|
| * Adapted to EConstr.Gravatar Pierre Courtieu2017-05-05
| * Adding an even more compact mode for goal display.Gravatar Pierre Courtieu2017-05-03
* | Fix two new unused opens.Gravatar Maxime Dénès2017-05-02
|/
* Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\
* | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\ \
| | * Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
| | * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | * 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
|\ \ \ \ | |_|/ / |/| | |
| | | * Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
| | | * Fixing several wrong computations of implicit arguments by positionGravatar Hugo Herbelin2017-04-09
| | | * Minor cosmetic commit.Gravatar Hugo Herbelin2017-04-09
| | | * Removing internal support for accepting "{struct x}" and co in "Theorem with".Gravatar Hugo Herbelin2017-04-09
| |_|/ |/| |
| * | 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
|/ / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 06:07:29 +0000