diff options
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 23b1f2534..db35031d9 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,7 +16,7 @@ open Univ (*s Cooking the constants. *) -type work_list = identifier array Cmap.t * identifier array KNmap.t +type work_list = identifier array Cmap.t * identifier array Mindmap.t type recipe = { d_from : constant_body; |