| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | 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 |
| | |\ | |||
| | | * | 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 |
| | | | | | |||
| * | | | | Refine API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | | |||
| * | | | | Goal API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | | |||
| * | | | | Cleaning up opening of the EConstr module in pretyping folder. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | | |||
| * | | | | Making judgment type generic over the type of inner constrs. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | | |||
| * | | | | Pretyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | | | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |