From 494ef20fc93dbe7bf373f713284f08b034da9075 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 25 Nov 2013 12:27:16 +0100
Subject: Factoring: is_section_variable.

In 0c7a77, I inadvertantly re-defined an is_section_variable function.
---
 pretyping/evarutil.ml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3de63c9d40..08643a1d9a 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -330,12 +330,6 @@ let push_rel_context_to_named_context env typ =
     | Name id' when id_ord id id' = 0 -> None
     | Name id' -> Some id'
   in
-  let is_section_variable =
-    let global = Global.env () in
-    fun id ->
-      try ignore (Environ.lookup_named id global);true
-      with Not_found -> false
-  in
   (* move the rel context to a named context and extend the named instance *)
   (* with vars of the rel context *)
   (* We do keep the instances corresponding to local definition (see above) *)
-- 
cgit v1.2.3