aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-20 17:06:20 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-20 17:06:20 +0200
commit26da42bee0b32c0f7316475e64ca2204c740efd2 (patch)
tree2f9625fb70a68e33494090d470b11f8a7f3c4089 /checker
parent9a4ca53a3a021cb16de7706ec79a26e49f54de49 (diff)
Fix #6798: coqchk ignores ugraph when comparing constant instances
Diffstat (limited to 'checker')
-rw-r--r--checker/closure.ml18
-rw-r--r--checker/closure.mli5
-rw-r--r--checker/reduction.ml8
3 files changed, 12 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 ->