From 33d8b9d956e6e0a9f079751e670873e9c68d6683 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 4 Dec 2012 23:26:40 +0000
Subject: 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
---
 interp/constrintern.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'interp')

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)
 
-- 
cgit v1.2.3