From 11a12c1108358d3ceb6372f01ef9a79ff99b3a4c Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 13 Jul 2005 11:36:09 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7211 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 40ec74f53f..0882758576 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*)
-- 
cgit v1.2.3