aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* Using appropriate lambda decomposition function counting let-ins whenGravatar Hugo Herbelin2015-10-18
* Fix inference of return clause raising a type error.Gravatar Matthieu Sozeau2015-10-09
* Univs: fix bug #4161.Gravatar Matthieu Sozeau2015-10-08
* Documenting the code when preference is given to expansion of defaultGravatar Hugo Herbelin2015-09-08
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Fixing first part of bug #3210 (inference of pattern-matching returnGravatar Hugo Herbelin2015-02-27
* Fixing #4001 (missing type constraints when building return clause of match).Gravatar Hugo Herbelin2015-02-10
* Update headers.Gravatar Maxime Dénès2015-01-12
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Fixing wrong evar_map in return clause inference, revealed by 48509b611.Gravatar Hugo Herbelin2014-12-08
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
* Fixing an evar leak in pattern-matching compilation (#3758).Gravatar Hugo Herbelin2014-10-22
* When facing problem ?id = ?id' in resolution of return predicate,Gravatar Hugo Herbelin2014-10-17
* Make use of unfolded primitive projections when elaborating match on aGravatar Matthieu Sozeau2014-10-15
* Added support for several impossible cases in compilation of "match".Gravatar Hugo Herbelin2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
* 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
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* An old typo which was preventing example #3537 to work the same as itGravatar Hugo Herbelin2014-09-12
* 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 bug #3584, elaborating pattern-matching on primitive records to theGravatar Matthieu Sozeau2014-09-06
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* Fix program cases and inversion tactic to correctly record universe constraints.Gravatar Matthieu Sozeau2014-06-24
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Refresh some universes in cases.ml as they might appear in the term.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-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
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Fix test-suite/success/evars.v.Gravatar Arnaud Spiwack2013-12-06
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Fix compilation of pattern matching wrt variables: alias.Gravatar aspiwack2013-11-02
* Fix the compilation of pattern matching wrt to variables.Gravatar aspiwack2013-11-02
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Fixing a source of evars leak, revealed by contrib QuicksortComplexityGravatar herbelin2013-05-11
* Uniformization: isevars -> evdref/sigma/evdGravatar herbelin2013-05-09
* Fix wrong computation of dependency signature in cases raising an uncaught ex...Gravatar msozeau2013-04-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:39:29 +0000