aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
Commit message (Expand)AuthorAge
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* New approach to deal with evar-evar unification problems in differentGravatar Hugo Herbelin2014-12-04
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Experimentally applying eager evar substitution at the same time asGravatar Hugo Herbelin2014-11-04
* Removing dead code from Evd.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.diff function.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.merge function.Gravatar Pierre-Marie Pédrot2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* 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
* Adding a tactic which fails if one of the goals under focus is dependent in a...Gravatar Hugo Herbelin2014-10-13
* 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
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Exporting apply_subfilter from Evd.ml.Gravatar Hugo Herbelin2014-09-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* When building on-the-fly elimination principles, set the predicates universe ...Gravatar Matthieu Sozeau2014-06-29
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar 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 many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* Useless instantiation function exported in Evd.Gravatar Pierre-Marie Pédrot2013-11-30
* Removing Evd.undefined_evars.Gravatar ppedrot2013-10-28
* Removing useless filter allocation in evar construction.Gravatar ppedrot2013-10-27
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 15:22:53 +0000