aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
...
| | * | Fast path in computation of frozen evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Most of the time, undefined evars are not modified by the considered function, which leads to the costly recomputation of a trivial partition of evars. We simply take advantage of physical equality to discriminate when this is useless and special-case it in the type of frozen evars.
| | * | 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.
* | | Merge PR#437: Improve unification debug trace.Gravatar Maxime Dénès2017-03-17
|\ \ \
| | | * Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-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.
| | | * Dedicated datatype for aliases in Evarsolve.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Putting back the occur_meta_or_undefined_evar function in the old term API.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | This is another perfomance-critical function in unification. Putting it in the EConstr API was changing the heuristic, so better revert on that change.
| | | * 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.
| | | * Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Putting back the subst_defined_metas_evars function in the old term API.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It seems this is a performance-critical function for unification-heavy code. In particular, tactics relying on meta unification suffered an important penalty after this function was rewritten with the evar-insensitive API, as witnessed e.g. by Ncring_polynom whose compilation time increased by ~30%. I am not sure about the specification of this function, but it seems safer to revert the changes and just do it the old way. It may even disappear if we get rid of the old unification algorithm at some point.
| | | * 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
| | | |
| | | * 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
| | | |
| | | * Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Reductionops 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
| | | |
| | | * Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Hints 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
| | | |
| | | * Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Tacmach 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
| | | |
| | | * Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Classops 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
| | | |
| | | * Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Patternops 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
| | | |
| | | * Recordops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Find_subterm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
| | | * Cbv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 20:20:08 +0000