diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-22 19:23:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-22 19:23:33 +0000 |
| commit | 39bc0059d2730961c48b99a007127804d9fe2122 (patch) | |
| tree | 808f6213c4f116ff39440143f04edefd16490777 /kernel/term.mli | |
| parent | 2c968766b5bb57041694782ae2ffcda82ea5fe38 (diff) | |
Remove specific hash-consing of Term.types (was unused anyway)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14488 85f007b7-540e-0410-9357-904b9bb8a0f7
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 aa9a55abc..2ec1bd9b9 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 |