From 6deddd3e0c6cc1d7cbf8414f7553c5d7752a0801 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 28 Apr 2017 14:02:00 -0400
Subject: Allow interactive editing of {C,}Morphisms in PG

---
 theories/Classes/CMorphisms.v | 2 +-
 theories/Classes/Morphisms.v  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Classes')

diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 1cfca4169..74ca5d4c8 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8 -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
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     *)
-- 
cgit v1.2.3