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, 0 insertions, 23 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index c64495d41..1485d6bf0 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -20,7 +20,6 @@ type stratification = {
 
 type env = {
     env_globals       : globals;
-    env_named_context : named_context;
     env_rel_context   : rel_context;
     env_stratification : stratification;
     env_imports : Digest.t MPmap.t }
@@ -32,7 +31,6 @@ let empty_env = {
     env_inductives_eq = KNmap.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
-  env_named_context = [];
   env_rel_context = [];
   env_stratification =
   { env_universes = Univ.initial_universes;
@@ -41,7 +39,6 @@ let empty_env = {
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
-let named_context env = env.env_named_context
 let rel_context env = env.env_rel_context
 
 let set_engagement c env =
@@ -78,26 +75,6 @@ let push_rec_types (lna,typarray,_) env =
   let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
-(* Named context *)
-
-let push_named d env =
-(*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
-  assert (env.env_rel_context = []); *)
-    { env with
-      env_named_context = d :: env.env_named_context }
-
-let lookup_named id env =
-  let rec lookup_named id = function
-    | (id',_,_ as decl) :: _ when id=id' -> decl
-    | _ :: sign -> lookup_named id sign
-    | [] -> raise Not_found in
-  lookup_named id env.env_named_context
-
-(* A local const is evaluable if it is defined  *)
-
-let named_type id env =
-  let (_,_,t) = lookup_named id env in t
-
 (* Universe constraints *)
 let add_constraints c env =
   if c == empty_constraint then