diff options
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 97255dd49..4e508dc77 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open CErrors open Util open Cic @@ -54,7 +55,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of Names.projection * lift + | Zlproj of Names.Projection.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -142,7 +143,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> f fx1 fx2; cmp_rec a1 a2 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (Names.eq_con_chk + if not (Names.Constant.UserOrd.equal (Names.Projection.constant c1) (Names.Projection.constant c2)) then raise NotConvertible @@ -297,6 +298,11 @@ let oracle_order infos l2r k1 k2 = if Int.equal n1 n2 then l2r else n1 < n2 +let eq_table_key univ = + Names.eq_table_key (fun (c1,u1) (c2,u2) -> + Constant.UserOrd.equal c1 c2 && + Univ.Instance.check_eq univ u1 u2) + (* 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,[])) @@ -343,7 +349,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try (* try first intensional equality *) - if eq_table_key fl1 fl2 + if eq_table_key univ fl1 fl2 then convert_stacks univ infos lft1 lft2 v1 v2 else raise NotConvertible with NotConvertible -> |