aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index fe8a888a6d..c8f6ea4a14 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -133,7 +133,6 @@ type cofixpoint = int * rec_declaration
term *)
val kind_of_term : constr -> (constr, types) kind_of_term
-val mk_constr : (constr, types) kind_of_term -> constr
(*s Term constructors. *)