diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:15:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:15:57 +0000 |
| commit | 5fb9b0b82547eac276b5fb5d64a63396b557e3bc (patch) | |
| tree | 338e057f11321a00283aa68beece4173642b3b11 /kernel/reduction.ml | |
| parent | ad7bec4eacfc3255f7270feab55eca407ac8766c (diff) | |
Bug réduction suite modifs let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@750 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index d27935187..5ec58c167 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -791,32 +791,29 @@ and eqappr cv_pb infos appr1 appr2 = (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *) - | (FFlex (fl1,al1), FFlex (fl2,al2)) -> + | (FFlex fl1, FFlex fl2) -> convert_or (* try first intensional equality *) (bool_and_convert (fl1 = fl2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) - v1 v2))) + (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) (* else expand the second occurrence (arbitrary heuristic) *) (fun u -> - match search_frozen_value infos fl2 al2 with + match search_frozen_value infos fl2 with | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) u - | None -> (match search_frozen_value infos fl1 al1 with + | None -> (match search_frozen_value infos fl1 with | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 u | None -> raise NotConvertible)) (* only one constant, existential, defined var or defined rel *) - | (FFlex (fl1,al1), _) -> - (match search_frozen_value infos fl1 al1 with + | (FFlex fl1, _) -> + (match search_frozen_value infos fl1 with | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 | None -> fun _ -> raise NotConvertible) - | (_, FFlex (fl2,al2)) -> - (match search_frozen_value infos fl2 al2 with + | (_, FFlex fl2) -> + (match search_frozen_value infos fl2 with | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) | None -> fun _ -> raise NotConvertible) |