diff options
| author | Pierre-Marie Pédrot | 2020-01-28 13:49:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-28 13:53:12 +0100 |
| commit | 25b85ec88a16de73b942564994b7798d8330f396 (patch) | |
| tree | d0b4014e53d498e9dca5b4acec04186ba4f48a9e /engine/univGen.ml | |
| parent | b105077dd42e34f19d0849620fec2837e84b4887 (diff) | |
Remove dead code in Globnames.
Diffstat (limited to 'engine/univGen.ml')
| -rw-r--r-- | engine/univGen.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/engine/univGen.ml b/engine/univGen.ml index 1fe09270ba..b270f9dc0b 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function (** Fresh universe polymorphic construction *) -open Globnames - let fresh_global_instance ?loc ?names env gr = let auctx = Environ.universes_of_global env gr in let u, ctx = fresh_instance_from ?loc auctx names in @@ -78,10 +76,6 @@ let constr_of_monomorphic_global gr = Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ str " would forget universes.") -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty |