From 2bd0d2a681d79f027919aec58661f06a2d184426 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 14 Aug 2000 17:09:06 +0000
Subject: enhancement of outline regexps for coq, now when hiding bodies, we
 see completely definitions and theorems, but proof script are hidden (but can
 be blindly sent to the prover). Seems to work correctly.

---
 coq/coq.el | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 07ceef3e..d00ee90e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -88,11 +88,11 @@
 ;; ----- outline
 
 (defvar coq-outline-regexp
-  (proof-ids-to-regexp 
-	   '("Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact"
-	   "Remark" "Record" "Inductive" "Definition")))
+  (concat "(\\*\\|" (proof-ids-to-regexp 
+	   '(
+"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Hint" "Hints" "Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint"))))
 
-(defvar coq-outline-heading-end-regexp "\.\\|\\*)")
+(defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.\n")
 
 (defvar coq-shell-outline-regexp coq-goal-regexp)
 (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)
-- 
cgit v1.2.3