diff options
| author | herbelin | 2012-12-04 23:26:40 +0000 |
|---|---|---|
| committer | herbelin | 2012-12-04 23:26:40 +0000 |
| commit | 33d8b9d956e6e0a9f079751e670873e9c68d6683 (patch) | |
| tree | 0e88c513970e19163b70895ca9aff572398e4993 /test-suite/success | |
| parent | 5ece01c8d71e2fdf7a87de71c342445599e137a0 (diff) | |
Backtrack on activating scopes with type casts (was r15978).
IT happens that there are some other uses of casts, e.g. in nat_int de
MathClasses which uses a notation 0 for some class constructor zero,
and a cast (0:nat) to force this notation 0 to represent the instance
O in nat of the class of types having a zero (eventually, 0,
i.e. "zero nat O" and "O" are convertible but the information of being
a class instance is lost).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Scopes.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index e15ae838ad..43e3493c1e 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -20,4 +20,3 @@ Inductive U := A. Bind Scope u with U. Notation "'ε'" := A : u. Definition c := ε : U. -Check ε : U. |