diff options
Diffstat (limited to 'library/globnames.mli')
| -rw-r--r-- | library/globnames.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/library/globnames.mli b/library/globnames.mli index 02ac51fb1..af1f10ee4 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -72,6 +72,12 @@ module ExtRefOrdered : sig val compare : t -> t -> int end +type global_reference_or_constr = + | IsGlobal of global_reference + | IsConstr of constr + +val constr_of_global_or_constr : global_reference_or_constr -> constr + (** {6 Temporary function to brutally form kernel names from section paths } *) val encode_mind : dir_path -> identifier -> mutual_inductive |