aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-02 11:24:20 +0000
committerGitHub2020-10-02 11:24:20 +0000
commit214215e5a130b543cea4a14ef75c6190fecf6a12 (patch)
tree955290a6dc869f9a67e9c8ee3aeec3da8a90df83 /Makefile.dev
parentbb2d0d56df08ca54764be5a3eb5c09ce00009d6c (diff)
parent4476f64dc87fb86738fc4c9f939113b70843c035 (diff)
Merge PR #13054: {new,setoid_}ring -> ring
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.dev b/Makefile.dev
index f48a6f0d8f..5825a884c2 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -154,7 +154,7 @@ LTACVO:=$(filter theories/ltac/%, $(THEORIESVO))
omega: $(OMEGAVO) $(OMEGACMO)
micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
-setoid_ring: $(RINGVO) $(RINGCMO)
+ring: $(RINGVO) $(RINGCMO)
nsatz: $(NSATZVO) $(NSATZCMO)
extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
funind: $(FUNINDCMO) $(FUNINDVO)
@@ -163,7 +163,7 @@ rtauto: $(RTAUTOVO) $(RTAUTOCMO)
btauto: $(BTAUTOVO) $(BTAUTOCMO)
ltac: $(LTACVO) $(LTACCMO)
-.PHONY: omega micromega setoid_ring nsatz extraction
+.PHONY: omega micromega ring nsatz extraction
.PHONY: funind cc rtauto btauto ltac
# For emacs: