aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* 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
|/
* Merge PR #1095: [stm] Remove state handling from FuturesGravatar Maxime Dénès2017-10-20
|\
* | Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| * [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
|/
* [stdlib] Fix warnings on deprecated `Add Setoid`Gravatar Emilio Jesus Gallego Arias2017-10-15
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
* Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-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
| |_|/ / |/| | |
* | | | Merge PR #1118: Extraction : minor support stuff for the new Extraction Compu...Gravatar Maxime Dénès2017-10-06
|\ \ \ \
| | | * | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
| | | | * romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
| | | | * Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Gravatar Pierre Letouzey2017-10-05
| | | |/
* | | / Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...Gravatar Pierre Letouzey2017-10-05
| |_|/ |/| |
* | | Merge PR #1006: fix: ssrmatching and primitive projectionsGravatar Maxime Dénès2017-10-04
|\ \ \
* \ \ \ Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\ \ \ \
| | | * | Extraction : minor support stuff for the new Extraction Compute pluginGravatar Pierre Letouzey2017-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
|\ \ \
* \ \ \ Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\ \ \ \
* | | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| * | | | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
| * | | | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/ / / /
| * | | Properly display the "only" prefix for selectors (bug #5760).Gravatar Guillaume Melquiond2017-09-26
| | * | Report missing arguments in error messageGravatar Tej Chajed2017-09-21
| |/ /
| | * ssr: fix canonical strucut key comparison with primproj onGravatar Enrico Tassi2017-09-20
| |/
* | Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* | Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
|/
* Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\
* \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Gravatar Maxime Dénès2017-09-15
|\ \ \
| | | * Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| |_|/ |/| |
| | * Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| |/ |/|
* | Merge PR #931: Parametrize module bodyGravatar Maxime Dénès2017-09-07
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 07:51:25 +0000