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, 3 insertions, 49 deletions

diff --git a/checker/term.mli b/checker/term.mli
index cc9d5cf97..4993e0718 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