diff options
Diffstat (limited to 'library/globnames.mli')
| -rw-r--r-- | library/globnames.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/library/globnames.mli b/library/globnames.mli index 8acea5ef28..58e0efbc7a 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -34,7 +34,6 @@ val destConstructRef : GlobRef.t -> constructor val is_global : GlobRef.t -> constr -> bool [@@ocaml.deprecated "Use [Constr.isRefX] instead."] -val subst_constructor : substitution -> constructor -> constructor val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t |