aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Collapse)AuthorAge
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\
* | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | | | | | | | The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| |
| * | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\ \
| | | * Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately.
| | | * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | |/ | |/| | | | | | | | | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
| * | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| | | | | | | | | | | | | | | | | | | | | - Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390.
| | * Show unused-intro-pattern warning.Gravatar Théo Zimmermann2017-03-14
| | | | | | | | | | | | This warning was shown in CoqIDE but not by coqc.
* | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| |
* | | 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.
* | | 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.
* | | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
* | | 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.
* | | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms.
* | | 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
| | |
* | | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | We make mli files look to what they were looking before the move to EConstr by opening this module.
* | | Removing various compatibility layers of tactics.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
| | |
* | | 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
| | |
* | | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Inv 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
| | |
* | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Refine 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
| | |
* | | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Find_subterm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | |/
| * Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ | | | | | | | | | Was PR#339: Documenting type class options, typeclasses eauto
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 23:23:35 +0000