diff options
| author | Vincent Laporte | 2019-10-11 12:45:53 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-16 09:25:24 +0000 |
| commit | e500c71e46e6ff252455b9698addedb101662994 (patch) | |
| tree | af48fa2d87132bdae316e76f07ff8a3c11d4d6bb /engine/univGen.mli | |
| parent | 5d82451d6d6f591ad81919d8e6529cee48474b9e (diff) | |
[engine] Remove UnivGen.global_of_constr
Diffstat (limited to 'engine/univGen.mli')
| -rw-r--r-- | engine/univGen.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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. |