diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-26 14:46:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-26 14:46:20 +0000 |
| commit | e7140d45b65e47dc195c0c5c8f21c9251b6f3814 (patch) | |
| tree | 44b9d6cdb394b3c10999150d18aa2b784550e758 /pretyping | |
| parent | 6aaf0c643b585b173f6de4d9eb01bcf08b9aaeb1 (diff) | |
Bug de contextes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1224 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f0b50aa0d..8dab70441 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -241,16 +241,20 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | IsFix (li1,(tys1,_,bds1)), IsFix (li2,(tys2,_,bds2)) -> + | IsFix (li1,(tys1,_,bds1 as recdef1)), IsFix (li2,(tys2,_,bds2)) -> li1=li2 & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) - & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2) + & (array_for_all2 + (evar_conv_x (push_rec_types recdef1 env) isevars CONV) + bds1 bds2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | IsCoFix (i1,(tys1,_,bds1)), IsCoFix (i2,(tys2,_,bds2)) -> + | IsCoFix (i1,(tys1,_,bds1 as recdef1)), IsCoFix (i2,(tys2,_,bds2)) -> i1=i2 & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) - & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2) + & (array_for_all2 + (evar_conv_x (push_rec_types recdef1 env) isevars CONV) + bds1 bds2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) | (IsMeta _ | IsXtra _ | IsLambda _), _ -> false |