CLEANUP: Simplifying the changes done in "kernel/*"

...

...

...

...

...

...

...

...

...

...

...

...

...

...

8 files changed, 30 insertions, 55 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index dc98cc65d..4476fe524 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -245,10 +245,12 @@ and 'a infos = {
 let info_flags info = info.i_flags
 let info_env info = info.i_cache.i_env
 
+open Context.Named.Declaration
+
 let rec assoc_defined id = function
 | [] -> raise Not_found
-| Context.Named.Declaration.LocalAssum _ :: ctxt -> assoc_defined id ctxt
-| Context.Named.Declaration.LocalDef (id', c, _) :: ctxt ->
+| LocalAssum _ :: ctxt -> assoc_defined id ctxt
+| LocalDef (id', c, _) :: ctxt ->
   if Id.equal id id' then c else assoc_defined id ctxt
 
 let ref_value_cache ({i_cache = cache} as infos)  ref =
@@ -285,9 +287,10 @@ let defined_rels flags env =
   let ctx = rel_context env in
   let len = List.length ctx in
   let ans = Array.make len None in
+  let open Context.Rel.Declaration in
   let iter i = function
-    | Context.Rel.Declaration.LocalAssum _ -> ()
-    | Context.Rel.Declaration.LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b)
+    | LocalAssum _ -> ()
+    | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b)
   in
   let () = List.iteri iter ctx in
   ans
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d2106f860..86d786b09 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -203,9 +203,8 @@ let cook_constant env { from = cb; info } =
   let const_hyps =
     Context.Named.fold_outside (fun decl hyps ->
       let open Context.Named.Declaration in
-      let h = get_id decl in
-      List.filter (fun decl -> let id = get_id decl in
-                               not (Id.equal id h)) hyps)
+      List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl')))
+		  hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
     | RegularArity t ->
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index cfbb89f06..9d58f6615 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -190,8 +190,8 @@ and slot_for_fv env fv =
       begin match force_lazy_val nv with
       | None ->
          let open Context.Named in
-         let open Context.Named.Declaration in
-         fill_fv_cache nv id val_of_named idfun (lookup id env.env_named_context |> get_value)
+         let open Declaration in
+	 env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun
       | Some (v, _) -> v
       end
   | FVrel i ->
@@ -199,8 +199,8 @@ and slot_for_fv env fv =
       begin match force_lazy_val rv with
       | None ->
          let open Context.Rel in
-         let open Context.Rel.Declaration in
-	 fill_fv_cache rv i val_of_rel env_of_rel (lookup i env.env_rel_context |> get_value)
+         let open Declaration in
+	 env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
   | FVuniv_var idu ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index cb67135ad..a09a8b786 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -9,6 +9,7 @@
 open Declarations
 open Mod_subst
 open Util
+open Context.Rel.Declaration
 
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -87,18 +88,8 @@ let is_opaque cb = match cb.const_body with
 
 (** {7 Constant substitutions } *)
 
-let subst_rel_declaration sub x =
-  let open Context.Rel.Declaration in
-  match x with
-  | LocalAssum (id,t) ->
-     let t' = subst_mps sub t in
-     if t == t' then x
-     else LocalAssum (id,t')
-  | LocalDef (id,v,t) ->
-     let v' = subst_mps sub v in
-     let t' = subst_mps sub t in
-     if v == v' && t == t' then x
-     else LocalDef (id,v',t')
+let subst_rel_declaration sub =
+  map_constr (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
@@ -148,20 +139,8 @@ let subst_const_body sub cb =
     share internal fields (e.g. constr), and not the records
     themselves. But would it really bring substantial gains ? *)
 
-let hcons_rel_decl d =
-  let open Context.Rel.Declaration in
-  match d with
-  | LocalAssum (n,t) ->
-     let n' = Names.Name.hcons n
-     and t' = Term.hcons_types t in
-     if n' == n && t' == t then d
-     else LocalAssum (n',t')
-  | LocalDef (n,v,t) ->
-     let n' = Names.Name.hcons n
-     and v' = Term.hcons_constr v
-     and t' = Term.hcons_types t in
-     if n' == n && v' == v && t' == t then d
-     else LocalDef (n',v',t')
+let hcons_rel_decl =
+  map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1089dff92..d8493d9ba 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -27,6 +27,7 @@ open Term
 open Vars
 open Declarations
 open Pre_env
+open Context.Rel.Declaration
 
 (* The type of environments. *)
 
@@ -72,8 +73,7 @@ let lookup_rel n env =
   Context.Rel.lookup n env.env_rel_context
 
 let evaluable_rel n env =
-  let open Context.Rel.Declaration in
-  lookup_rel n env |> is_local_def
+  is_local_def (lookup_rel n env)
 
 let nb_rel env = env.env_nb_rel
 
@@ -82,7 +82,6 @@ let push_rel = push_rel
 let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let open Context.Rel.Declaration in
   let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
@@ -128,11 +127,13 @@ let eq_named_context_val c1 c2 =
 
 (* A local const is evaluable if it is defined  *)
 
+open Context.Named.Declaration
+
 let named_type id env =
-  lookup_named id env |> Context.Named.Declaration.get_type
+  get_type (lookup_named id env)
 
 let named_body id env =
-  lookup_named id env |> Context.Named.Declaration.get_value
+  get_value (lookup_named id env)
 
 let evaluable_named id env =
   match named_body id env with
@@ -417,7 +418,6 @@ let global_vars_set env constr =
    contained in the types of the needed variables. *)
 
 let really_needed env needed =
-  let open Context.Named.Declaration in
   Context.Named.fold_inside
     (fun need decl ->
       if Id.Set.mem (get_id decl) need then
@@ -436,7 +436,6 @@ let keep_hyps env needed =
   let really_needed = really_needed env needed in
   Context.Named.fold_outside
     (fun d nsign ->
-      let open Context.Named.Declaration in
       if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign
       else nsign)
     (named_context env)
@@ -487,7 +486,6 @@ let compile_constant_body = Cbytegen.compile_constant_body false
 exception Hyp_not_found
 
 let apply_to_hyp (ctxt,vals) id f =
-  let open Context.Named.Declaration in
   let rec aux rtail ctxt vals =
     match ctxt, vals with
     | d::ctxt, v::vals ->
@@ -501,7 +499,6 @@ let apply_to_hyp (ctxt,vals) id f =
   in aux [] ctxt vals
 
 let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
-  let open Context.Named.Declaration in
   let rec aux ctxt vals =
     match ctxt,vals with
     | d::ctxt, v::vals ->
@@ -516,7 +513,6 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   in aux ctxt vals
 
 let insert_after_hyp (ctxt,vals) id d check =
-  let open Context.Named.Declaration in
   let rec aux ctxt vals =
     match  ctxt, vals with
     | decl::ctxt', v::vals' ->
@@ -533,7 +529,6 @@ let insert_after_hyp (ctxt,vals) id d check =
 
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
-  let open Context.Named.Declaration in
   let rec remove_hyps ctxt vals = match ctxt, vals with
   | [], [] -> [], []
   | d :: rctxt, (nid, v) :: rvals ->
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index df95c93dc..7f4ba8ecb 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -74,8 +74,7 @@ let judge_of_type u =
 let judge_of_relative env n =
   try
     let open Context.Rel.Declaration in
-    let typ = get_type (lookup_rel n env) in
-    lift n typ
+    env |> lookup_rel n |> get_type |> lift n
   with Not_found ->
     error_unbound_rel env n
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca29d83f6..229508ea3 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -319,7 +319,7 @@ let is_correct_arity env c pj ind specif params =
           let () =
             try conv env a1 a1'
             with NotConvertible -> raise (LocalArity None) in
-          srec (push_rel (LocalAssum (na1,a1)) env) t ar' 
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
       (* The last Prod domain is the type of the scrutinee *)
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
 	 let env' = push_rel (LocalAssum (na1,a1)) env in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 47274a5cd..dabe905de 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1832,10 +1832,10 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
   auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
 
 and compile_rel env sigma univ auxdefs n =
-  let decl = Context.Rel.lookup n env.env_rel_context in
-  let n = Context.Rel.length env.env_rel_context - n in
-  let open Context.Rel.Declaration in
-  match decl with
+  let open Context.Rel in
+  let n = length env.env_rel_context - n in
+  let open Declaration in
+  match lookup n env.env_rel_context with
   | LocalDef (_,t,_) ->
       let code = lambda_of_constr env sigma t in
       let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in