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 1586adae7..7adb00da6 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -14,7 +14,7 @@ open Univ (** {6 Cooking the constants. } *) -type work_list = identifier array Cmap.t * identifier array Mindmap.t +type work_list = Id.t array Cmap.t * Id.t array Mindmap.t type recipe = { d_from : constant_body; |