diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-13 11:59:31 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-13 11:59:31 +0000 |
| commit | ede35d97c697fb52d7edc17556e9089c0eb8f5dc (patch) | |
| tree | 004c42568c65e1a31da5f789206bc41288f69370 /contrib/funind/indfun_common.mli | |
| parent | 9c8fdb79a0e43ae3d7bf7ed94c7dafad572fd61a (diff) | |
trying f
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10659 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/indfun_common.mli')
| -rw-r--r-- | contrib/funind/indfun_common.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli index 7da1d6f0b..dd7078f4c 100644 --- a/contrib/funind/indfun_common.mli +++ b/contrib/funind/indfun_common.mli @@ -1,6 +1,9 @@ open Names open Pp +(* This map is used to deal with debruijn linked indices. *) +module Link : Map.S with type key = int + (* The mk_?_id function build different name w.r.t. a function Each of their use is justified in the code |