1 files changed, 29 insertions, 27 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f7f5e507..0059111c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,19 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Environ
 open Entries
 open Reduction
 open Inductive
 open Type_errors
+open Context.Rel.Declaration
 
 let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
 
@@ -37,7 +37,7 @@ let check_constraints cst env =
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env j =
-  match kind_of_term(whd_betadeltaiota env j.uj_type) with
+  match kind_of_term(whd_all env j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type env j
 
@@ -79,7 +79,7 @@ let judge_of_type u =
 
 let judge_of_relative env n =
   try
-    let (_,_,typ) = lookup_rel n env in
+    let typ = get_type (lookup_rel n env) in
     { uj_val  = mkRel n;
       uj_type = lift n typ }
   with Not_found ->
@@ -99,18 +99,20 @@ let judge_of_variable env id =
    variables of the current env.
    Order does not have to be checked assuming that all names are distinct *)
 let check_hyps_inclusion env c sign =
-  Context.fold_named_context
-    (fun (id,b1,ty1) () ->
+  Context.Named.fold_outside
+    (fun d1 () ->
+      let open Context.Named.Declaration in
+      let id = get_id d1 in
       try
-        let (_,b2,ty2) = lookup_named id env in
-        conv env ty2 ty1;
-        (match b2,b1 with
-        | None, None -> ()
-        | None, Some _ ->
+        let d2 = lookup_named id env in
+        conv env (get_type d2) (get_type d1);
+        (match d2,d1 with
+        | LocalAssum _, LocalAssum _ -> ()
+        | LocalAssum _, LocalDef _ ->
             (* This is wrong, because we don't know if the body is
                needed or not for typechecking: *) ()
-        | Some _, None -> raise NotConvertible
-        | Some b2, Some b1 -> conv env b2 b1);
+        | LocalDef _, LocalAssum _ -> raise NotConvertible
+        | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1);
       with Not_found | NotConvertible | Option.Heterogeneous ->
         error_reference_variables env id c)
     sign
@@ -125,9 +127,9 @@ let extract_level env p =
   match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
 
 let extract_context_levels env l =
-  let fold l (_, b, p) = match b with
-  | None -> extract_level env p :: l
-  | _ -> l
+  let fold l = function
+    | LocalAssum (_,p) -> extract_level env p :: l
+    | LocalDef _ -> l
   in
   List.fold_left fold [] l
 
@@ -135,7 +137,7 @@ let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
   match kind_of_term ccl with
   | Sort (Type u) ->
-     let ind, l = decompose_app (whd_betadeltaiota env c) in
+     let ind, l = decompose_app (whd_all env c) in
      if isInd ind && List.is_empty l then
        let mis = lookup_mind_specif env (fst (destInd ind)) in
        let nparams = Inductive.inductive_params mis in
@@ -231,7 +233,7 @@ let judge_of_apply env funj argjv =
 	{ uj_val  = mkApp (j_val funj, Array.map j_val argjv);
           uj_type = typ }
     | hj::restjl ->
-        (match kind_of_term (whd_betadeltaiota env typ) with
+        (match kind_of_term (whd_all env typ) with
           | Prod (_,c1,c2) ->
 	      (try
 		 let () = conv_leq false env hj.uj_type c1 in
@@ -459,13 +461,13 @@ let rec execute env cstr =
 
     | Lambda (name,c1,c2) ->
       let varj = execute_type env c1 in
-      let env1 = push_rel (name,None,varj.utj_val) env in
+      let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in
       let j' = execute env1 c2 in
         judge_of_abstraction env name varj j'
 
     | Prod (name,c1,c2) ->
       let varj = execute_type env c1 in
-      let env1 = push_rel (name,None,varj.utj_val) env in
+      let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in
       let varj' = execute_type env1 c2 in
 	judge_of_product env name varj varj'
 
@@ -473,7 +475,7 @@ let rec execute env cstr =
       let j1 = execute env c1 in
       let j2 = execute_type env c2 in
       let _ = judge_of_cast env j1 DEFAULTcast j2 in
-      let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
+      let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in
       let j' = execute env1 c3 in
         judge_of_letin env name j1 j2 j'
 
@@ -549,18 +551,18 @@ let infer_v env cv =
 (* Typing of several terms. *)
 
 let infer_local_decl env id = function
-  | LocalDef c ->
+  | LocalDefEntry c ->
       let j = infer env c in
-      (Name id, Some j.uj_val, j.uj_type)
-  | LocalAssum c ->
+      LocalDef (Name id, j.uj_val, j.uj_type)
+  | LocalAssumEntry c ->
       let j = infer env c in
-      (Name id, None, assumption_of_judgment env j)
+      LocalAssum (Name id, assumption_of_judgment env j)
 
 let infer_local_decls env decls =
   let rec inferec env = function
   | (id, d) :: l ->
       let (env, l) = inferec env l in
       let d = infer_local_decl env id d in
-	(push_rel d env, add_rel_decl d l)
-  | [] -> (env, empty_rel_context) in
+	(push_rel d env, Context.Rel.add d l)
+  | [] -> (env, Context.Rel.empty) in
   inferec env decls