aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-27Revert "Add support for generalization also on named variables in pattern-mat...Hugo Herbelin
2016-04-27Revert "Add support for deep dependencies in variables within the recursive s...Hugo Herbelin
2016-04-27Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Hugo Herbelin
2016-04-27Revert "Using existing names as a basis for the inner names of the pattern-ma...Hugo Herbelin
2016-04-27Revert "Vers un filtrage profond ..."Hugo Herbelin
2016-04-27Vers un filtrage profond ...Hugo Herbelin
2016-04-27Using existing names as a basis for the inner names of the pattern-matching p...Hugo Herbelin
2016-04-27Fixing a De Bruijn bug in computing return predicate by inversion.Hugo Herbelin
2016-04-27Add support for deep dependencies in variables within the recursive structure.Hugo Herbelin
2016-04-27Add support for generalization also on named variables in pattern-matchingHugo Herbelin
2016-04-27Optimization in building a return clause by pattern-matching: do notHugo Herbelin
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-05About building of substitutions from instances.Hugo Herbelin
2015-10-18Using appropriate lambda decomposition function counting let-ins whenHugo Herbelin
2015-10-09Fix inference of return clause raising a type error.Matthieu Sozeau
2015-10-08Univs: fix bug #4161.Matthieu Sozeau
2015-09-08Documenting the code when preference is given to expansion of defaultHugo Herbelin
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-02-27Fixing first part of bug #3210 (inference of pattern-matching returnHugo Herbelin
2015-02-10Fixing #4001 (missing type constraints when building return clause of match).Hugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-08Fixing wrong evar_map in return clause inference, revealed by 48509b611.Hugo Herbelin
2014-12-07Improved tracking of the origin of evars.Hugo Herbelin
2014-10-22Fixing an evar leak in pattern-matching compilation (#3758).Hugo Herbelin
2014-10-17When facing problem ?id = ?id' in resolution of return predicate,Hugo Herbelin
2014-10-15Make use of unfolded primitive projections when elaborating match on aMatthieu Sozeau
2014-10-13Added support for several impossible cases in compilation of "match".Hugo Herbelin
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-05A few improvements on pattern-matching compilation.Hugo Herbelin
2014-10-04A few Global.env removed.Hugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-12An old typo which was preventing example #3537 to work the same as itHugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
2014-06-24Fix program cases and inversion tactic to correctly record universe constraints.Matthieu Sozeau
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 21:38:42 +0000