diff options
| author | Arnaud Spiwack | 2013-11-25 12:27:16 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-11-25 16:22:41 +0100 |
| commit | 494ef20fc93dbe7bf373f713284f08b034da9075 (patch) | |
| tree | 6f994c90c21b6a95fe09d33e94421e86e74047d9 | |
| parent | 619b04a80ac6b17d54ac9227cba2d597cbda00a9 (diff) | |
Factoring: is_section_variable.
In 0c7a77, I inadvertantly re-defined an is_section_variable function.
| -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) *) |