diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /lib/rtree.ml | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'lib/rtree.ml')
| -rw-r--r-- | lib/rtree.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/rtree.ml b/lib/rtree.ml index 53cc372f..ab689be1 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.ml,v 1.2.8.1 2004/07/16 19:30:31 herbelin Exp $ i*) +(*i $Id: rtree.ml 8648 2006-03-18 15:37:14Z herbelin $ i*) (* Type of regular trees: - Param denotes tree variables (like de Bruijn indices) - - Node denotes the usual tree node, labelles with 'a + - Node denotes the usual tree node, labelled with 'a - Rec(j,v1..vn) introduces infinite tree. It denotes v(j+1) with parameters 0..n-1 replaced by Rec(0,v1..vn)..Rec(n-1,v1..vn) respectively. - Parameters n and higher denote parameters globals to the + Parameters n and higher denote parameters global to the current Rec node (as usual in de Bruijn binding system) *) type 'a t = |