aboutsummaryrefslogtreecommitdiff
path: root/kernel/sign.mli
diff options
context:
space:
mode:
authorfilliatr2000-01-28 23:51:42 +0000
committerfilliatr2000-01-28 23:51:42 +0000
commite521ccb7d16b7e2192a0c0d6bc046534a4466848 (patch)
tree1616a21eb4cb88bef2fcae0830d666bec2e02ab0 /kernel/sign.mli
parentbd23886243736ba75a584c475b7da521571c646d (diff)
documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@288 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/sign.mli')
-rw-r--r--kernel/sign.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 3a8f8a47a5..82d71fd4cb 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -9,7 +9,7 @@ open Term
(* Signatures of named variables. *)
-type 'a signature (* = identifier list * 'a list*)
+type 'a signature (* = [identifier list * 'a list] *)
val nil_sign : 'a signature
val add_sign : (identifier * 'a) -> 'a signature -> 'a signature