diff options
| author | Pierre-Marie Pédrot | 2019-10-29 14:03:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-29 14:03:06 +0100 |
| commit | e9dddcb2b5297f2e601a2e2d65a131ee5fde19e4 (patch) | |
| tree | 46ae8fcf9516ac84d0de44d2956d4ae661fc2f4f /engine | |
| parent | 5370e79c1128dd96a75e3c37569daa3fd98dcd86 (diff) | |
| parent | e500c71e46e6ff252455b9698addedb101662994 (diff) | |
Merge PR #10892: [engine] Remove UnivGen.global_of_constr
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univGen.ml | 8 | ||||
| -rw-r--r-- | engine/univGen.mli | 3 |
2 files changed, 0 insertions, 11 deletions
diff --git a/engine/univGen.ml b/engine/univGen.ml index b1ed3b2694..1fe09270ba 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -82,14 +82,6 @@ let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty | IsGlobal gr -> fresh_global_instance env gr -let global_of_constr c = - match kind c with - | Const (c, u) -> GlobRef.ConstRef c, u - | Ind (i, u) -> GlobRef.IndRef i, u - | Construct (c, u) -> GlobRef.ConstructRef c, u - | Var id -> GlobRef.VarRef id, Instance.empty - | _ -> raise Not_found - 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 1c8735bfa8..1b351c61c4 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -54,9 +54,6 @@ val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_const val fresh_universe_context_set_instance : ContextSet.t -> universe_level_subst * ContextSet.t -(** Raises [Not_found] if not a global reference. *) -val global_of_constr : constr -> GlobRef.t puniverses - (** Create a fresh global in the global environment, without side effects. BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. |