diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index aa9a55abc0..2ec1bd9b96 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -626,16 +626,6 @@ val hash_constr : constr -> int (*********************************************************************) -val hcons_constr: - (constant -> constant) * - (mutual_inductive -> mutual_inductive) * - (dir_path -> dir_path) * - (name -> name) * - (identifier -> identifier) - -> - (constr -> constr) * - (types -> types) - val hcons1_constr : constr -> constr val hcons1_types : types -> types |