diff options
| -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. |