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 --- checker/closure.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'checker/closure.ml') diff --git a/checker/closure.ml b/checker/closure.ml index 054057d1f..27848efa7 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -376,7 +376,12 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -let mind_equiv_infos info = eq_ind +let mind_equiv_infos info = mind_equiv info.i_env + +let eq_table_key k1 k2 = + match k1,k2 with + | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2 + | _,_ -> k1=k2 let create mk_cl flgs env = { i_flags = flgs; -- cgit v1.2.3