diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index cb782afac..33c6b0b08 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -369,11 +369,11 @@ val mkConstructU : constructor puniverses -> constr val mkConstructUi : (pinductive * int) -> constr [@@ocaml.deprecated "Alias for Constr"] val mkCase : case_info * constr * constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkCase"] val mkFix : fixpoint -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkFix"] val mkCoFix : cofixpoint -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkCoFix"] (** {6 Aliases} *) |