aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/closure.ml19
-rw-r--r--kernel/closure.mli5
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/reduction.ml10
-rw-r--r--kernel/vconv.ml3
-rw-r--r--pretyping/cases.ml8
-rw-r--r--test-suite/modules/ind.v28
7 files changed, 53 insertions, 22 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6bdca4f8f..364475019 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -375,14 +375,17 @@ let defined_rels flags env =
(rel_context env) ~init:(0,[])
(* else (0,[])*)
-
-let rec mind_equiv info kn1 kn2 =
- kn1 = kn2 ||
- match (lookup_mind kn1 info.i_env).mind_equiv with
- Some kn1' -> mind_equiv info kn2 kn1'
- | None -> match (lookup_mind kn2 info.i_env).mind_equiv with
- Some kn2' -> mind_equiv info kn2' kn1
- | None -> false
+let rec mind_equiv env (kn1,i1) (kn2,i2) =
+ let rec equiv kn1 kn2 =
+ kn1 = kn2 ||
+ match (lookup_mind kn1 env).mind_equiv with
+ Some kn1' -> equiv kn2 kn1'
+ | None -> match (lookup_mind kn2 env).mind_equiv with
+ Some kn2' -> equiv kn2' kn1
+ | None -> false in
+ i1 = i2 && equiv kn1 kn2
+
+let mind_equiv_infos info = mind_equiv info.i_env
let create mk_cl flgs env =
{ i_flags = flgs;
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 88f9139e6..2a0c1f89e 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -179,8 +179,9 @@ val whd_stack :
(* [unfold_reference] unfolds references in a [fconstr] *)
val unfold_reference : clos_infos -> table_key -> fconstr option
-(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
-val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
+(* [mind_equiv] checks whether two inductive types are intentionally equal *)
+val mind_equiv : env -> inductive -> inductive -> bool
+val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
(************************************************************************)
(*i This is for lazy debug *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2e2bcafce..d62af2e5e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -364,7 +364,7 @@ let inductive_equiv env (kn1,i1) (kn2,i2) =
let check_case_info env indsp ci =
let (mib,mip) = lookup_mind_specif env indsp in
if
- (indsp <> ci.ci_ind) or
+ not (Closure.mind_equiv env indsp ci.ci_ind) or
(mib.mind_nparams <> ci.ci_npar) or
(mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5b69ac7b6..28176ecc5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -257,14 +257,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
(* Inductive types: MutInd MutConstruct Fix Cofix *)
- | (FInd (kn1,i1), FInd (kn2,i2)) ->
- if i1 = i2 && mind_equiv infos kn1 kn2
+ | (FInd ind1, FInd ind2) ->
+ if mind_equiv_infos infos ind1 ind2
then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
- | (FConstruct ((kn1,i1),j1), FConstruct ((kn2,i2),j2)) ->
- if i1 = i2 && j1 = j2 && mind_equiv infos kn1 kn2
+ | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
+ if j1 = j2 && mind_equiv_infos infos ind1 ind2
then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
@@ -317,7 +317,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
compare_stacks
(fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
- (fun (mind1,i1) (mind2,i2) -> i1=i2 && mind_equiv infos mind1 mind2)
+ (mind_equiv_infos infos)
lft1 stk1 lft2 stk2 cuniv
and convert_vect infos lft1 lft2 v1 v2 cuniv =
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 7115097e4..7c515735d 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -83,7 +83,8 @@ and conv_whd pb k whd1 whd2 cu =
and conv_atom pb k a1 stk1 a2 stk2 cu =
match a1, a2 with
| Aind (kn1,i1), Aind(kn2,i2) ->
- if i1 = i2 && mind_equiv !infos kn1 kn2 && compare_stack stk1 stk2 then
+ if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
+ then
conv_stack k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b2c37f7e6..badf8796e 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
diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v
index a4f9d3a28..a15f390a3 100644
--- a/test-suite/modules/ind.v
+++ b/test-suite/modules/ind.v
@@ -14,4 +14,30 @@ End M.
Module N := M.
-Check (N.f M.A). \ No newline at end of file
+Check (N.f M.A).
+
+(* Check use of equivalence on inductive types (bug #1242) *)
+
+ Module Type ASIG.
+ Inductive t : Set := a | b : t.
+ Definition f := fun x => match x with a => true | b => false end.
+ End ASIG.
+
+ Module Type BSIG.
+ Declare Module A : ASIG.
+ Definition f := fun x => match x with A.a => true | A.b => false end.
+ End BSIG.
+
+ Module C (A : ASIG) (B : BSIG with Module A:=A).
+
+ (* Check equivalence is considered in "case_info" *)
+ Lemma test : forall x, A.f x = B.f x.
+ intro x. unfold B.f, A.f.
+ destruct x; reflexivity.
+ Qed.
+
+ (* Check equivalence is considered in pattern-matching *)
+ Definition f (x : A.t) := match x with B.A.a => true | B.A.b => false end.
+
+ End C.
+