aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.mli
AgeCommit message (Expand)Author
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2015-02-24[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Arnaud Spiwack
2015-02-23Compensating 6fd763431 on postponing subtyping evar-evar problems.Hugo Herbelin
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-04New approach to deal with evar-evar unification problems in differentHugo Herbelin
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-04Experimentally applying eager evar substitution at the same time asHugo Herbelin
2014-10-27Removing dead code from Evd.Pierre-Marie Pédrot
2014-10-27Removing the Evd.diff function.Pierre-Marie Pédrot
2014-10-27Removing the Evd.merge function.Pierre-Marie Pédrot
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-16Refine: proper scoping of the future goals.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-13Adding a tactic which fails if one of the goals under focus is dependent in a...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-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-13Exporting apply_subfilter from Evd.ml.Hugo Herbelin
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-13Checking typability of evar instances. Using ";" to separate bindingsHugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-13Bettre pretty-printing of evar maps, avoids printing universe informationMatthieu Sozeau
2014-07-03When defining a monomorphic Program, do not allow arbitrary instantiationsMatthieu Sozeau
2014-06-29When building on-the-fly elimination principles, set the predicates universe ...Matthieu Sozeau
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-08- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Matthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06Find a more efficient fix for dealing with template universes:Matthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Restore reasonable performance by not allocating during universe checks,Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu 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 many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2013-11-30Useless instantiation function exported in Evd.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:30:16 +0000