From d1053a06aa31ce05fa0741fb61dfb1266fcb0364 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 10 Apr 2020 13:08:29 +0200
Subject: Fixed proof using annotation mechanism.

I ended up using (in a slight devious way) the lemma dependency
mechanism of PG: the dependency information stored in the span is only
the ones suggested by coq: only the one that should appear in theproof
using annotation (and only when coq felt the need to suggest them.
---
 generic/proof-config.el  | 7 +++++++
 generic/proof-depends.el | 3 ++-
 2 files changed, 9 insertions(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/proof-config.el b/generic/proof-config.el
index f9947757..41c5e9d7 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1758,6 +1758,13 @@ This hook is used within Proof General to refresh the toolbar."
   :type '(repeat function)
   :group 'proof-shell)
 
+;;;;;;
+(defcustom proof-dependencies-system-specific nil
+  "doc TODO"
+  :type '(repeat function)
+  :group 'proof-shell)
+;;;;;
+
 (defcustom proof-shell-syntax-table-entries nil
   "List of syntax table entries for proof script mode.
 A flat list of the form
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 163a0968..c3de97f7 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -120,7 +120,8 @@ Called from `proof-done-advancing' when a save is processed and
 		  'type))))
 
     (span-set-property gspan 'dependencies-within-file depspans)
-    (setq proof-last-theorem-dependencies nil)))
+    (setq proof-last-theorem-dependencies nil)
+    (funcall 'proof-dependencies-system-specific name gspan)))
 
 
 
-- 
cgit v1.2.3