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/proof-config.el | |
| 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/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 7 |
1 files changed, 7 insertions, 0 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 |