aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
AgeCommit message (Expand)Author
2016-10-22Fix a bug in error printing of unif constraintsMatthieu Sozeau
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-03Opacifying the type of evar naming structure in Evd.Pierre-Marie Pédrot
2016-01-27Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-29Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Pierre-Marie Pédrot
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-14Fixing evarmap implementation.Pierre-Marie Pédrot
2015-10-08Univs: fix bug #3807Matthieu Sozeau
2015-10-07Univs: fix FingerTree contrib.Matthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs (evd): deal with global universes and sideffMatthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-10-02Univs: force all universes to be >= Set.Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-27Fixing loss of extra data in Evd.Pierre-Marie Pédrot
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu Sozeau
2015-05-28Fixup for 866c41bEnrico Tassi
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-19Adding an extensible global state to evarmaps.Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-03-17Add function to fix the non-substituted universe variables of an evar_map.Matthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 01:45:54 +0000