diff options
| -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 |