From ce84f518a210237804779c8840b2783e1f5d8e56 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Sat, 27 May 2017 22:05:03 +0200 Subject: make the expansion of the "DECLARE PLUGIN" closer to the way how a human would write that code --- grammar/vernacextend.mlp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 >>; ] ] ] ; -- cgit v1.2.3 From 71004fe0ab615da7e5fd6cd5634253e3cc43eae2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Sun, 28 May 2017 11:40:35 +0200 Subject: cleanup in ".merlin" file --- .merlin | 2 -- 1 file changed, 2 deletions(-) diff --git a/.merlin b/.merlin index b78f24551..2e351dd01 100644 --- a/.merlin +++ b/.merlin @@ -1,7 +1,5 @@ FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50 -S ltac -B ltac S config B config S ide -- cgit v1.2.3 From 5e7d5491304ce3765fa245bb697a239b05921636 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Tue, 30 May 2017 10:54:03 +0200 Subject: removing duplicate line from "tools/CoqMakefile.in" --- tools/CoqMakefile.in | 1 - 1 file changed, 1 deletion(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index fb064c495..13a57a37d 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@ -- cgit v1.2.3