diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-05 15:40:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-05 15:40:31 +0000 |
| commit | 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b (patch) | |
| tree | 9aea1570bb1de6ccc8e306c8344d4aaaf6352b57 /pretyping/cases.ml | |
| parent | 3004d1c1d53a13c4ea34e1997367ad6e0b1c31eb (diff) | |
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
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |