From 56c88d763b0cf636a740f531bd7d734426769d7d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 Apr 2013 16:04:56 +0000
Subject: Checker: regroup all vo-related types in cic.mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/check.ml         |   4 +-
 checker/check_stat.ml    |   1 +
 checker/checker.ml       |   2 +-
 checker/cic.mli          | 331 +++++++++++++++++++++++++++++++++++++++++++++++
 checker/closure.ml       |   3 +-
 checker/closure.mli      |   2 +-
 checker/declarations.ml  | 206 +----------------------------
 checker/declarations.mli | 191 +--------------------------
 checker/environ.ml       |   1 +
 checker/environ.mli      |  33 ++---
 checker/indtypes.ml      |   1 +
 checker/indtypes.mli     |   3 +-
 checker/inductive.ml     |   1 +
 checker/inductive.mli    |   3 +-
 checker/mod_checking.ml  |   1 +
 checker/mod_checking.mli |   2 +-
 checker/modops.ml        |   1 +
 checker/modops.mli       |   3 +-
 checker/reduction.ml     |   1 +
 checker/reduction.mli    |   1 +
 checker/safe_typing.ml   |   1 +
 checker/safe_typing.mli  |   4 +-
 checker/subtyping.ml     |   1 +
 checker/subtyping.mli    |   4 +-
 checker/term.ml          |  70 +---------
 checker/term.mli         |  52 +-------
 checker/type_errors.ml   |   1 +
 checker/type_errors.mli  |   2 +-
 checker/typeops.ml       |   1 +
 checker/typeops.mli      |   3 +-
 kernel/term.mli          |   4 +-
 31 files changed, 387 insertions(+), 547 deletions(-)
 create mode 100644 checker/cic.mli

diff --git a/checker/check.ml b/checker/check.ml
index 1b9fd07013..7ac15393a8 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -56,7 +56,7 @@ type library_t = {
   library_name : compilation_unit_name;
   library_filename : CUnix.physical_path;
   library_compiled : Safe_typing.compiled_library;
-  library_opaques : Term.constr array;
+  library_opaques : Cic.constr array;
   library_deps : (compilation_unit_name * Digest.t) array;
   library_digest : Digest.t }
 
@@ -314,7 +314,7 @@ let intern_from_file (dir, f) =
       let ch = with_magic_number_check raw_intern_library f in
       let (md:library_disk) = System.marshal_in f ch in
       let (digest:Digest.t) = System.marshal_in f ch in
-      let (table:Term.constr array) = System.marshal_in f ch in
+      let (table:Cic.constr array) = System.marshal_in f ch in
       (* Verification of the final checksum *)
       let pos = pos_in ch in
       let (checksum:Digest.t) = System.marshal_in f ch in
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 3176a4307f..62d5ac0648 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Names
+open Cic
 open Declarations
 open Environ
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 6b76b6b32f..e981cf8fea 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -284,7 +284,7 @@ let parse_args argv =
   let rec parse = function
     | [] -> ()
     | "-impredicative-set" :: rem ->
-      set_engagement Declarations.ImpredicativeSet; parse rem
+      set_engagement Cic.ImpredicativeSet; parse rem
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
diff --git a/checker/cic.mli b/checker/cic.mli
new file mode 100644
index 0000000000..5c1345ba03
--- /dev/null
+++ b/checker/cic.mli
@@ -0,0 +1,331 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Type definitions for the Calculus of Inductive Constructions *)
+
+(** We regroup here the type definitions for structures of the Coq kernel
+    that are present in .vo files. Here is everything the Checker needs
+    to know about these structures for verifying a .vo. Note that this
+    isn't an exact copy of the kernel code :
+
+    - there isn't any abstraction here (see e.g. [constr] or [lazy_constr])
+    - some types are left undefined when they aren't used by the Checker
+    - some types have less constructors when the final constructors aren't
+      supposed to appear in .vo (see [REVERTcast] and [Direct]).
+
+    The following types are also described in a reified manner in values.ml,
+    for validating the layout of structures after de-marshalling. So:
+
+    IF YOU ADAPT THIS FILE, PLEASE MODIFY ACCORDINGLY values.ml !
+*)
+
+open Names
+
+(*************************************************************************)
+(** {4 From term.ml} *)
+
+(** {6 The sorts of CCI. } *)
+
+type contents = Pos | Null
+
+type sorts =
+  | Prop of contents       (** Prop and Set *)
+  | Type of Univ.universe  (** Type *)
+
+(** {6 The sorts family of CCI. } *)
+
+type sorts_family = InProp | InSet | InType
+
+(** {6 Useful types } *)
+
+(** {6 Existential variables } *)
+type existential_key = int
+
+(** {6 Existential variables } *)
+type metavariable = int
+
+(** {6 Case annotation } *)
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
+  | RegularStyle (** infer printing form from number of constructor *)
+type case_printing =
+  { ind_nargs : int; (** length of the arity of the inductive type *)
+    style     : case_style }
+
+(** the integer is the number of real args, needed for reduction *)
+type case_info =
+  { ci_ind        : inductive;
+    ci_npar       : int;
+    ci_cstr_ndecls : int array; (** number of real args of each constructor *)
+    ci_pp_info    : case_printing (** not interpreted by the kernel *)
+  }
+
+(** This defines the strategy to use for verifiying a Cast. *)
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast (* | REVERTcast *)
+
+(** {6 The type of constructions } *)
+
+(** [constr array] is an instance matching definitional [named_context] in
+    the same order (i.e. last argument first) *)
+type 'constr pexistential = existential_key * 'constr array
+type 'constr prec_declaration =
+    Name.t array * 'constr array * 'constr array
+type 'constr pfixpoint =
+    (int array * int) * 'constr prec_declaration
+type 'constr pcofixpoint =
+    int * 'constr prec_declaration
+
+type constr =
+  | Rel       of int
+  | Var       of Id.t
+  | Meta      of metavariable
+  | Evar      of constr pexistential
+  | Sort      of sorts
+  | Cast      of constr * cast_kind * constr
+  | Prod      of Name.t * constr * constr
+  | Lambda    of Name.t * constr * constr
+  | LetIn     of Name.t * constr * constr * constr
+  | App       of constr * constr array
+  | Const     of constant
+  | Ind       of inductive
+  | Construct of constructor
+  | Case      of case_info * constr * constr * constr array
+  | Fix       of constr pfixpoint
+  | CoFix     of constr pcofixpoint
+
+type existential = constr pexistential
+type rec_declaration = constr prec_declaration
+type fixpoint = constr pfixpoint
+type cofixpoint = constr pcofixpoint
+
+(** {6 Type of assumptions and contexts}  *)
+
+type named_declaration = Id.t * constr option * constr
+type rel_declaration = Name.t * constr option * constr
+
+type rel_context = rel_declaration list
+
+
+(*************************************************************************)
+(** {4 From sign.ml} *)
+
+type named_context = named_declaration list
+type section_context = named_context
+
+
+(*************************************************************************)
+(** {4 From mod_susbt.ml and lazyconstr.ml} *)
+
+(** {6 Substitutions} *)
+
+type delta_hint =
+  | Inline of int * constr option
+  | Equiv of kernel_name
+
+type delta_resolver = module_path MPmap.t * delta_hint KNmap.t
+
+type 'a umap_t = 'a MPmap.t * 'a MBImap.t
+type substitution = (module_path * delta_resolver) umap_t
+
+(** {6 Delayed constr} *)
+
+type 'a lazy_subst =
+  | LSval of 'a
+  | LSlazy of substitution list * 'a
+
+type constr_substituted = constr lazy_subst ref
+
+(** Nota : in coqtop, the [lazy_constr] type also have a [Direct]
+    constructor, but it shouldn't occur inside a .vo, so we ignore it *)
+
+type lazy_constr =
+  | Indirect of substitution list * DirPath.t * int
+(* | Direct of constr_substituted *)
+
+
+(*************************************************************************)
+(** {4 From declarations.mli} *)
+
+(** Some types unused in the checker, hence left undefined *)
+
+(** Bytecode *)
+type reloc_table
+type to_patch_substituted
+(** Native code *)
+type native_name
+(** Retroknowledge *)
+type action
+
+(** Engagements *)
+
+type engagement = ImpredicativeSet
+
+(** {6 Representation of constants (Definition/Axiom) } *)
+
+type polymorphic_arity = {
+  poly_param_levels : Univ.universe option list;
+  poly_level : Univ.universe;
+}
+
+type constant_type =
+  | NonPolymorphicType of constr
+  | PolymorphicArity of rel_context * polymorphic_arity
+
+(** Inlining level of parameters at functor applications.
+    This is ignored by the checker. *)
+
+type inline = int option
+
+(** A constant can have no body (axiom/parameter), or a
+    transparent body, or an opaque one *)
+
+type constant_def =
+  | Undef of inline
+  | Def of constr_substituted
+  | OpaqueDef of lazy_constr
+
+type constant_body = {
+    const_hyps : section_context; (** New: younger hyp at top *)
+    const_body : constant_def;
+    const_type : constant_type;
+    const_body_code : to_patch_substituted;
+    const_constraints : Univ.constraints;
+    const_native_name : native_name ref;
+    const_inline_code : bool }
+
+(** {6 Representation of mutual inductive types } *)
+
+type recarg =
+  | Norec
+  | Mrec of inductive
+  | Imbr of inductive
+
+type wf_paths = recarg Rtree.t
+
+type monomorphic_inductive_arity = {
+  mind_user_arity : constr;
+  mind_sort : sorts;
+}
+
+type inductive_arity =
+| Monomorphic of monomorphic_inductive_arity
+| Polymorphic of polymorphic_arity
+
+type one_inductive_body = {
+(** {8 Primitive datas } *)
+
+    mind_typename : Id.t; (** Name of the type: [Ii] *)
+
+    mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
+
+    mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
+
+    mind_consnames : Id.t array; (** Names of the constructors: [cij] *)
+
+    mind_user_lc : constr array;
+ (** Types of the constructors with parameters:  [forall params, Tij],
+     where the Ik are replaced by de Bruijn index in the
+     context I1:forall params, U1 ..  In:forall params, Un *)
+
+(** {8 Derived datas } *)
+
+    mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *)
+
+    mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *)
+
+    mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
+
+    mind_nf_lc : constr array; (** Head normalized constructor types so that their conclusion is atomic *)
+
+    mind_consnrealdecls : int array;
+ (** Length of the signature of the constructors (with let, w/o params)
+    (not used in the kernel) *)
+
+    mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
+
+(** {8 Datas for bytecode compilation } *)
+
+    mind_nb_constant : int; (** number of constant constructor *)
+
+    mind_nb_args : int; (** number of no constant constructor *)
+
+    mind_reloc_tbl : reloc_table;
+  }
+
+type mutual_inductive_body = {
+
+    mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
+
+    mind_record : bool;  (** Whether the inductive type has been declared as a record *)
+
+    mind_finite : bool;  (** Whether the type is inductive or coinductive *)
+
+    mind_ntypes : int;  (** Number of types in the block *)
+
+    mind_hyps : section_context;  (** Section hypotheses on which the block depends *)
+
+    mind_nparams : int;  (** Number of expected parameters *)
+
+    mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
+
+    mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
+
+    mind_constraints : Univ.constraints;  (** Universes constraints enforced by the inductive declaration *)
+
+(** {8 Data for native compilation } *)
+
+    mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
+  }
+
+(** {6 Modules: signature component specifications, module types, and
+  module declarations } *)
+
+type structure_field_body =
+  | SFBconst of constant_body
+  | SFBmind of mutual_inductive_body
+  | SFBmodule of module_body
+  | SFBmodtype of module_type_body
+
+and structure_body = (label * structure_field_body) list
+
+and struct_expr_body =
+  | SEBident of module_path
+  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
+  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
+  | SEBstruct of structure_body
+  | SEBwith of struct_expr_body * with_declaration_body
+
+and with_declaration_body =
+    With_module_body of Id.t list * module_path
+  | With_definition_body of  Id.t list * constant_body
+and module_body =
+    {  (** absolute path of the module *)
+      mod_mp : module_path;
+      (** Implementation *)
+      mod_expr : struct_expr_body option;
+      (** Signature *)
+      mod_type : struct_expr_body;
+      (** algebraic structure expression is kept
+	 if it's relevant for extraction  *)
+      mod_type_alg : struct_expr_body option;
+      (** set of all constraint in the module  *)
+      mod_constraints : Univ.constraints;
+      (** quotiented set of equivalent constant and inductive name  *)
+      mod_delta : delta_resolver;
+      mod_retroknowledge : action list}
+
+and module_type_body =
+    {
+      (** Path of the module type *)
+      typ_mp : module_path;
+      typ_expr : struct_expr_body;
+      (** algebraic structure expression is kept
+	 if it's relevant for extraction  *)
+      typ_expr_alg : struct_expr_body option ;
+      typ_constraints : Univ.constraints;
+      (** quotiented set of equivalent constant and inductive name  *)
+      typ_delta : delta_resolver}
diff --git a/checker/closure.ml b/checker/closure.ml
index 9677680e6e..45452874e2 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -8,8 +8,9 @@
 
 open Util
 open Pp
-open Term
 open Names
+open Cic
+open Term
 open Esubst
 open Environ
 
diff --git a/checker/closure.mli b/checker/closure.mli
index 443eeb6aa1..bee6b1bb84 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -9,7 +9,7 @@
 (*i*)
 open Pp
 open Names
-open Term
+open Cic
 open Esubst
 open Environ
 (*i*)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index cfaa2f5f73..42d49e83b8 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,45 +1,21 @@
 open Util
 open Names
+open Cic
 open Term
 open Validate
 
-(* Bytecode *)
-type values
-type reloc_table
-type to_patch_substituted
-(* Native code *)
-type native_name
-(*Retroknowledge *)
-type action
-type retroknowledge
-
-type engagement = ImpredicativeSet
 let val_eng = val_enum "eng" 1
 
-
-type polymorphic_arity = {
-  poly_param_levels : Univ.universe option list;
-  poly_level : Univ.universe;
-}
 let val_pol_arity =
   val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
 
-type constant_type =
-  | NonPolymorphicType of constr
-  | PolymorphicArity of rel_context * polymorphic_arity
-
 let val_cst_type =
   val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
 
 (** Substitutions, code imported from kernel/mod_subst *)
 
-type delta_hint =
-  | Inline of int * constr option
-  | Equiv of kernel_name
-
-
 module Deltamap = struct
-  type t = module_path MPmap.t * delta_hint KNmap.t
+  type t = delta_resolver
   let empty = MPmap.empty, KNmap.empty
   let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km
   let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
@@ -55,12 +31,10 @@ module Deltamap = struct
   let join map1 map2 = fold add_mp add_kn map1 map2
 end
 
-type delta_resolver = Deltamap.t
-
 let empty_delta_resolver = Deltamap.empty
 
 module Umap = struct
-  type 'a t = 'a MPmap.t * 'a MBImap.t
+  type 'a t = 'a umap_t
   let empty = MPmap.empty, MBImap.empty
   let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
   let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2)
@@ -75,7 +49,6 @@ module Umap = struct
   let join map1 map2 = fold add_mp add_mbi map1 map2
 end
 
-type substitution = (module_path * delta_resolver) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
 let empty_subst = Umap.empty
@@ -324,13 +297,6 @@ let subst_mps sub c =
   if is_empty_subst sub then c
   else map_kn (subst_ind sub) (subst_con0 sub) c
 
-
-type 'a lazy_subst =
-  | LSval of 'a
-  | LSlazy of substitution list * 'a
-
-type 'a substituted = 'a lazy_subst ref
-
 let val_substituted val_a =
   val_ref
     (val_sum "constr_substituted" 0
@@ -482,19 +448,10 @@ let force_constr = force subst_mps
 
 let from_val c = ref (LSval c)
 
-type constr_substituted = constr substituted
-
 let val_cstr_subst = val_substituted val_constr
 
 let subst_constr_subst = subst_substituted
 
-(* Nota : in coqtop, the [lazy_constr] type also have a [Direct]
-   constructor, but it shouldn't occur inside a .vo, so we ignore it *)
-
-type lazy_constr =
-  | Indirect of substitution list * DirPath.t * int
-(* | Direct of constr_substituted *)
-
 let subst_lazy_constr sub = function
   | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
 
@@ -509,19 +466,6 @@ let force_lazy_constr = function
 let val_lazy_constr =
   val_sum "lazy_constr" 0 [|[|val_list val_subst;val_dp;val_int|]|]
 
-(** Inlining level of parameters at functor applications.
-    This is ignored by the checker. *)
-
-type inline = int option
-
-(** A constant can have no body (axiom/parameter), or a
-    transparent body, or an opaque one *)
-
-type constant_def =
-  | Undef of inline
-  | Def of constr_substituted
-  | OpaqueDef of lazy_constr
-
 let val_cst_def =
   val_sum "constant_def" 0
     [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|]
@@ -531,15 +475,6 @@ let subst_constant_def sub = function
   | Def c -> Def (subst_constr_subst sub c)
   | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
 
-type constant_body = {
-    const_hyps : section_context; (* New: younger hyp at top *)
-    const_body : constant_def;
-    const_type : constant_type;
-    const_body_code : to_patch_substituted;
-    const_constraints : Univ.constraints;
-    const_native_name : native_name ref;
-    const_inline_code : bool }
-
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
   | Def c -> Some (force_constr c)
@@ -569,10 +504,6 @@ let subst_rel_declaration sub (id,copt,t as x) =
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-type recarg =
-  | Norec
-  | Mrec of inductive
-  | Imbr of inductive
 let val_recarg = val_sum "recarg" 1 (* Norec *)
   [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|]
 
@@ -581,7 +512,6 @@ let subst_recarg sub r = match r with
   | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in
       if kn==kn' then r else Imbr (kn',i)
 
-type wf_paths = recarg Rtree.t
 let val_wfp = val_rec_sum "wf_paths" 0
   (fun val_wfp ->
     [|[|val_int;val_int|]; (* Rtree.Param *)
@@ -611,110 +541,17 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
    with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
 *)
 
-type monomorphic_inductive_arity = {
-  mind_user_arity : constr;
-  mind_sort : sorts;
-}
 let val_mono_ind_arity =
   val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|]
 
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
 let val_ind_arity = val_sum "inductive_arity" 0
   [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
 
-type one_inductive_body = {
-
-(* Primitive datas *)
-
- (* Name of the type: [Ii] *)
-    mind_typename : Id.t;
-
- (* Arity context of [Ii] with parameters: [forall params, Ui] *)
-    mind_arity_ctxt : rel_context;
-
- (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *)
-    mind_arity : inductive_arity;
-
- (* Names of the constructors: [cij] *)
-    mind_consnames : Id.t array;
-
- (* Types of the constructors with parameters: [forall params, Tij],
-    where the Ik are replaced by de Bruijn index in the context
-    I1:forall params, U1 ..  In:forall params, Un *)
-    mind_user_lc : constr array;
-
-(* Derived datas *)
-
- (* Number of expected real arguments of the type (no let, no params) *)
-    mind_nrealargs : int;
-
- (* Length of realargs context (with let, no params) *)
-    mind_nrealargs_ctxt : int;
-
- (* List of allowed elimination sorts *)
-    mind_kelim : sorts_family list;
-
- (* Head normalized constructor types so that their conclusion is atomic *)
-    mind_nf_lc : constr array;
-
- (* Length of the signature of the constructors (with let, w/o params) *)
-    mind_consnrealdecls : int array;
-
- (* Signature of recursive arguments in the constructors *)
-    mind_recargs : wf_paths;
-
-(* Datas for bytecode compilation *)
-
- (* number of constant constructor *)
-    mind_nb_constant : int;
-
- (* number of no constant constructor *)
-    mind_nb_args : int;
-
-    mind_reloc_tbl :  reloc_table;
-  }
-
 let val_one_ind = val_tuple ~name:"one_inductive_body"
   [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
     val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int;
     val_wfp;val_int;val_int;no_val|]
 
-
-type mutual_inductive_body = {
-
-  (* The component of the mutual inductive block *)
-    mind_packets : one_inductive_body array;
-
-  (* Whether the inductive type has been declared as a record *)
-    mind_record : bool;
-
-  (* Whether the type is inductive or coinductive *)
-    mind_finite : bool;
-
-  (* Number of types in the block *)
-    mind_ntypes : int;
-
-  (* Section hypotheses on which the block depends *)
-    mind_hyps : section_context;
-
-  (* Number of expected parameters *)
-    mind_nparams : int;
-
-  (* Number of recursively uniform (i.e. ordinary) parameters *)
-    mind_nparams_rec : int;
-
-  (* The context of parameters (includes let-in declaration) *)
-    mind_params_ctxt : rel_context;
-
-  (* Universes constraints enforced by the inductive declaration *)
-    mind_constraints : Univ.constraints;
-
-  (* Data for native compilation *)
-    mind_native_name : native_name ref;
-
-  }
 let val_ind_pack = val_tuple ~name:"mutual_inductive_body"
   [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
     val_int; val_int; val_rctxt;val_cstrs;no_val|]
@@ -772,43 +609,6 @@ let subst_mind sub mib =
 
 (* Modules *)
 
-(* Whenever you change these types, please do update the validation
-   functions below *)
-type structure_field_body =
-  | SFBconst of constant_body
-  | SFBmind of mutual_inductive_body
-  | SFBmodule of module_body
-  | SFBmodtype of module_type_body
-
-and structure_body = (label * structure_field_body) list
-
-and struct_expr_body =
-  | SEBident of module_path
-  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
-  | SEBstruct of structure_body
-  | SEBwith of struct_expr_body * with_declaration_body
-
-and with_declaration_body =
-    With_module_body of Id.t list * module_path
-  | With_definition_body of  Id.t list * constant_body
-
-and module_body =
-    { mod_mp : module_path;
-      mod_expr : struct_expr_body option; 
-      mod_type : struct_expr_body;
-      mod_type_alg : struct_expr_body option;
-      mod_constraints : Univ.constraints;
-      mod_delta : delta_resolver;
-      mod_retroknowledge : action list}
-
-and module_type_body =
-    { typ_mp : module_path;
-      typ_expr : struct_expr_body;
-      typ_expr_alg : struct_expr_body option ;
-      typ_constraints : Univ.constraints;
-      typ_delta :delta_resolver}
-
 (* the validation functions: *)
 let rec val_sfb o = val_sum "struct_field_body" 0
   [|[|val_cb|];       (* SFBconst *)
diff --git a/checker/declarations.mli b/checker/declarations.mli
index cc3123ca7d..af38ab0fba 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -1,60 +1,12 @@
 open Names
-open Term
+open Cic
 
-(* Bytecode *)
-type values
-type reloc_table
-type to_patch_substituted
-(* Native code *)
-type native_name
-(*Retroknowledge *)
-type action
-type retroknowledge
-
-(* Engagements *)
-
-type engagement = ImpredicativeSet
-
-(* Constants *)
-
-type polymorphic_arity = {
-  poly_param_levels : Univ.universe option list;
-  poly_level : Univ.universe;
-}
-
-type constant_type =
-  | NonPolymorphicType of constr
-  | PolymorphicArity of rel_context * polymorphic_arity
-
-type constr_substituted
 val force_constr : constr_substituted -> constr
 val from_val : constr -> constr_substituted
 
-type lazy_constr
-
 val indirect_opaque_access : (DirPath.t -> int -> constr) ref
 
-(** Inlining level of parameters at functor applications.
-    This is ignored by the checker. *)
-
-type inline = int option
-
-(** A constant can have no body (axiom/parameter), or a
-    transparent body, or an opaque one *)
-
-type constant_def =
-  | Undef of inline
-  | Def of constr_substituted
-  | OpaqueDef of lazy_constr
-
-type constant_body = {
-    const_hyps : section_context; (* New: younger hyp at top *)
-    const_body : constant_def;
-    const_type : constant_type;
-    const_body_code : to_patch_substituted;
-    const_constraints : Univ.constraints;
-    const_native_name : native_name ref;
-    const_inline_code : bool }
+(** Constant_body *)
 
 val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
@@ -62,154 +14,15 @@ val is_opaque : constant_body -> bool
 
 (* Mutual inductives *)
 
-type recarg =
-  | Norec
-  | Mrec of inductive
-  | Imbr of inductive
-
-type wf_paths = recarg Rtree.t
-
 val mk_norec : wf_paths
 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
 
-type monomorphic_inductive_arity = {
-  mind_user_arity : constr;
-  mind_sort : sorts;
-}
-
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
-
-type one_inductive_body = {
-
-(* Primitive datas *)
-
- (* Name of the type: [Ii] *)
-    mind_typename : Id.t;
-
- (* Arity context of [Ii] with parameters: [forall params, Ui] *)
-    mind_arity_ctxt : rel_context;
-
- (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *)
-    mind_arity : inductive_arity;
-
- (* Names of the constructors: [cij] *)
-    mind_consnames : Id.t array;
-
- (* Types of the constructors with parameters: [forall params, Tij],
-    where the Ik are replaced by de Bruijn index in the context
-    I1:forall params, U1 ..  In:forall params, Un *)
-    mind_user_lc : constr array;
-
-(* Derived datas *)
-
- (* Number of expected real arguments of the type (no let, no params) *)
-    mind_nrealargs : int;
-
- (* Length of realargs context (with let, no params) *)
-    mind_nrealargs_ctxt : int;
-
- (* List of allowed elimination sorts *)
-    mind_kelim : sorts_family list;
-
- (* Head normalized constructor types so that their conclusion is atomic *)
-    mind_nf_lc : constr array;
-
- (* Length of the signature of the constructors (with let, w/o params) *)
-    mind_consnrealdecls : int array;
-
- (* Signature of recursive arguments in the constructors *)
-    mind_recargs : wf_paths;
-
-(* Datas for bytecode compilation *)
-
- (* number of constant constructor *)
-    mind_nb_constant : int;
-
- (* number of no constant constructor *)
-    mind_nb_args : int;
-
-    mind_reloc_tbl :  reloc_table;
-  }
-
-type mutual_inductive_body = {
-
-  (* The component of the mutual inductive block *)
-    mind_packets : one_inductive_body array;
-
-  (* Whether the inductive type has been declared as a record *)
-    mind_record : bool;
-
-  (* Whether the type is inductive or coinductive *)
-    mind_finite : bool;
-
-  (* Number of types in the block *)
-    mind_ntypes : int;
-
-  (* Section hypotheses on which the block depends *)
-    mind_hyps : section_context;
-
-  (* Number of expected parameters *)
-    mind_nparams : int;
-
-  (* Number of recursively uniform (i.e. ordinary) parameters *)
-    mind_nparams_rec : int;
-
-  (* The context of parameters (includes let-in declaration) *)
-    mind_params_ctxt : rel_context;
-
-  (* Universes constraints enforced by the inductive declaration *)
-    mind_constraints : Univ.constraints;
-
-  (* Data for native compilation *)
-    mind_native_name : native_name ref;
-
-  }
-
 (* Modules *)
 
-type substitution
-type delta_resolver
 val empty_delta_resolver : delta_resolver
 
-type structure_field_body =
-  | SFBconst of constant_body
-  | SFBmind of mutual_inductive_body
-  | SFBmodule of module_body
-  | SFBmodtype of module_type_body
-
-and structure_body = (label * structure_field_body) list
-
-and struct_expr_body =
-  | SEBident of module_path
-  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
-  | SEBstruct of structure_body
-  | SEBwith of struct_expr_body * with_declaration_body
-
-and with_declaration_body =
-    With_module_body of Id.t list * module_path
-  | With_definition_body of  Id.t list * constant_body
-
-and module_body =
-    { mod_mp : module_path;
-      mod_expr : struct_expr_body option; 
-      mod_type : struct_expr_body;
-      mod_type_alg : struct_expr_body option;
-      mod_constraints : Univ.constraints;
-      mod_delta : delta_resolver;
-      mod_retroknowledge : action list}
-
-and module_type_body =
-    { typ_mp : module_path;
-      typ_expr : struct_expr_body;
-      typ_expr_alg : struct_expr_body option ;
-      typ_constraints : Univ.constraints;
-      typ_delta :delta_resolver}
-
 (* Substitutions *)
 
 type 'a subst_fun = substitution -> 'a -> 'a
diff --git a/checker/environ.ml b/checker/environ.ml
index 0b475ad490..c64495d41a 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -2,6 +2,7 @@ open Errors
 open Util
 open Names
 open Univ
+open Cic
 open Term
 open Declarations
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 095d93ae57..4165f0bcf7 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -1,17 +1,18 @@
 open Names
-open Term
+open Cic
+
 
 (* Environments *)
 
 type globals = {
-  env_constants : Declarations.constant_body Cmap_env.t;
-  env_inductives : Declarations.mutual_inductive_body Mindmap_env.t;
+  env_constants : constant_body Cmap_env.t;
+  env_inductives : mutual_inductive_body Mindmap_env.t;
   env_inductives_eq : kernel_name KNmap.t;
-  env_modules : Declarations.module_body MPmap.t;
-  env_modtypes : Declarations.module_type_body MPmap.t}
+  env_modules : module_body MPmap.t;
+  env_modtypes : module_type_body MPmap.t}
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : Declarations.engagement option;
+  env_engagement : engagement option;
 }
 type env = {
   env_globals : globals;
@@ -23,8 +24,8 @@ type env = {
 val empty_env : env
 
 (* Engagement *)
-val engagement : env -> Declarations.engagement option
-val set_engagement : Declarations.engagement -> env -> env
+val engagement : env -> Cic.engagement option
+val set_engagement : Cic.engagement -> env -> env
 
 (* Digests *)
 val add_digest : env -> DirPath.t -> Digest.t -> env
@@ -48,8 +49,8 @@ val universes : env -> Univ.universes
 val add_constraints : Univ.constraints -> env -> env
 
 (* Constants *)
-val lookup_constant : constant -> env -> Declarations.constant_body
-val add_constant : constant -> Declarations.constant_body -> env -> env
+val lookup_constant : constant -> env -> Cic.constant_body
+val add_constant : constant -> Cic.constant_body -> env -> env
 type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> constant -> constr
@@ -59,16 +60,16 @@ val evaluable_constant : constant -> env -> bool
 val mind_equiv : env -> inductive -> inductive -> bool
 
 val lookup_mind :
-  mutual_inductive -> env -> Declarations.mutual_inductive_body
+  mutual_inductive -> env -> Cic.mutual_inductive_body
 
 val add_mind :
-  mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
+  mutual_inductive -> Cic.mutual_inductive_body -> env -> env
 
 (* Modules *)
 val add_modtype :
-  module_path -> Declarations.module_type_body -> env -> env
+  module_path -> Cic.module_type_body -> env -> env
 val shallow_add_module :
-  module_path -> Declarations.module_body -> env -> env
+  module_path -> Cic.module_body -> env -> env
 val shallow_remove_module : module_path -> env -> env
-val lookup_module : module_path -> env -> Declarations.module_body
-val lookup_modtype : module_path -> env -> Declarations.module_type_body
+val lookup_module : module_path -> env -> Cic.module_body
+val lookup_modtype : module_path -> env -> Cic.module_type_body
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 8f93ff0be8..69e16386eb 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Univ
+open Cic
 open Term
 open Inductive
 open Reduction
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index 5c032a0ca2..0029eb652b 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -9,9 +9,8 @@
 (*i*)
 open Names
 open Univ
-open Term
+open Cic
 open Typeops
-open Declarations
 open Environ
 (*i*)
 
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 5fdca0fab4..ac9bf415c5 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Univ
+open Cic
 open Term
 open Reduction
 open Type_errors
diff --git a/checker/inductive.mli b/checker/inductive.mli
index d0040e3db7..0e9b9ccf34 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -8,8 +8,7 @@
 
 (*i*)
 open Names
-open Term
-open Declarations
+open Cic
 open Environ
 (*i*)
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ebe44997da..089414f633 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -3,6 +3,7 @@ open Pp
 open Errors
 open Util
 open Names
+open Cic
 open Term
 open Reduction
 open Typeops
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index a88afd7b3e..9425a6e3ac 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val check_module : Environ.env -> Names.module_path -> Declarations.module_body -> unit
+val check_module : Environ.env -> Names.module_path -> Cic.module_body -> unit
diff --git a/checker/modops.ml b/checker/modops.ml
index 13e436a5ea..20f330812b 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Pp
 open Names
+open Cic
 open Term
 open Declarations
 (*i*)
diff --git a/checker/modops.mli b/checker/modops.mli
index ef3bb6fd24..0b94edb545 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -9,8 +9,7 @@
 (*i*)
 open Names
 open Univ
-open Term
-open Declarations
+open Cic
 open Environ
 (*i*)
 
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 57e39f9cec..53a12295e1 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -8,6 +8,7 @@
 
 open Errors
 open Util
+open Cic
 open Term
 open Univ
 open Closure
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 2f6e5c3b79..915805d26b 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Cic
 open Term
 open Environ
 (*i*)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 492f5bc20e..2ccaad3e96 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -9,6 +9,7 @@
 open Pp
 open Errors
 open Util
+open Cic
 open Names
 open Declarations
 open Environ
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index a5f014935d..6a77089710 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -8,7 +8,7 @@
 
 (*i*)
 open Names
-open Term
+open Cic
 open Environ
 (*i*)
 
@@ -17,7 +17,7 @@ val get_env : unit -> env
 (* exporting and importing modules *)
 type compiled_library
 
-val set_engagement : Declarations.engagement -> unit
+val set_engagement : engagement -> unit
 val import         :
   CUnix.physical_path -> compiled_library -> constr array -> Digest.t -> unit
 val unsafe_import  :
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index d0d18c68ce..609918495d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Univ
+open Cic
 open Term
 open Declarations
 open Environ
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index 121e37542c..e0ca4a5075 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -7,9 +7,7 @@
 (************************************************************************)
 
 (*i*)
-open Univ
-open Term
-open Declarations
+open Cic
 open Environ
 (*i*)
 
diff --git a/checker/term.ml b/checker/term.ml
index bdbc7f8ec1..937b27ca0a 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -15,25 +15,8 @@ open Univ
 open Esubst
 open Validate
 
-(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
-
-type existential_key = int
-type metavariable = int
-
-(* This defines the strategy to use for verifiying a Cast *)
-
-(* This defines Cases annotations *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle |
-  RegularStyle
-type case_printing =
-  { ind_nargs : int; (* length of the arity of the inductive type *)
-    style     : case_style }
-type case_info =
-  { ci_ind         : inductive;
-    ci_npar        : int;
-    ci_cstr_ndecls : int array; (* number of pattern var of each constructor *)
-    ci_pp_info     : case_printing (* not interpreted by the kernel *)
-  }
+open Cic
+
 let val_ci =
   let val_cstyle = val_enum "case_style" 5 in
   let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in
@@ -41,14 +24,6 @@ let val_ci =
 
 (* Sorts. *)
 
-type contents = Pos | Null
-
-type sorts =
-  | Prop of contents                      (* proposition types *)
-  | Type of universe
-
-type sorts_family = InProp | InSet | InType
-
 let family_of_sort = function
   | Prop Null -> InProp
   | Prop Pos -> InSet
@@ -61,16 +36,6 @@ let val_sortfam = val_enum "sorts_family" 3
 (*       Constructions as implemented                               *)
 (********************************************************************)
 
-(* [constr array] is an instance matching definitional [named_context] in
-   the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
-type 'constr prec_declaration =
-    name array * 'constr array * 'constr array
-type 'constr pfixpoint =
-    (int array * int) * 'constr prec_declaration
-type 'constr pcofixpoint =
-    int * 'constr prec_declaration
-
 let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|]
 let val_prec f =
   val_tuple ~name:"prec_declaration"
@@ -80,30 +45,11 @@ let val_fix f =
     [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|]
 let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|]
 
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast
 let val_cast = val_enum "cast_kind" 3
 
 (*s*******************************************************************)
 (* The type of constructions *)
 
-type constr =
-  | Rel       of int
-  | Var       of Id.t
-  | Meta      of metavariable
-  | Evar      of constr pexistential
-  | Sort      of sorts
-  | Cast      of constr * cast_kind * constr
-  | Prod      of name * constr * constr
-  | Lambda    of name * constr * constr
-  | LetIn     of name * constr * constr * constr
-  | App       of constr * constr array
-  | Const     of constant
-  | Ind       of inductive
-  | Construct of constructor
-  | Case      of case_info * constr * constr * constr array
-  | Fix       of constr pfixpoint
-  | CoFix     of constr pcofixpoint
-
 let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
   [|val_int|]; (* Rel *)
   [|val_id|]; (* Var *)
@@ -123,11 +69,6 @@ let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
   [|val_cofix val_constr|] (* CoFix *)
 |])
 
-type existential = constr pexistential
-type rec_declaration = constr prec_declaration
-type fixpoint = constr pfixpoint
-type cofixpoint = constr pcofixpoint
-
 
 let rec strip_outer_cast c = match c with
   | Cast (c,_,_) -> strip_outer_cast c
@@ -318,16 +259,9 @@ let val_rdecl =
 let val_nctxt = val_list val_ndecl
 let val_rctxt = val_list val_rdecl
 
-type named_declaration = Id.t * constr option * constr
-type rel_declaration = name * constr option * constr
-
-type named_context = named_declaration list
 let empty_named_context = []
 let fold_named_context f l ~init = List.fold_right f l init
 
-type section_context = named_context
-
-type rel_context = rel_declaration list
 let empty_rel_context = []
 let rel_context_length = List.length
 let rel_context_nhyps hyps =
diff --git a/checker/term.mli b/checker/term.mli
index cc9d5cf97f..4993e07182 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -1,50 +1,8 @@
 open Names
+open Cic
 
-type existential_key = int
-type metavariable = int
-type case_style =
-    LetStyle
-  | IfStyle
-  | LetPatternStyle
-  | MatchStyle
-  | RegularStyle
-type case_printing = { ind_nargs : int; style : case_style; }
-type case_info = {
-  ci_ind : inductive;
-  ci_npar : int;
-  ci_cstr_ndecls : int array;
-  ci_pp_info : case_printing;
-}
-type contents = Pos | Null
-type sorts = Prop of contents | Type of Univ.universe
-type sorts_family = InProp | InSet | InType
 val family_of_sort : sorts -> sorts_family
-type 'a pexistential = existential_key * 'a array
-type 'a prec_declaration = name array * 'a array * 'a array
-type 'a pfixpoint = (int array * int) * 'a prec_declaration
-type 'a pcofixpoint = int * 'a prec_declaration
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast
-type constr =
-    Rel of int
-  | Var of Id.t
-  | Meta of metavariable
-  | Evar of constr pexistential
-  | Sort of sorts
-  | Cast of constr * cast_kind * constr
-  | Prod of name * constr * constr
-  | Lambda of name * constr * constr
-  | LetIn of name * constr * constr * constr
-  | App of constr * constr array
-  | Const of constant
-  | Ind of inductive
-  | Construct of constructor
-  | Case of case_info * constr * constr * constr array
-  | Fix of constr pfixpoint
-  | CoFix of constr pcofixpoint
-type existential = constr pexistential
-type rec_declaration = constr prec_declaration
-type fixpoint = constr pfixpoint
-type cofixpoint = constr pcofixpoint
+
 val strip_outer_cast : constr -> constr
 val collapse_appl : constr -> constr
 val decompose_app : constr -> constr * constr list
@@ -71,14 +29,9 @@ val substnl : constr list -> int -> constr -> constr
 val substl : constr list -> constr -> constr
 val subst1 : constr -> constr -> constr
 
-type named_declaration = Id.t * constr option * constr
-type rel_declaration = name * constr option * constr
-type named_context = named_declaration list
 val empty_named_context : named_context
 val fold_named_context :
   (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
-type section_context = named_context
-type rel_context = rel_declaration list
 val empty_rel_context : rel_context
 val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
@@ -96,6 +49,7 @@ val decompose_prod_assum : constr -> rel_context * constr
 val decompose_prod_n_assum : int -> constr -> rel_context * constr
 
 type arity = rel_context * sorts
+
 val mkArity : arity -> constr
 val destArity : constr -> arity
 val isArity : constr -> bool
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index bcfc31c6ff..6cf814dce1 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Names
+open Cic
 open Term
 open Environ
 
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index c57b1556ac..bcd4360b3a 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -8,7 +8,7 @@
 
 (*i*)
 open Names
-open Term
+open Cic
 open Environ
 (*i*)
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index a5b110f9b2..3c6fa7c04b 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Univ
+open Cic
 open Term
 open Reduction
 open Type_errors
diff --git a/checker/typeops.mli b/checker/typeops.mli
index fc16c9ed05..5e71ec77f3 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -8,8 +8,7 @@
 
 (*i*)
 open Names
-open Term
-open Declarations
+open Cic
 open Environ
 (*i*)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index c5f23ae9c4..e585e66b71 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -95,7 +95,7 @@ val mkSet  : types
 val mkType : Univ.universe -> types
 
 
-(* This defines the strategy to use for verifiying a Cast *)
+(** This defines the strategy to use for verifiying a Cast *)
 type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
 
 (** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
@@ -331,7 +331,7 @@ val destFix : constr -> fixpoint
 val destCoFix : constr -> cofixpoint
 
 
-(** {6 Local } *)
+(** {6 Local context} *)
 (** A {e declaration} has the form [(name,body,type)]. It is either an
     {e assumption} if [body=None] or a {e definition} if
     [body=Some actualbody]. It is referred by {e name} if [na] is an
-- 
cgit v1.2.3