diff options
| author | Maxime Dénès | 2017-11-15 08:48:33 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-15 08:48:33 +0100 |
| commit | 72f9bc46d6df56f8a5d28acbd6c3cfb544cefcb3 (patch) | |
| tree | 640407a38cc96645a66ccb7754ace80092fdfe22 /kernel | |
| parent | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff) | |
| parent | 6bd240fce21c172680a0cec5346b66e08c76418a (diff) | |
Merge PR #6045: [travis] [coq] Complete 4.06.0 support.
Diffstat (limited to 'kernel')
| -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 cb782aface..33c6b0b08d 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} *) |