From a1278112e8a613069bbfb9fa47bee2b9089efd4a Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Thu, 2 Mar 2017 11:07:56 -0500
Subject: use Utf8 from Coq library

---
 coq/ex/example-utf8.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'coq/ex')

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).
-- 
cgit v1.2.3