diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2ee8ed02f9..9ab4c64cda 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) |