diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-05 17:16:58 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-05 17:16:58 +0000 |
| commit | ef14e67d209edf4581223c6de4c38a79e4831940 (patch) | |
| tree | 7012a9b32a16a14b765c03e76e4f32415f55ec86 /kernel/esubst.mli | |
| parent | 8235d977028498a99d8c3c097f6fd2094298f3ff (diff) | |
Improved reduction machine with closure: should use less memory
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/esubst.mli')
| -rw-r--r-- | kernel/esubst.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 284c2f32e..cbb5c37cc 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -39,3 +39,4 @@ val subs_liftn: int -> 'a subs -> 'a subs val subs_shift_cons: int * 'a subs * 'a -> 'a subs val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union val is_subs_id: 'a subs -> bool +val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
\ No newline at end of file |