aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Expand)Author
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-02Refresh rigid universes as well, and in 8.4 compatibility mode,Matthieu Sozeau
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-26Hardening the API of evarmaps.Pierre-Marie Pédrot
2015-09-26Fixing bug #4347: Not_found Exception with some Records.Pierre-Marie Pédrot
2015-05-13Fix for a second avatar of bug #4234.Pierre-Marie Pédrot
2015-05-12Fixing bug #4234.Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-02-25STM: proof state also includes meta countersEnrico Tassi
2015-02-24[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Arnaud Spiwack
2015-01-12Update headers.Maxime Dénès
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-04Occur-check in refine.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-04A few Global.env removed.Hugo 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-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-13Using "Evd.restrict" in tactic clear so as to keep evar names.Hugo Herbelin
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-03- Fix has_undefined_evars not using its or_sorts argument anymore.Matthieu Sozeau
2014-07-20Use kernel conversion on terms that contain universe variables during unifica...Matthieu Sozeau
2014-07-14Add interface function to replace new_Type ()Matthieu Sozeau
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-13Fixing "clear" in internal_cut_replace: forbid dependencies in theHugo Herbelin
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
2014-05-08Cleanup code in pretyping/evarutilMatthieu Sozeau
2014-05-08Fix performance problem with unification in presence of universes (bug #3302)...Matthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:56:43 +0000