diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-01-12 22:17:22 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-01-12 22:17:22 +0000 |
| commit | 4eb269982af632d39fe9f28c866436acd7d36370 (patch) | |
| tree | 5eeeb009146f765d3a06dc5108d6fe246594fb47 /coq/coq-syntax.el | |
| parent | c91f610f662a1357522a12276ee51e8cb18fce91 (diff) | |
Add preliminary support for multiple files for coq.
The following points are implemented already:
- recompile either via an external command (make) or let
ProofGeneral handle everything internally
- complete dependency tracking and recompilation for coq files in
internal mode
- support for extending the LoadPath: does almost work, even if
specified file-locally
- move back to clean state if recompilation fails
There are the following known problems:
- coq-load-path extensions are not retracted
- fails on partially qualified library names
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 7b5306d3..5b15cb3a 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -962,10 +962,10 @@ Used by `coq-goal-command-p'" ;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) ;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" -(defconst coq-require-command-regexp - (concat "Require\\s-+\\(" proof-id "\\)") - "Regular expression matching Require commands in Coq. -Group number 1 matches the name of the library which is required.") +;; (defconst coq-require-command-regexp +;; (concat "Require\\s-+\\(" proof-id "\\)") +;; "Regular expression matching Require commands in Coq. +;; Group number 1 matches the name of the library which is required.") ;; ;; font-lock |