diff options
| author | barras | 2008-09-02 14:15:12 +0000 |
|---|---|---|
| committer | barras | 2008-09-02 14:15:12 +0000 |
| commit | 1d1e9fcd021cab1206376508516d84896f4d1570 (patch) | |
| tree | b1d40c10a89b1fb98bcaecdf83217ab4058d5156 | |
| parent | 307c7610df6389768848e574170da85f1ab2c8fe (diff) | |
[checker] basic conversion oracle: expand local vars first
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11345 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | checker/reduction.ml | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 49f05dafd2..c398f0a41d 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -195,6 +195,12 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true | FLOCKED -> assert false +let oracle_order fl1 fl2 = + match fl1,fl2 with + ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false + | _, ConstKey _ -> true + | _ -> false + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) @@ -247,6 +253,14 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = with NotConvertible -> (* else the oracle tells which constant is to be expanded *) let (app1,app2) = + if oracle_order fl1 fl2 then + match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> raise NotConvertible) + else match unfold_reference infos fl2 with | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) | None -> |