Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | * | Namegen primitives now apply on evar constrs. | 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. | |||
| | | * | Moving printing code from Evd to Termops. | 2017-02-14 | ||
| | | | | ||||
| | | * | Chasing a few unsafe constr coercions. | 2017-02-14 | ||
| | | | | ||||
| | | * | Putting back the subst_defined_metas_evars function in the old term API. | 2017-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. | 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. | 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. | 2017-02-14 | ||
| | | | | ||||
| | | * | Cleaning up interfaces. | 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. | 2017-02-14 | ||
| | | | | ||||
| | | * | Removing compatibility layers related to printing. | 2017-02-14 | ||
| | | | | ||||
| | | * | Ltac now uses evar-based constrs. | 2017-02-14 | ||
| | | | | ||||
| | | * | Removing compatibility layers in Retyping | 2017-02-14 | ||
| | | | | ||||
| | | * | Removing some return type compatibility layers in Termops. | 2017-02-14 | ||
| | | | | ||||
| | | * | Cc API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Reductionops now return EConstrs. | 2017-02-14 | ||
| | | | | ||||
| | | * | Eliminating parts of the right-hand side compatibility layer | 2017-02-14 | ||
| | | | | ||||
| | | * | Rewrite API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Tactic_matching API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Class_tactics API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Hints API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Leminv API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Inv API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Tactics API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Clenv API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Tacmach API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Cleaning up opening of the EConstr module in pretyping folder. | 2017-02-14 | ||
| | | | | ||||
| | | * | Making judgment type generic over the type of inner constrs. | 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. | 2017-02-14 | ||
| | | | | ||||
| | | * | Pretyping API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Cases API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Coercion API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Classops API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Typeclasses API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Tacred API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Constr_matching API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Patternops API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Typing API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Evarconv API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Recordops API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Evarsolve API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Evardefine API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Find_subterm API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Cbv API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Retyping API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Nativenorm API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Vnorm API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Reductionops API using EConstr. | 2017-02-14 | ||
| | | | | ||||
| | | * | Termops API using EConstr. | 2017-02-14 | ||
| | | | | ||||
* | | | | Merge PR#393: Replace Typeops with Fast_typeops | 2017-02-08 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge branch 'v8.6' | 2017-02-01 | ||
|\ \ \ \ \ | | |_|/ / | |/| | | |