diff options
| -rw-r--r-- | coq/ex/example-utf8.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/coq/ex/example-utf8.v b/coq/ex/example-utf8.v index 4cba17c8..0f528f14 100644 --- a/coq/ex/example-utf8.v +++ b/coq/ex/example-utf8.v @@ -1,11 +1,6 @@ (* -*- coding: utf-8; -*- *) -(* utf8 notations: You can (re)use the version here, - or a compiled version distributed with Coq IDE: - Add LoadPath "/usr/lib/coq/ide". - Require Import utf8. -*) -Load "utf8". +Require Import Utf8. (* Printing of unicode notation, in *goals* *) Lemma test : ∀ A:Prop, A -> A. @@ -23,4 +18,4 @@ Qed. Check (fun (X:Set)(x:X) => x). (* Parsing of unicode notation here, printing in *response* *) -Check (∀A, A→A).
\ No newline at end of file +Check (∀A, A→A). |