aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fix a mishandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | Due to the introduction of the monadic layer, an exception was raised at a later time and not caught properly.
* 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.
* Moving evar-normalization functions to EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | This removes code duplication between Evarutil and EConstr.
* 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.
* Making Evd independent from Namegen.Gravatar Pierre-Marie Pédrot2017-02-14
|
* 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
|
* Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
* 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
|
* Removing compatibility layers from TacticalsGravatar 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.
* Omega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Micromega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Funind API using EConstr.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
|
* Setoid_ring API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Proofview.Goal primitive 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
|
* Tauto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* G_class API using Econstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* G_auto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Extratactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Eqdecide API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Eauto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Auto 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
|
* Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tacticals 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
|
* Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 12:57:00 +0000