aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/past.mli
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-18 15:02:52 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-18 15:02:52 +0000
commita5cf61907148d79e5627930ae78bfb0a393b617d (patch)
tree193537fe267675eca3042d22e996aedd8c8ecd1e /contrib/correctness/past.mli
parent655b95012717f3b9fba714f591dfdb39d0174200 (diff)
retablissement de Correctness (pas encore teste' cependant)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3016 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/past.mli')
-rw-r--r--contrib/correctness/past.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 9919ee993..3c5a56c1d 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -23,7 +23,7 @@ type variable = identifier
type pattern =
| PatVar of identifier
- | PatConstruct of identifier * ((section_path * int) * int)
+ | PatConstruct of identifier * ((kernel_name * int) * int)
| PatAlias of pattern * identifier
| PatPair of pattern * pattern
| PatApp of pattern list