aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
Commit message (Expand)AuthorAge
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* Fix bug #4151: discrepancy between exact and eexact/eassumption.Gravatar Matthieu Sozeau2015-11-02
* Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Univs: fix FingerTree contrib.Gravatar Matthieu Sozeau2015-10-07
* Univs (evd): deal with global universes and sideffGravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Adding an extensible global state to evarmaps.Gravatar Pierre-Marie Pédrot2015-05-19
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Add function to fix the non-substituted universe variables of an evar_map.Gravatar Matthieu Sozeau2015-03-17
* [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Gravatar Arnaud Spiwack2015-02-24
* Compensating 6fd763431 on postponing subtyping evar-evar problems.Gravatar Hugo Herbelin2015-02-23
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* New approach to deal with evar-evar unification problems in differentGravatar Hugo Herbelin2014-12-04
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Experimentally applying eager evar substitution at the same time asGravatar Hugo Herbelin2014-11-04
* Removing dead code from Evd.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.diff function.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.merge function.Gravatar Pierre-Marie Pédrot2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* Move the handling a new evars from the [Proofview.Refine] module to [Evd].Gravatar Arnaud Spiwack2014-10-16
* Adding a tactic which fails if one of the goals under focus is dependent in a...Gravatar Hugo Herbelin2014-10-13
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Exporting apply_subfilter from Evd.ml.Gravatar Hugo Herbelin2014-09-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* When building on-the-fly elimination principles, set the predicates universe ...Gravatar Matthieu Sozeau2014-06-29
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 21:51:11 +0000