aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/inference.out
Commit message (Expand)AuthorAge
* Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\
| * Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\
| * Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* | Adapting output test inference.v after c23f0cab6 (experimentingGravatar Hugo Herbelin2015-11-08
|/
* Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.Gravatar Maxime Dénès2015-06-24
* Do not display the status of monomorphic constants unless in universe-polymor...Gravatar Guillaume Melquiond2015-03-09
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
* Fixing output test-suite: since universe polymorphism, the Print commandGravatar Pierre-Marie Pédrot2014-05-08
* Fixing 2 output test-suites.Gravatar ppedrot2013-10-08
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* A small test for type inference (used to be a regression at some time).Gravatar herbelin2011-12-04