aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
Commit message (Expand)AuthorAge
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
* Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \
| * | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | More efficient implementation of equality-up-to-universes in Universes.Gravatar Pierre-Marie Pédrot2015-11-26
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Refresh rigid universes as well, and in 8.4 compatibility mode,Gravatar Matthieu Sozeau2015-11-02
* | Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
* | Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
| * Fixing bug #4347: Not_found Exception with some Records.Gravatar Pierre-Marie Pédrot2015-09-26
|/
* Fix for a second avatar of bug #4234.Gravatar Pierre-Marie Pédrot2015-05-13
* Fixing bug #4234.Gravatar Pierre-Marie Pédrot2015-05-12
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Gravatar Arnaud Spiwack2015-02-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 15:19:35 +0000