aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
Commit message (Expand)AuthorAge
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 16:10:29 +0000