aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness/psyntax.mli
diff options
context:
space:
mode:
authorherbelin2003-08-14 13:41:39 +0000
committerherbelin2003-08-14 13:41:39 +0000
commit4135e812a99fdfd7404fd354f31f286a4b4f005a (patch)
treefd831a1e14acfa8c3c9a63b625e11135413506e1 /contrib/correctness/psyntax.mli
parent8595888095feba842ebe880a91edbad170b0023a (diff)
Traducteur de correctness
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4275 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/psyntax.mli')
-rw-r--r--contrib/correctness/psyntax.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli
index dac571de55..0d3eb1bcb4 100644
--- a/contrib/correctness/psyntax.mli
+++ b/contrib/correctness/psyntax.mli
@@ -23,4 +23,3 @@ module Programs :
val type_v : constr_expr ml_type_v Gram.Entry.e
val type_c : constr_expr ml_type_c Gram.Entry.e
end
-