diff options
| -rw-r--r-- | checker/closure.ml | 18 | ||||
| -rw-r--r-- | checker/closure.mli | 5 | ||||
| -rw-r--r-- | checker/reduction.ml | 8 | ||||
| -rw-r--r-- | test-suite/coqchk/univ.v | 13 |
4 files changed, 25 insertions, 19 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index bfba6c161..66e69f225 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -135,22 +135,16 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * instantiations (cbv or lazy) are. *) -type 'a tableKey = - | ConstKey of 'a - | VarKey of Id.t - | RelKey of int - type table_key = Constant.t puniverses tableKey + +let eq_pconstant_key (c,u) (c',u') = + eq_constant_key c c' && Univ.Instance.equal u u' + module KeyHash = struct type t = table_key - let equal k1 k2 = match k1, k2 with - | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 - && Univ.Instance.equal u1 u2 - | VarKey id1, VarKey id2 -> Id.equal id1 id2 - | RelKey i1, RelKey i2 -> Int.equal i1 i2 - | (ConstKey _ | VarKey _ | RelKey _), _ -> false + let equal = Names.eq_table_key eq_pconstant_key open Hashset.Combine @@ -201,8 +195,6 @@ let defined_rels flags env = let mind_equiv_infos info = mind_equiv info.i_env -let eq_table_key = KeyHash.equal - let create mk_cl flgs env = { i_flags = flgs; i_repr = mk_cl; diff --git a/checker/closure.mli b/checker/closure.mli index 4cf02ae2b..49b07f730 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -58,10 +58,6 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type 'a tableKey = - | ConstKey of 'a - | VarKey of Id.t - | RelKey of int type table_key = Constant.t puniverses tableKey @@ -162,7 +158,6 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (* [mind_equiv] checks whether two inductive types are intentionally equal *) val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool -val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) diff --git a/checker/reduction.ml b/checker/reduction.ml index 072dec63f..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 @@ -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 -> diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index 19eea94b1..fcd740927 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -46,3 +46,16 @@ Inductive constraint4 : (Type -> Type) -> Type := mk_constraint4 : let U1 := Type in let U2 := Type in constraint4 (fun x : U1 => (x : U2)). + +Module CMP_CON. + (* Comparison of opaque constants MUST be up to the universe graph. + See #6798. *) + Universe big. + + Polymorphic Lemma foo@{u} : Type@{big}. + Proof. exact Type@{u}. Qed. + + Universes U V. + + Definition yo : foo@{U} = foo@{V} := eq_refl. +End CMP_CON. |