diff options
Diffstat (limited to 'kernel/constant.mli')
| -rw-r--r-- | kernel/constant.mli | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/kernel/constant.mli b/kernel/constant.mli index 5c6fb0d139..4de51f8593 100644 --- a/kernel/constant.mli +++ b/kernel/constant.mli @@ -1,4 +1,20 @@ (* $Id$ *) -type constant +open Names +open Term + +type discharge_recipe + +type recipe = + | Cooked of constr + | Recipe of discharge_recipe + +type constant_body = { + const_kind : path_kind; + const_body : recipe ref option; + const_type : type_judgment; + mutable const_eval : ((int * constr) list * int * bool) option option; +} + +type constant_entry = section_path * constant_body |