diff options
| author | David Aspinall | 2008-01-24 23:48:13 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-01-24 23:48:13 +0000 |
| commit | 36def03bb49b891a0c6eea80cac77a15e8c4686d (patch) | |
| tree | 7070bbd9a15f2c9a20451e24e14375d0e8e6d191 | |
| parent | 1fc7fc2d99f1db94bfbc518f1a0daa4ca3aa344c (diff) | |
Updated.
| -rw-r--r-- | coq/example-utf8.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/example-utf8.v b/coq/example-utf8.v index f6dfd3c6..555c7546 100644 --- a/coq/example-utf8.v +++ b/coq/example-utf8.v @@ -12,7 +12,7 @@ Lemma test : forall A:Prop, A -> A. auto. Qed. -(* Parsing of unicode notation, in *goals* *) +(* Parsing of unicode notation here, printing in *goals* *) Lemma test2 : ∀ A:Prop, A → A. intro. intro. @@ -22,5 +22,5 @@ Qed. (* Printing of unicode notation, in *response* *) Check (fun (X:Set)(x:X) => x). -(* Parsing of unicode notation, in *response* *) +(* Parsing of unicode notation here, printing in *response* *) Check (∀A, A→A).
\ No newline at end of file |