aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-12 16:33:35 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-12 16:33:35 +0000
commite35ad3c1aa44aa8f0a7309ad343cae7d8634d555 (patch)
treeb33b1071fa08461e833b896d0730a9db8ab7c06c
parent9dc22cb097f1895af57d71c76a8dcda384596301 (diff)
Updated.
-rw-r--r--coq/test8.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/coq/test8.v b/coq/test8.v
index c6ab8c59..caa82a0e 100644
--- a/coq/test8.v
+++ b/coq/test8.v
@@ -1,4 +1,6 @@
-Add LoadPath "/home/courtieu/coq/actual/ide".
+(* -*- coding: utf-8; -*- *)
+
+Add LoadPath "/usr/lib/coq/ide".
Require Import utf8.
(* Printing of unicode notation, in *goals* *)