diff options
| -rw-r--r-- | pretyping/evarutil.ml | 6 |
1 files changed, 0 insertions, 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) *) |