diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 8a2e892ef2..38fcebafa5 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -197,7 +197,7 @@ val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool (** Hash-consing *) -val hcons_names : unit -> +val hcons_names : (constant -> constant) * (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) * (name -> name) * (identifier -> identifier) |