From 0c260ba25423ec1c142296f19c3009fa0702819a Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 6 Jan 2010 10:24:41 +0000
Subject: Patch on subtyping check of opaque constants.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12631 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/subtyping.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 41f4c640ce..2a5f35f1a4 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -254,6 +254,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let con = make_con mp1 empty_dirpath l in
       let cst =
 	if cb2.const_opaque then
+	  (* In this case we compare opaque definitions, we need to bypass
+	     the opacity and do a delta step*)
 	  match cb2.const_body with
             | None -> cst
             | Some lc2 ->
@@ -262,8 +264,11 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		  | Some lc1 ->
 		      let c = Declarations.force lc1 in
 			begin
-			  match (kind_of_term c) with
-			      Const n ->
+			  match (kind_of_term c),(kind_of_term c2) with
+			      Const n1,Const n2 when (eq_constant n1 n2) -> c
+				(* c1 may have been strenghtened 
+				   we need to unfold it*)
+			    | Const n,_ ->
 				let cb = subst_const_body subst1
 				  (lookup_constant n env) in
 				  (match cb.const_opaque,
@@ -271,7 +276,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 				       | true, Some lc1 ->
 					   Declarations.force lc1
 				       | _,_ -> c)
-			    | _ -> c
+			    | _ ,_-> c
 			end
 		  | None -> mkConst con
 		in
-- 
cgit v1.2.3