aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Morphisms.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-28 14:02:00 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-04-28 14:02:00 -0400
commit6deddd3e0c6cc1d7cbf8414f7553c5d7752a0801 (patch)
tree1eab4605d82535a40a93ba7ef9db69feb7246174 /theories/Classes/Morphisms.v
parent7943b1fade775af48917d54878e65b80217be038 (diff)
Allow interactive editing of {C,}Morphisms in PG
Diffstat (limited to 'theories/Classes/Morphisms.v')
-rw-r--r--theories/Classes/Morphisms.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 06511ace5..6396e5390 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8 -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)