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

1 files changed, 17 insertions, 16 deletions

diff --git a/checker/environ.mli b/checker/environ.mli
index 095d93ae5..4165f0bcf 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