From 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 Oct 2006 15:40:31 +0000
Subject: Correction de deux cas où les types inductifs n'étaient pas comparés
 vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug
 #1242)

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

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b2c37f7e6f..badf8796ef 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -497,12 +497,12 @@ let rec adjust_local_defs loc = function
   | [], [] -> []
   | _ -> raise NotAdjustable
 
-let check_and_adjust_constructor ind cstrs = function 
+let check_and_adjust_constructor env ind cstrs = function 
   | PatVar _ as pat -> pat
   | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
-      if ind' = ind then
+      if Closure.mind_equiv env ind' ind then
 	(* Check the constructor has the right number of args *)
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
@@ -1129,7 +1129,7 @@ let first_clause_irrefutable env = function
   | eqn::mat -> List.for_all (irrefutable env) eqn.patterns
   | _ -> false
 
-let group_equations pb mind current cstrs mat =
+let group_equations pb ind current cstrs mat =
   let mat =
     if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
   let brs = Array.create (Array.length cstrs) [] in
@@ -1139,7 +1139,7 @@ let group_equations pb mind current cstrs mat =
       (fun eqn () ->
 	 let rest = remove_current_pattern eqn in
 	 let pat = current_pattern eqn in
-	 match check_and_adjust_constructor mind cstrs pat with 
+	 match check_and_adjust_constructor pb.env ind cstrs pat with 
 	   | PatVar (_,name) -> 
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
-- 
cgit v1.2.3