Checker: get rid of code handling section variables

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

1 files changed, 1 insertions, 9 deletions

diff --git a/checker/term.ml b/checker/term.ml
index a3c9225f5..371889436 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -209,12 +209,6 @@ let subst1 lam = substl [lam]
 (*     Type of assumptions and contexts                                    *)
 (***************************************************************************)
 
-type named_declaration = Id.t * 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
-
 let empty_rel_context = []
 let rel_context_length = List.length
 let rel_context_nhyps hyps =
@@ -225,7 +219,7 @@ let rel_context_nhyps hyps =
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
-let map_context f l =
+let map_rel_context f l =
   let map_decl (n, body_o, typ as decl) =
     let body_o' = Option.smartmap f body_o in
     let typ' = f typ in
@@ -234,8 +228,6 @@ let map_context f l =
   in
     List.smartmap map_decl l
 
-let map_rel_context = map_context
-
 let extended_rel_list n hyps =
   let rec reln l p = function
     | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps