aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
AgeCommit message (Expand)Author
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2015-02-24[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Arnaud Spiwack
2015-02-23Compensating 6fd763431 on postponing subtyping evar-evar problems.Hugo Herbelin
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-14Fix merging of name maps in union of universe contexts.Matthieu Sozeau
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-07Improved tracking of the origin of evars.Hugo Herbelin
2014-12-05More consistent printing of evars in evar_map debugging printer.Hugo Herbelin
2014-12-04New approach to deal with evar-evar unification problems in differentHugo Herbelin
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-08Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Hugo Herbelin
2014-11-04Experimentally applying eager evar substitution at the same time asHugo Herbelin
2014-10-27Removing dead code from Evd.Pierre-Marie Pédrot
2014-10-27Removing the Evd.diff function.Pierre-Marie Pédrot
2014-10-27Removing the Evd.merge function.Pierre-Marie Pédrot
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-22Add more primitives to the [Monad.Make] arguments.Arnaud Spiwack
2014-10-21Dead code.Hugo Herbelin
2014-10-16Refine: proper scoping of the future goals.Arnaud Spiwack
2014-10-16Move the handling of the principal evar from refine to evd.Arnaud Spiwack
2014-10-16Move the handling a new evars from the [Proofview.Refine] module to [Evd].Arnaud Spiwack
2014-10-16Evd: a few comments to document the increasingly wide internal [evar_map] type.Arnaud Spiwack
2014-10-16Evd: remove/update obsolete comments.Arnaud Spiwack
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-10-03Fixing ennoying warning about evars named ?23 and so on.Hugo Herbelin
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-13Exporting apply_subfilter from Evd.ml.Hugo Herbelin
2014-09-13Fixing synchronization of evar names table when merging evar_map.Hugo Herbelin
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-13Checking typability of evar instances. Using ";" to separate bindingsHugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-13Bettre pretty-printing of evar maps, avoids printing universe informationMatthieu Sozeau
2014-08-09Using the asymmetric merging primitive in Evd.Pierre-Marie Pédrot
2014-08-09Cleaning up interface of ContextSet.Pierre-Marie Pédrot
2014-08-09Tentative performance fix for Evd.merge_uctx.Pierre-Marie Pédrot
2014-08-05Small code simplification.Pierre-Marie Pédrot
2014-07-20Use kernel conversion on terms that contain universe variables during unifica...Matthieu Sozeau
2014-07-03When defining a monomorphic Program, do not allow arbitrary instantiationsMatthieu Sozeau
2014-06-30Clarifying 'No such bound variable' message in apply, as suggested in #2387Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:18:13 +0000