Suite restructuration inductifs; changement nom module Constant en Declarations

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

3 files changed, 6 insertions, 20 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 36281359b..85bce776a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -3,7 +3,7 @@ open Util
 open Names
 open Generic
 open Term
-open Constant
+open Declarations
 open Inductive
 open Environ
 open Sign
@@ -220,23 +220,9 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
 let lift_tomatch n ((current,typ),info) =
   ((lift n current,lift_tomatch_type n typ),info)
 
-let substn_many_ind_instance cv depth mis = {
-  mis_sp = mis.mis_sp;
-  mis_mib = mis.mis_mib;
-  mis_tyi = mis.mis_tyi;
-  mis_args = Array.map (substn_many cv depth) mis.mis_args;
-  mis_mip = mis.mis_mip
-}
-
-let substn_many_ind_data cv depth (IndFamily (mis,params)) =
-  IndFamily (substn_many_ind_instance cv depth mis,
-	     List.map (substn_many cv depth) params)
-
 let substn_many_tomatch v depth = function
-  | IsInd (t,IndType (ind_data,realargs)) ->
-      IsInd (substn_many v depth t,
-	     IndType (substn_many_ind_data v depth ind_data,
-		      List.map (substn_many v depth) realargs))
+  | IsInd (t,indt) ->
+      IsInd (substn_many v depth t,substn_many_ind_type v depth indt)
   | NotInd t -> NotInd (substn_many v depth t)
 
 let subst_tomatch (depth,c) = substn_many_tomatch [|make_substituend c|] depth
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 9b5a02c6f..0d011fcce 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -7,7 +7,7 @@ open Names
 open Generic
 open Term
 open Inductive
-open Constant
+open Declarations
 open Environ
 open Lib
 open Classops
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 091c14a2e..34ffa2f95 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -116,9 +116,9 @@ let encode_inductive id =
   (indsp,constr_lengths)
 
 let sp_of_spi (refsp,tyi) =
-  let mip = Constant.mind_nth_type_packet (Global.lookup_mind refsp) tyi in
+  let mip = Declarations.mind_nth_type_packet (Global.lookup_mind refsp) tyi in
   let (pa,_,k) = repr_path refsp in 
-  make_path pa mip.Constant.mind_typename k
+  make_path pa mip.Declarations.mind_typename k
 
 (*
   let (_,mip) = mind_specif_of_mind_light spi in