Should fix #49 and #55 (compilation of From .. Require).

1 files changed, 7 insertions, 6 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 415f65ee..8ce4b0c2 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -300,12 +300,6 @@ the latter condition into an error, then set this variable to
   :safe 'stringp
   :group 'coq-auto-compile)
 
-(defconst coq-require-command-regexp
-  "^Require[ \t\n]+\\(Import\\|Export\\)?[ \t\n]*"
-  "Regular expression matching Require commands in Coq.
-Should match \"Require\" with its import and export variants up to (but not
-including) the first character of the first required module. The required
-modules are matched separately with `coq-require-id-regexp'")
 
 (defconst coq-require-id-regexp
   "[ \t\n]*\\([A-Za-z0-9_']+\\(\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*"
@@ -315,6 +309,13 @@ white space. The module identifier must be matched with group number 1.
 Note that the trailing dot in \"Require A.\" is not part of the module
 identifier and should therefore not be matched by this regexp.")
 
+(defconst coq-require-command-regexp
+  "\\(?:^From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*\\)?\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*"
+  "Regular expression matching Require commands in Coq.
+Should match \"Require\" with its import and export variants up to (but not
+including) the first character of the first required module. The required
+modules are matched separately with `coq-require-id-regexp'")
+
 (defvar coq-compile-history nil
   "History of external Coq compilation commands.")