Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix a heuristic used by legacy typeclass resolution. | Pierre-Marie Pédrot | 2017-04-08 |
| | | | | | | The evarmap used by the heuristic could contain resolved evars, which could lead to a failure of backtracking in the EConstr branch. This is experimental and may be to costly. | ||
* | Merge branch 'master' into econstr | Pierre-Marie Pédrot | 2017-04-07 |
|\ | |||
| * | Merge PR#508: Optimize pending evars | Maxime Dénès | 2017-04-06 |
| |\ | |||
* | | | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | 2017-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. | ||
* | | | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | 2017-04-01 |
| | | | | | | | | | | | | | | | For now we only normalize sorts, and we leave instances for the next commit. | ||
* | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 |
|\| | | |||
| * | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-23 |
| |\ \ | |||
| | | * | Fast path for implicit tactic solving. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-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. | ||
| | * | Merge PR#480: show unused intro pattern warning | Maxime Dénès | 2017-03-22 |
| | |\ | |||
| * | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-03-22 |
| |\| | | |||
| * | | | Attempt to improve error message when "apply in" fail. | Hugo Herbelin | 2017-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. | Théo Zimmermann | 2017-03-14 |
| | | | | | | | | | | | | | | | | This warning was shown in CoqIDE but not by coqc. | ||
| | * | | Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals ↵ | Maxime Dénès | 2017-03-10 |
| | |\ \ | | | |/ | | |/| | | | | | correctly as… | ||
* | | | | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 |
|\| | | | |||
* | | | | Quick hack to fix interpretation of patterns in Ltac. | Pierre-Marie Pédrot | 2017-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 a subtle nf_enter in Class_tactics. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | | | | | | | | | | | | | | | | | The underlying hint mode implementation was not using the evar-insensitive API so that it resulted in strange bugs. | ||
* | | | | Removing most nf_enter in tactics. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | | | | | | | | | | | | | | | | | Now they are useless because all of the primitives are (should?) be evar-insensitive. | ||
* | | | | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Do not ask for a normalized goal to get hypotheses and conclusions. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Removing compatibility layers from Tacticals | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Cleaning up interfaces. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Removing compatibility layers related to printing. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Eqdecide API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Class_tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Eauto API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Auto API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Hints API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Leminv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Inv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Contradiction API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Equality API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Elim API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Hipattern API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Tacticals API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Clenv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | |||
* | | | | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | |