From 26da42bee0b32c0f7316475e64ca2204c740efd2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 20 Apr 2018 17:06:20 +0200
Subject: Fix #6798: coqchk ignores ugraph when comparing constant instances

---
 checker/closure.ml   | 18 +++++-------------
 checker/closure.mli  |  5 -----
 checker/reduction.ml |  8 +++++++-
 3 files changed, 12 insertions(+), 19 deletions(-)

(limited to 'checker')

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 ->
-- 
cgit v1.2.3