Fixes the fix of #407. Is this temporary.

This fix is not completely satisfying for the following reason:

1- I had to add a new hook in generic code. But I don't see how we
   could avoid this: the computation of options must happen AFTER the
   proof-prog-name is asked to the user, because this computation
   depends on the version of coq.

2- We should fix the synchronization between coq-prog-name and
   proof-prog-name. Either remove coq-prog-name and use only
   proof-prog-name, or have the generic coq always point to
   some (proof-ass-sym prog-name).

1 files changed, 10 insertions, 0 deletions

diff --git a/coq/coq-system.el b/coq/coq-system.el
index 28c73ae7..e89a0fdb 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -618,6 +618,16 @@ Does nothing if `coq-use-project-file' is nil."
                        'coq-load-project-file
                        nil t)))
 
+; detecting coqtop args should happen at the last moment before
+; calling the process. In particular it should ahppen after that
+; proof-prog-name-ask is performed, this hook is at the right place.
+(add-hook 'proof-shell-before-process-hook
+          '(lambda ()
+             ;; It seems coq-prog-name and proof-prog-name are not correctly linked
+             ;; so let us make sure they are the same before computing options
+             (setq coq-prog-name proof-prog-name)
+             (setq coq-prog-args (coq-prog-args))))
+
 ;; smie's parenthesis blinking is too slow, let us have the default one back
 (add-hook 'coq-mode-hook
           '(lambda ()