diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-13 11:36:09 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-13 11:36:09 +0000 |
| commit | 11a12c1108358d3ceb6372f01ef9a79ff99b3a4c (patch) | |
| tree | a77466cc80963aa0103de7f1a486cfb974ba2fa9 /kernel | |
| parent | 48d2f53aa6d051db60af5cab09a20f35bdf5c63b (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7211 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 40ec74f53..088275857 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -115,6 +115,7 @@ val stack_args_size : 'a stack -> int val app_stack : constr * constr stack -> constr val stack_tail : int -> 'a stack -> 'a stack val stack_nth : 'a stack -> int -> 'a +val zip_term : ('a -> constr) -> constr -> 'a stack -> constr (************************************************************************) (*s Lazy reduction. *) @@ -154,6 +155,8 @@ val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr +(* prevents a term from being evaluated *) +val set_norm : fconstr -> unit (* Global and local constant cache *) type clos_infos @@ -198,6 +201,5 @@ val kl : clos_infos -> fconstr -> constr val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr val optimise_closure : fconstr subs -> constr -> fconstr subs * constr -val set_norm : fconstr -> unit (* End of cbn debug section i*) |