diff options
| author | Pierre Courtieu | 2020-04-10 13:08:29 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-04-10 13:08:29 +0200 |
| commit | d1053a06aa31ce05fa0741fb61dfb1266fcb0364 (patch) | |
| tree | 67c8ef6766a8b890f5e5656462fd1afe654af1ae /generic | |
| parent | 4dba3f78e50604d899ef80bfda45c5aa4467adeb (diff) | |
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.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 7 | ||||
| -rw-r--r-- | generic/proof-depends.el | 3 |
2 files changed, 9 insertions, 1 deletions
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))) |