diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:40 +0000 |
| commit | 33d8b9d956e6e0a9f079751e670873e9c68d6683 (patch) | |
| tree | 0e88c513970e19163b70895ca9aff572398e4993 | |
| 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
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/Scopes.v | 1 |
2 files changed, 1 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2ee8ed02f..9ab4c64cd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1471,9 +1471,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | CSort (loc, s) -> GSort(loc,s) | CCast (loc, c1, c2) -> - let c2 = Miscops.map_cast_type (intern_type env) c2 in - let env' = set_scope env c2 in - GCast (loc,intern env' c1, c2) + GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2) and intern_type env = intern (set_type_scope env) diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index e15ae838a..43e3493c1 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. |