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

1 files changed, 3 insertions, 3 deletions

diff --git a/checker/term.ml b/checker/term.ml
index 8d65bbe17..c39491ab5 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -487,9 +487,9 @@ let compare_constr f t1 t2 =
           f h1 h2 & List.for_all2 f l1 l2
         else false
   | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
-  | Const c1, Const c2 -> eq_constant c1 c2
-  | Ind c1, Ind c2 -> c1 = c2
-  | Construct c1, Construct c2 -> c1 = c2
+  | Const c1, Const c2 -> eq_con_chk c1 c2
+  | Ind c1, Ind c2 -> eq_ind_chk c1 c2
+  | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
       f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
   | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->