aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
Commit message (Expand)AuthorAge
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* Move the handling a new evars from the [Proofview.Refine] module to [Evd].Gravatar Arnaud Spiwack2014-10-16
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Using "Evd.restrict" in tactic clear so as to keep evar names.Gravatar Hugo Herbelin2014-09-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* - Fix has_undefined_evars not using its or_sorts argument anymore.Gravatar Matthieu Sozeau2014-08-03
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* Add interface function to replace new_Type ()Gravatar Matthieu Sozeau2014-07-14
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Cleanup code in pretyping/evarutilGravatar Matthieu Sozeau2014-05-08
* Fix performance problem with unification in presence of universes (bug #3302)...Gravatar Matthieu Sozeau2014-05-08
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Made Pre_env.lazy_val opaque.Gravatar Pierre-Marie Pédrot2014-02-11
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
* Using Map.smartmap whenever deemed useful.Gravatar Pierre-Marie Pédrot2014-01-29
* STM: additional fix for STM + vm_computeGravatar Enrico Tassi2014-01-07
* Removing useless meta-related functions.Gravatar Pierre-Marie Pédrot2013-12-03
* Better heuristic for name generation backward compatibility. We fallbackGravatar Pierre-Marie Pédrot2013-11-30
* Tentative fix to recover fresh name generation as it was beforeGravatar Pierre-Marie Pédrot2013-11-30
* Factoring: is_section_variable.Gravatar Arnaud Spiwack2013-11-25
* Less partial applications in Vars, as well as better memory allocation.Gravatar ppedrot2013-11-06
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
* push_rel_context: do not rename section variables.Gravatar aspiwack2013-11-02
* A newly introduced variable inside a named context is no longer α-renamed.Gravatar aspiwack2013-11-02
* Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.Gravatar ppedrot2013-10-29
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Optimizing evar filters. It seems to cost quite a lot in unification,Gravatar ppedrot2013-10-22
* Small code cleaning in Evarutil.Gravatar ppedrot2013-10-08
* Removing useless evar code.Gravatar ppedrot2013-10-06
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Removing almost all new_untyped_evar, and a bunch of Evd.add.Gravatar ppedrot2013-09-18
* Optimizing some evar_maps manipulation. In particular, using a [map] insteadGravatar ppedrot2013-09-05
* Partly replacing list-based access functions in Evd. This is stillGravatar ppedrot2013-09-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 12:16:55 +0000