aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Scopes.v
Commit message (Expand)AuthorAge
* Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
* Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
* Backtrack on activating scopes with type casts (was r15978).Gravatar herbelin2012-12-04
* Fixing test-suite: Scope.vGravatar ppedrot2012-11-21
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Backtracking on r14876 (fix for bug #2267): extra scopes might beGravatar herbelin2012-01-05
* Test l'interprétation des scopesGravatar herbelin2004-03-11