correspondance des records et noms de champs de records entre un module et sa signature

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 10 insertions, 36 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 238fd470f3..7f56101a4d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -60,10 +60,6 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
 (* appliquer le chemin de coercions p à hj *)
 
 let apply_coercion env p hj typ_cl =
-  if !compter then begin
-    nbpathc := !nbpathc +1; 
-    nbcoer := !nbcoer + (List.length p)
-  end;
   try 
     fst (List.fold_left
            (fun (ja,typ_cl) i -> 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 42af2bfe62..6917d67358 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -377,21 +377,16 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
 	 (new_isevar isevars env dloc (substl ks b)) :: ks)
       [] bs
   in
-  if (list_for_all2eq 
-	(fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
-	us2 us)
-    &
-    (list_for_all2eq 
-       (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
-       params1 params)
-    & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
-    & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
-  then
-    (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
-                              nbimplstruc:=!nbimplstruc+(List.length ks);true)
-            else true)
-  else false
-
+  (list_for_all2eq 
+     (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
+     us2 us)
+  &
+  (list_for_all2eq 
+     (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
+     params1 params)
+  & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
+  & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
+    
 let the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV  t1 t2
 let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2
  
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 49baf2ade5..fb11eb5587 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -238,7 +238,6 @@ let rec pretype tycon env isevars lvar = function
       anomaly "Found a pattern variable in a rawterm to type"
 	   
   | RHole (loc,k) ->
-      if !compter then nbimpl:=!nbimpl+1;
       (match tycon with
 	 | Some ty ->
 	     { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
@@ -892,7 +891,6 @@ let rec pretype tycon env isevars lvar = function
 (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
 and pretype_type valcon env isevars lvar = function
   | RHole loc ->
-      if !compter then nbimpl:=!nbimpl+1;
       (match valcon with
 	 | Some v ->
              let s =
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e2e574d7f7..4ea0da0a4a 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -20,14 +20,6 @@ open Libobject
 open Library
 open Classops
 
-let nbimpl = ref 0
-let nbpathc = ref 0
-let nbcoer = ref 0
-let nbstruc = ref 0
-let nbimplstruc = ref 0
-
-let compter = ref false
-
 (*s Une structure S est un type inductif non récursif à un seul
    constructeur (de nom par défaut Build_S) *)
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f758776de4..7989535b93 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -18,13 +18,6 @@ open Libobject
 open Library
 (*i*)
 
-val nbimpl : int ref
-val nbpathc : int ref
-val nbcoer : int ref
-val nbstruc : int ref
-val nbimplstruc : int ref
-val compter : bool ref
-
 type struc_typ = {
   s_CONST : identifier; 
   s_PARAM : int;