aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Expand)Author
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
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06Restore reasonable performance by not allocating during universe checks,Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-01-29Using Map.smartmap whenever deemed useful.Pierre-Marie Pédrot
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
2013-12-03Removing useless meta-related functions.Pierre-Marie Pédrot
2013-11-30Better heuristic for name generation backward compatibility. We fallbackPierre-Marie Pédrot
2013-11-30Tentative fix to recover fresh name generation as it was beforePierre-Marie Pédrot
2013-11-25Factoring: is_section_variable.Arnaud Spiwack
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
2013-11-04Nicer infered names in refine.aspiwack
2013-11-02push_rel_context: do not rename section variables.aspiwack
2013-11-02A newly introduced variable inside a named context is no longer α-renamed.aspiwack
2013-10-29Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.ppedrot
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-22Removing some generic equalities.ppedrot
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
2013-10-08Small code cleaning in Evarutil.ppedrot
2013-10-06Removing useless evar code.ppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 19:14:48 +0000