aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.mli
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-05 11:03:20 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-05 11:03:20 +0000
commit1e485645ef6481a856e8a67477f186519fb8ec9d (patch)
treefe06414569b65ae325c474f55e831fe228a0c23c /kernel/cooking.mli
parentdfb48b895bb114e6eb49840d960268e18f8aaf0c (diff)
Lazy experimentale temporaire...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cooking.mli')
-rw-r--r--kernel/cooking.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 3cd03fc9a..1787478b9 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -32,7 +32,7 @@ type recipe = {
d_modlist : work_list }
val cook_constant :
- env -> recipe -> constr option * constr * constraints * bool
+ env -> recipe -> constr Lazy.t option * constr * constraints * bool
(*s Utility functions used in module [Discharge]. *)