diff options
| author | Théo Zimmermann | 2019-05-07 13:41:04 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-07 13:41:04 +0200 |
| commit | 7602c2cb547fe6664f7a065d17717baf12b9da88 (patch) | |
| tree | 1b034b3646090d35a8d730cbec6a5cf1c91da804 /Makefile.vofiles | |
| parent | 8aa64e7c4661549fef63a1c9c2e4e5284db911d8 (diff) | |
| parent | 9779c0bf4945693bfd37b141e2c9f0fea200ba4d (diff) | |
Merge PR #10002: Integrate ltac2
Ack-by: JasonGross
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: jfehrle
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'Makefile.vofiles')
| -rw-r--r-- | Makefile.vofiles | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile.vofiles b/Makefile.vofiles index a71d68e565..e05822c889 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -13,7 +13,7 @@ endif ########################################################################### THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v")) -PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins -type f -name "*.v")) +PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins user-contrib -type f -name "*.v")) ALLVO := $(THEORIESVO) $(PLUGINSVO) VFILES := $(ALLVO:.$(VO)=.v) @@ -24,16 +24,16 @@ THEORIESLIGHTVO:= \ # convert a (stdlib) filename into a module name: # remove .vo, replace theories and plugins by Coq, and replace slashes by dots -vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))) +vo_to_mod = $(subst /,.,$(patsubst user-contrib/%,%,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))) ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo)) # Converting a stdlib filename into native compiler filenames # Used for install targets -vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*))))) +vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))) -vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))) +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))) ifdef QUICK GLOBFILES:= |