From 28809ba4180b0421d5b0e97f9e92ba72e63bda7c Mon Sep 17 00:00:00 2001
From: soubiran
Date: Thu, 29 Apr 2010 16:28:45 +0000
Subject: After the approval of Bruno, here the patch for the checker. In
 checker: - delta_resolver inferred by the module system is checked through
 regular delta reduction steps - the old mind_equiv field of mutual_inductive
 is simulated through a special table in environ - small optimization, if the
 signature and the implementation of a module are physically equal (always
 happen for the toplevel module of a vo) then the checker checks only the
 signature. In kernel - in names i have added two special equality functions
 over constant and inductive names for the checker, so that the checker does
 not take in account the cannonical name inferred by the module system.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12977 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml  | 4 ++++
 kernel/names.mli | 7 +++++++
 2 files changed, 11 insertions(+)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index dfa73e95a1..463f47ca4c 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -416,3 +416,7 @@ let eq_id_key ik1 ik2 =
     ConstKey (_,kn1),
       ConstKey (_,kn2) -> kn1=kn2
     | a,b -> a=b
+
+let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2
+let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2
+let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2
diff --git a/kernel/names.mli b/kernel/names.mli
index 1c74fdee6d..74cebd22a8 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -229,3 +229,10 @@ type inv_rel_key = int (** index in the [rel_context] part of environment
 type id_key = inv_rel_key tableKey
 
 val eq_id_key : id_key -> id_key -> bool
+
+(*equalities on constant and inductive 
+  names for the checker*)
+
+val eq_con_chk : constant -> constant -> bool
+val eq_ind_chk : inductive -> inductive -> bool
+
-- 
cgit v1.2.3