aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
...
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
* Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\
* | Revert "Add support for generalization also on named variables in pattern-mat...Gravatar Hugo Herbelin2016-04-27
* | Revert "Add support for deep dependencies in variables within the recursive s...Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Gravatar Hugo Herbelin2016-04-27
* | Revert "Using existing names as a basis for the inner names of the pattern-ma...Gravatar Hugo Herbelin2016-04-27
* | Revert "Vers un filtrage profond ..."Gravatar Hugo Herbelin2016-04-27
* | Vers un filtrage profond ...Gravatar Hugo Herbelin2016-04-27
* | Using existing names as a basis for the inner names of the pattern-matching p...Gravatar Hugo Herbelin2016-04-27
* | Fixing a De Bruijn bug in computing return predicate by inversion.Gravatar Hugo Herbelin2016-04-27
* | Add support for deep dependencies in variables within the recursive structure.Gravatar Hugo Herbelin2016-04-27
* | Add support for generalization also on named variables in pattern-matchingGravatar Hugo Herbelin2016-04-27
| * Optimization in building a return clause by pattern-matching: do notGravatar Hugo Herbelin2016-04-27
* | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
|/
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 15:28:01 +0000