diff options
| author | Maxime Dénès | 2020-09-18 14:15:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-02 13:23:30 +0200 |
| commit | 4476f64dc87fb86738fc4c9f939113b70843c035 (patch) | |
| tree | 955290a6dc869f9a67e9c8ee3aeec3da8a90df83 /Makefile.dev | |
| parent | bb2d0d56df08ca54764be5a3eb5c09ce00009d6c (diff) | |
{new,setoid_}ring -> ring
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 4 |
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: |