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

5 files changed, 23 insertions, 26 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2f6eeba1d..3ce312533 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -517,14 +517,8 @@ let map_decl_arity f g = function
   | RegularArity a -> RegularArity (f a)
   | TemplateArity a -> TemplateArity (g a)
 
-let subst_rel_declaration sub = function
-  | LocalAssum (id,t) as x ->
-     let t' = subst_mps sub t in
-     if t == t' then x else LocalAssum (id,t')
-  | LocalDef (id,c,t) as x ->
-     let c' = subst_mps sub c in
-     let t' = subst_mps sub t in
-     if c == c' && t == t' then x else LocalDef (id,c',t')
+let subst_rel_declaration sub =
+  Term.map_rel_decl (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index f11fa5a7a..566df673c 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   let nhyps = List.length hyps in
   let rec check k index = function
     | [] -> ()
-    | LocalDef (_,_,_) :: hyps -> check k (index+1) hyps
+    | LocalDef _ :: hyps -> check k (index+1) hyps
     | _::hyps ->
         match whd_betadeltaiota env lpar.(k) with
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
@@ -376,8 +376,9 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
   let auxntyp = 1 in
   let specif = lookup_mind_specif env mi in
   let env' =
-    push_rel (LocalAssum (Anonymous,
-                          hnf_prod_applist env (type_of_inductive env (specif,u)) lpar)) env in
+    let decl = LocalAssum (Anonymous,
+                           hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in
+    push_rel decl env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 948012421..5e2e14f7f 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -634,8 +634,9 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind specif env =
-     push_rel (LocalAssum (Anonymous,
-		           hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar)) env
+     let decl = LocalAssum (Anonymous,
+		            hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+     push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
   let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
diff --git a/checker/term.ml b/checker/term.ml
index 181d292ad..56cc9cdc2 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -227,19 +227,19 @@ let rel_context_nhyps hyps =
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
-let map_rel_context f l =
-  let map_decl = function
-    | LocalAssum (n, typ) as decl ->
-       let typ' = f typ in
-       if typ' == typ then decl else
-         LocalAssum (n, typ')
-    | LocalDef (n, body, typ) as decl ->
-       let body' = f body in
-       let typ' = f typ in
-       if body' == body && typ' == typ then decl else
-         LocalDef (n, body', typ')
-  in
-    List.smartmap map_decl l
+let map_rel_decl f = function
+  | LocalAssum (n, typ) as decl ->
+     let typ' = f typ in
+     if typ' == typ then decl else
+       LocalAssum (n, typ')
+  | LocalDef (n, body, typ) as decl ->
+     let body' = f body in
+     let typ' = f typ in
+     if body' == body && typ' == typ then decl else
+       LocalDef (n, body', typ')
+
+let map_rel_context f =
+  List.smartmap (map_rel_decl f)
 
 let extended_rel_list n hyps =
   let rec reln l p = function
diff --git a/checker/term.mli b/checker/term.mli
index d6455e23f..0af83e05d 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -35,6 +35,7 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
 val compose_lam : (name * constr) list -> constr -> constr