From 9e6e6202c073fed0e2fc915d7f7e6ce927d55218 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 1 Oct 2000 13:20:02 +0000
Subject: Disparition du type oper mais nouveau type global_reference

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/class.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/class.ml b/pretyping/class.ml
index 21935be3c7..f9c36315b6 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -443,9 +443,9 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
 	if defined_in_sec sp sec_sp then 
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
-	  let id = Global.id_of_global (MutConstruct((newsp,i),j)) in
+	  let id = Global.id_of_global (ConstructRef ((newsp,i),j)) in
           (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p
 	else
 	  ((coe,coeinfo),s1,t1),
-	  Global.id_of_global (MutConstruct((sp,i),j)),
+	  Global.id_of_global (ConstructRef ((sp,i),j)),
 	  p
-- 
cgit v1.2.3