aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.ml
Commit message (Expand)AuthorAge
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Univs: force all universes to be >= Set.Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Fixing loss of extra data in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Fixup for 866c41bGravatar Enrico Tassi2015-05-28
* 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
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
* More consistent printing of evars in evar_map debugging printer.Gravatar Hugo Herbelin2014-12-05
* 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
* Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Gravatar Hugo Herbelin2014-11-08
* 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
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
* Dead code.Gravatar Hugo Herbelin2014-10-21
* 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
* Evd: a few comments to document the increasingly wide internal [evar_map] type.Gravatar Arnaud Spiwack2014-10-16
* Evd: remove/update obsolete comments.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 debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Fixing ennoying warning about evars named ?23 and so on.Gravatar Hugo Herbelin2014-10-03
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* 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
* Fixing synchronization of evar names table when merging evar_map.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
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-19 09:14:13 +0000