aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
...
| | | * | | | [safe-string] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | No functional change, one extra copy introduced but it seems hard to avoid.
| | * | | | Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
* | | | | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
|\ \ \ \ \
* | | | | | Micromega: removing a constant preventing micromega to be loaded before Logic.v.Gravatar Hugo Herbelin2017-03-09
| | | | | | | | | | | | | | | | | | | | | | | | The constant was useless after 9f56baf which fixed #5073.
| | | | * | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
| | | * | [ltac] Move dummy plugin to plugins folder.Gravatar Emilio Jesus Gallego Arias2017-03-03
| | | | | | | | | | | | | | | | | | | | This is needed to fix `Declare ML Module "ltac_plugin".
* | | | | Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Tactic Notation
| | | * | | TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
* | | | | Revert "Add empty ltac_plugin file for forward compatibility."Gravatar Maxime Dénès2017-02-24
| | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only.
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
|\ \ \ \ \ | | |_|/ / | |/| | |
* | | | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
* | | | | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
| | | * | [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
| |_|/ / |/| | |
| | | * Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |\ | |_|_|/ |/| | |
| | | * Porting the ssrmatching plugin to the new EConstr API.Gravatar Enrico Tassi2017-02-14
| | | |
| | | * Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip through the pretyper, and relies on suspicious flagging of evars in the evar source field to recognize original pattern holes. After the pattern_of_constr function was made evar-insensitive, it expanded evars that were solved by magical side-effects of the pretyper, even if it hadn't been asked to perform any heuristics. We backtrack on the insensitivity of the pattern_of_constr function. This may have a performance penalty in other dubious code, e.g. hints. In the long run we should get rid of the pattern_of_constr function.
| | | * Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | Now they are useless because all of the primitives are (should?) be evar-insensitive.
| | | * Fix a mishandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | Due to the introduction of the monadic layer, an exception was raised at a later time and not caught properly.
| | | * Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
| | | * Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
| | | * Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Omega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Micromega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Setoid_ring API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
| | | * Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 23:37:59 +0000