aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
Commit message (Expand)AuthorAge
* [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
* Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\
* \ Merge PR #6210: More complete not-fully-applied error messages, #6145Gravatar Maxime Dénès2017-12-05
|\ \
| * | more complete not-fully-applied error messages, #6145Gravatar Paul Steckler2017-11-28
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* | | | Use Evarutil.has_undefined_evars for tactic has_evar.Gravatar Gaëtan Gilbert2017-11-24
| * | | Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
| * | | When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| * | | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| * | | Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/ / /
| | * Extending further PR#6047 (system to register printers for Ltac values).Gravatar Hugo Herbelin2017-11-24
| | * Printing again "intros **" as "intros" by default.Gravatar Hugo Herbelin2017-11-24
| |/ |/|
* | Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \
* \ \ Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \ \
| | * | [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
| |/ / |/| |
* | | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* | | Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesGravatar Maxime Dénès2017-11-21
|\ \ \
| * | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | * | Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
| |/ / |/| |
| * | Fixing printing of tactics encapsulated as tacarg with Tacexp.Gravatar Hugo Herbelin2017-11-15
| * | Using "l" printer for glob_constr, like for constr.Gravatar Hugo Herbelin2017-11-15
| |/
* / [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|/
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
| * [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* | Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
|/
* Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\
* \ Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Maxime Dénès2017-11-03
|\ \
| | * Ltac Debug: exporting env and sigma when needed so that term can be printed.Gravatar Hugo Herbelin2017-11-02
| | * Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
| | * Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
| | * Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
| | * Exporting a few more printing functions.Gravatar Hugo Herbelin2017-11-02
| | * Improving checks about the list separator in tactic notations.Gravatar Hugo Herbelin2017-11-02
| |/ |/|
| * Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Hugo Herbelin2017-10-30
* | Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\ \
* \ \ Merge PR #677: Trunk+abstracting injection flagsGravatar Maxime Dénès2017-10-27
|\ \ \ | |_|/ |/| |
| * | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | * [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| |/
* / Typo in comment in tactic_matching.ml.Gravatar Hugo Herbelin2017-10-24
|/
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
* Merge PR #1087: [stm] Switch to a functional APIGravatar Maxime Dénès2017-10-09
|\
* \ Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...Gravatar Maxime Dénès2017-10-09
|\ \
* \ \ Merge PR #1114: Generic handling of nameable objects for pluginsGravatar Maxime Dénès2017-10-09
|\ \ \
| | | * [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
| |_|/ |/| |
| | * [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
| |/ |/|
* | Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\ \
| | * Ltac uses the new generic locatable API.Gravatar Pierre-Marie Pédrot2017-10-03
| | * Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
| |/ |/|
* | Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Gravatar Maxime Dénès2017-10-03
|\ \