| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-02-14 | Putting back the subst_defined_metas_evars function in the old term API. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-02-14 | Definining EConstr-based contexts. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-02-14 | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | |
| This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. | |||
| 2017-02-14 | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Cleaning up interfaces. | Pierre-Marie Pédrot | |
| We make mli files look to what they were looking before the move to EConstr by opening this module. | |||
| 2017-02-14 | 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 | Cc API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops 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 | Rewrite API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Class_tactics 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 | Tactics 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 | 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 | |
| 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. | |||
| 2017-02-14 | Unification API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Pretyping API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Cases API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Coercion API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Classops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Typeclasses API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tacred API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Constr_matching API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Patternops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Typing API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Evarconv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Recordops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Evarsolve API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Evardefine API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Find_subterm API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Cbv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Retyping API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Nativenorm API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Vnorm API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Termops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-08 | Merge PR#393: Replace Typeops with Fast_typeops | Maxime Dénès | |
| 2017-02-01 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-01-22 | Adding a new evar source to remember the name of evars which were | Hugo Herbelin | |
| named in the original term. Useful at least for debugging, useful to give a better message than "this placeholder", even if in the loc is known in this case. | |||
| 2017-01-22 | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins). | Hugo Herbelin | |
| A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing a matching over a "catch-all" variable, when let-ins occur in the arity. However ade2363e35 failed to understand what was the correct fix, introducing instead the regressions mentioned in #5322 and #5324. This fixes all of #5322 and #5324, as well as the handling of let-ins in the arity. Thanks to Jason for helping in diagnosing the problem. | |||
| 2016-12-13 | Improve unification debug trace. | Théo Zimmermann | |
| - Add a debug message when applying a heuristic. - Fix double newlines. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |