aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 11:48:28 +0000