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, 2 insertions, 68 deletions

diff --git a/checker/term.ml b/checker/term.ml
index bdbc7f8ec..937b27ca0 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 =