diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 13:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 13:14:09 +0200 |
| commit | 73fd3afba9e8917dfc0644d1d8d9b22063cfa2fe (patch) | |
| tree | 408d331e0a41d21fa2a787c54504e112962f195a | |
| parent | 77e4a3712dff87e5941dd93ebfa8028039ab0715 (diff) | |
| parent | 5e7d5491304ce3765fa245bb697a239b05921636 (diff) | |
Merge PR#698: Trunk misc
| -rw-r--r-- | grammar/vernacextend.mlp | 2 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 4f9a7c75c..798b46523 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -143,7 +143,7 @@ EXTEND | "DECLARE"; "PLUGIN"; name = STRING -> declare_str_items loc [ <:str_item< value __coq_plugin_name = $str:name$ >>; - <:str_item< value _ = Mltop.add_known_module $str:name$ >>; + <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>; ] ] ] ; diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 1308e9175..c25ad1f37 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -39,7 +39,6 @@ CAMLP4BIN := $(COQMF_CAMLP4BIN) CAMLP4LIB := $(COQMF_CAMLP4LIB) CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) -COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) @CONF_FILE@: @PROJECT_FILE@ @COQ_MAKEFILE_INVOCATION@ |