diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-18 15:37:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-18 15:37:14 +0000 |
| commit | 1571830454cb842bfed718801755da6075c4a350 (patch) | |
| tree | c334c9403b46866f829bc949205b586c24aa5d59 /lib/rtree.ml | |
| parent | 3a501aec80ea400216f833cf2f30977f4ff826a3 (diff) | |
Documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8648 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/rtree.ml')
| -rw-r--r-- | lib/rtree.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/rtree.ml b/lib/rtree.ml index b76a69834..bc6555e75 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -11,11 +11,11 @@ (* 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 = |