1 files changed, 58 insertions, 3 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 8a03e1cda..9ea7e20f8 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -15,10 +15,11 @@ open Term
 open Sign
 (*i*)
 
-(* This module defines the types of global declarations. This includes
-   global constants/axioms and mutual inductive definitions *)
+(* This module defines the internal representation of global
+   declarations. This includes global constants/axioms, mutual
+   inductive definitions, modules and module types *)
 
-(*s Constants (internal representation) (Definition/Axiom) *)
+(*s Constants (Definition/Axiom) *)
 
 type constant_body = {
   const_hyps : section_context; (* New: younger hyp at top *)
@@ -27,6 +28,8 @@ type constant_body = {
   const_constraints : constraints;
   const_opaque : bool }
 
+val subst_const_body : substitution -> constant_body -> constant_body
+
 (*s Inductive types (internal representation with redundant
     information). *)
 
@@ -35,6 +38,8 @@ type recarg =
   | Mrec of int 
   | Imbr of inductive
 
+val subst_recarg : substitution -> recarg -> recarg
+
 type wf_paths = recarg Rtree.t
 
 val mk_norec : wf_paths
@@ -42,6 +47,8 @@ val mk_paths : recarg -> wf_paths list array -> wf_paths
 val dest_recarg : wf_paths -> recarg
 val dest_subterms : wf_paths -> wf_paths list array
 
+val subst_wf_paths : substitution -> wf_paths -> wf_paths
+
 (* [mind_typename] is the name of the inductive; [mind_arity] is
    the arity generalized over global parameters; [mind_lc] is the list
    of types of constructors generalized over global parameters and
@@ -70,3 +77,51 @@ type mutual_inductive_body = {
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option }
+
+
+val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
+
+
+(*s Modules: signature component specifications, module types, and
+  module declarations *)
+
+type specification_body = 
+  | SPBconst of constant_body
+  | SPBmind of mutual_inductive_body
+  | SPBmodule of module_specification_body
+  | SPBmodtype of module_type_body
+
+and module_signature_body = (label * specification_body) list
+
+and module_type_body = 
+  | MTBident of kernel_name
+  | MTBfunsig of mod_bound_id * module_type_body * module_type_body
+  | MTBsig of mod_self_id * module_signature_body
+
+and module_expr_body =
+  | MEBident of module_path
+  | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
+  | MEBstruct of mod_self_id * module_structure_body
+  | MEBapply of module_expr_body * module_expr_body
+      * constraints
+
+and module_specification_body = module_type_body * module_path option
+
+and structure_elem_body = 
+  | SEBconst of constant_body
+  | SEBmind of mutual_inductive_body
+  | SEBmodule of module_body
+  | SEBmodtype of module_type_body
+
+and module_structure_body = (label * structure_elem_body) list
+
+and module_body = 
+    { mod_expr : module_expr_body option;
+      mod_user_type : (module_type_body * constraints) option;
+      mod_type : module_type_body;
+      mod_equiv : module_path option }
+
+
+
+
+