diff options
| author | Gaëtan Gilbert | 2020-01-29 11:34:43 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-29 11:34:43 +0100 |
| commit | f4163cb662983da2bd87a51b7bd1c6e5166b0d74 (patch) | |
| tree | c35c5b5acaf6bb28a949f31ad9f94e7e50ca3742 /engine | |
| parent | dd86f54cbe7b328b4514c49b8ce1a1c78819f094 (diff) | |
| parent | 25b85ec88a16de73b942564994b7798d8330f396 (diff) | |
Merge PR #11473: Remove dead code in Globnames.
Reviewed-by: SkySkimmer
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univGen.ml | 6 | ||||
| -rw-r--r-- | engine/univGen.mli | 3 |
2 files changed, 0 insertions, 9 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 diff --git a/engine/univGen.mli b/engine/univGen.mli index 1b351c61c4..bbde9d4e30 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor -> val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - (** Get fresh variables for the universe context. Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) val fresh_universe_context_set_instance : ContextSet.t -> |