aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/example-tokens.v
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-13 10:27:43 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-13 10:27:43 +0000
commite6b44c882f85960893d2b3aa8995ad605a28b972 (patch)
tree0e1549e180cf3a003b683c7fd318e0dcf5afa104 /coq/example-tokens.v
parenta6ea9f91f82c216b9ce756b7323c456eeb80658c (diff)
Updated.
Diffstat (limited to 'coq/example-tokens.v')
-rw-r--r--coq/example-tokens.v6
1 files changed, 4 insertions, 2 deletions
diff --git a/coq/example-tokens.v b/coq/example-tokens.v
index b6ea2a29..fe3ab88f 100644
--- a/coq/example-tokens.v
+++ b/coq/example-tokens.v
@@ -1,9 +1,11 @@
(*
- Example uses of X-Symbol symbols in Coq.
+ Example uses of Unicode Tokens symbols in Coq.
See README.
Trac this at http://proofgeneral.inf.ed.ac.uk/trac/ticket/313
- Pierre Courtieu
+ Pierre Courtieu, David Aspinall.
+
+ Turn on with Proof-General → Quick Options → Display → Unicode Tokens
$Id$
*)