Checker: reified encoding of .vo types in values.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 50 deletions

diff --git a/checker/term.ml b/checker/term.ml
index 937b27ca0..b52f08cfa 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -13,15 +13,9 @@ open Util
 open Names
 open Univ
 open Esubst
-open Validate
 
 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
-  val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
-
 (* Sorts. *)
 
 let family_of_sort = function
@@ -29,47 +23,10 @@ let family_of_sort = function
   | Prop Pos -> InSet
   | Type _ -> InType
 
-let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
-let val_sortfam = val_enum "sorts_family" 3
-
 (********************************************************************)
 (*       Constructions as implemented                               *)
 (********************************************************************)
 
-let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|]
-let val_prec f =
-  val_tuple ~name:"prec_declaration"
-    [|val_array val_name; val_array f; val_array f|]
-let val_fix f =
-  val_tuple ~name:"pfixpoint"
-    [|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|]
-
-let val_cast = val_enum "cast_kind" 3
-
-(*s*******************************************************************)
-(* The type of constructions *)
-
-let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
-  [|val_int|]; (* Rel *)
-  [|val_id|]; (* Var *)
-  [|val_int|]; (* Meta *)
-  [|val_evar val_constr|]; (* Evar *)
-  [|val_sort|]; (* Sort *)
-  [|val_constr;val_cast;val_constr|]; (* Cast *)
-  [|val_name;val_constr;val_constr|]; (* Prod *)
-  [|val_name;val_constr;val_constr|]; (* Lambda *)
-  [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
-  [|val_constr;val_array val_constr|]; (* App *)
-  [|val_con|]; (* Const *)
-  [|val_ind|]; (* Ind *)
-  [|val_cstr|]; (* Construct *)
-  [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
-  [|val_fix val_constr|]; (* Fix *)
-  [|val_cofix val_constr|] (* CoFix *)
-|])
-
-
 let rec strip_outer_cast c = match c with
   | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
@@ -252,13 +209,6 @@ let subst1 lam = substl [lam]
 (*     Type of assumptions and contexts                                    *)
 (***************************************************************************)
 
-let val_ndecl =
-  val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|]
-let val_rdecl =
-  val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
-let val_nctxt = val_list val_ndecl
-let val_rctxt = val_list val_rdecl
-
 let empty_named_context = []
 let fold_named_context f l ~init = List.fold_right f l init