Skip to content

Commit 4476f64

Browse files
maximedenesSkySkimmer
maximedenes
authored and
SkySkimmer
committed
{new,setoid_}ring -> ring
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
1 parent bb2d0d5 commit 4476f64

25 files changed

+61
-61
lines changed

Diff for: ‎.github/CODEOWNERS

+1-1
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@
160160
/plugins/nsatz/ @coq/nsatz-maintainers
161161
/theories/nsatz/ @coq/nsatz-maintainers
162162

163-
/plugins/setoid_ring/ @coq/ring-maintainers
163+
/plugins/ring/ @coq/ring-maintainers
164164
/theories/setoid_ring/ @coq/ring-maintainers
165165

166166
/plugins/ssrmatching/ @coq/ssreflect-maintainers

Diff for: ‎CREDITS

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ plugins/omega
4646
developed by Pierre Crégut (France Telecom R&D, 1996)
4747
plugins/rtauto
4848
developed by Pierre Corbineau (LRI, 2005)
49-
plugins/setoid_ring
49+
plugins/ring
5050
developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
5151
Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
5252
and Bruno Barras (INRIA LogiCal, 2005-2006),

Diff for: ‎META.coq.in

+7-7
Original file line numberDiff line numberDiff line change
@@ -352,19 +352,19 @@ package "plugins" (
352352
plugin(native) = "zify_plugin.cmxs"
353353
)
354354

355-
package "setoid_ring" (
355+
package "ring" (
356356

357-
description = "Coq newring plugin"
357+
description = "Coq ring plugin"
358358
version = "8.13"
359359

360360
requires = ""
361-
directory = "setoid_ring"
361+
directory = "ring"
362362

363-
archive(byte) = "newring_plugin.cmo"
364-
archive(native) = "newring_plugin.cmx"
363+
archive(byte) = "ring_plugin.cmo"
364+
archive(native) = "ring_plugin.cmx"
365365

366-
plugin(byte) = "newring_plugin.cmo"
367-
plugin(native) = "newring_plugin.cmxs"
366+
plugin(byte) = "ring_plugin.cmo"
367+
plugin(native) = "ring_plugin.cmxs"
368368
)
369369

370370
package "extraction" (

Diff for: ‎Makefile.common

+2-2
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ CORESRCDIRS:=\
103103

104104
PLUGINDIRS:=\
105105
omega micromega \
106-
setoid_ring extraction \
106+
ring extraction \
107107
cc funind firstorder derive \
108108
rtauto nsatz syntax btauto \
109109
ssrmatching ltac ssr ssrsearch
@@ -140,7 +140,7 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l
140140

141141
OMEGACMO:=plugins/omega/omega_plugin.cmo
142142
MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
143-
RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
143+
RINGCMO:=plugins/ring/ring_plugin.cmo
144144
NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
145145
EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
146146
FUNINDCMO:=plugins/funind/recdef_plugin.cmo

Diff for: ‎Makefile.dev

+2-2
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ LTACVO:=$(filter theories/ltac/%, $(THEORIESVO))
154154

155155
omega: $(OMEGAVO) $(OMEGACMO)
156156
micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
157-
setoid_ring: $(RINGVO) $(RINGCMO)
157+
ring: $(RINGVO) $(RINGCMO)
158158
nsatz: $(NSATZVO) $(NSATZCMO)
159159
extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
160160
funind: $(FUNINDCMO) $(FUNINDVO)
@@ -163,7 +163,7 @@ rtauto: $(RTAUTOVO) $(RTAUTOCMO)
163163
btauto: $(BTAUTOVO) $(BTAUTOCMO)
164164
ltac: $(LTACVO) $(LTACCMO)
165165

166-
.PHONY: omega micromega setoid_ring nsatz extraction
166+
.PHONY: omega micromega ring nsatz extraction
167167
.PHONY: funind cc rtauto btauto ltac
168168

169169
# For emacs:

Diff for: ‎dev/ocamldebug-coq.run

+1-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ exec $OCAMLDEBUG \
3030
-I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \
3131
-I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \
3232
-I $COQTOP/plugins/ring \
33-
-I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \
33+
-I $COQTOP/plugins/rtauto \
3434
-I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \
3535
-I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \
3636
-I $COQTOP/ide \

Diff for: ‎doc/sphinx/addendum/ring.rst

+5-5
Original file line numberDiff line numberDiff line change
@@ -387,16 +387,16 @@ The syntax for adding a new ring is
387387
interpretation via ``Cp_phi`` (the evaluation function of power
388388
coefficient) is the original term, or returns ``InitialRing.NotConstant``
389389
if not a constant coefficient (i.e. |L_tac| is the inverse function of
390-
``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v``
391-
and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic
390+
``Cp_phi``). See files ``plugins/ring/ZArithRing.v``
391+
and ``plugins/ring/RealField.v`` for examples. By default the tactic
392392
does not recognize power expressions as ring expressions.
393393

394394
:n:`sign @one_term`
395395
allows :tacn:`ring_simplify` to use a minus operation when
396396
outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
397397
term :token:`term` is a proof that a given sign function indicates expressions
398398
that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See
399-
``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
399+
``plugins/ring/InitialRing.v`` for examples of sign function.
400400

401401
:n:`div @one_term`
402402
allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with
@@ -405,7 +405,7 @@ The syntax for adding a new ring is
405405
euclidean division function (:n:`@one_term` has to be a proof of
406406
``Ring_theory.div_theory``). For example, this function is called when
407407
trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See
408-
``plugins/setoid_ring/InitialRing.v`` for examples of div function.
408+
``plugins/ring/InitialRing.v`` for examples of div function.
409409

410410
:n:`closed [ {+ @qualid } ]`
411411
to be documented
@@ -538,7 +538,7 @@ Dealing with fields
538538
The tactic must be loaded by ``Require Import Field``. New field
539539
structures can be declared to the system with the ``Add Field`` command
540540
(see below). The field of real numbers is defined in module ``RealField``
541-
(in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so
541+
(in ``plugins/ring``). It is exported by module ``Rbase``, so
542542
that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on
543543
real numbers. Rational numbers in canonical form are also declared as
544544
a field in the module ``Qcanon``.

Diff for: ‎doc/sphinx/proof-engine/tactics.rst

+1-1
Original file line numberDiff line numberDiff line change
@@ -4726,7 +4726,7 @@ Automating
47264726

47274727
.. seealso::
47284728

4729-
File plugins/setoid_ring/RealField.v for an example of instantiation,
4729+
File plugins/ring/RealField.v for an example of instantiation,
47304730
theory theories/Reals for many examples of use of field.
47314731

47324732
Non-logical tactics

Diff for: ‎doc/tools/docgram/dune

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@
2424
(glob_files %{project_root}/plugins/nsatz/*.mlg)
2525
(glob_files %{project_root}/plugins/omega/*.mlg)
2626
(glob_files %{project_root}/plugins/rtauto/*.mlg)
27-
(glob_files %{project_root}/plugins/setoid_ring/*.mlg)
27+
(glob_files %{project_root}/plugins/ring/*.mlg)
2828
(glob_files %{project_root}/plugins/syntax/*.mlg)
2929
(glob_files %{project_root}/user-contrib/Ltac2/*.mlg)
3030
; Sphinx files

Diff for: ‎kernel/cClosure.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ val inject : constr -> fconstr
159159
(** mk_atom: prevents a term from being evaluated *)
160160
val mk_atom : constr -> fconstr
161161

162-
(** mk_red: makes a reducible term (used in newring) *)
162+
(** mk_red: makes a reducible term (used in ring) *)
163163
val mk_red : fterm -> fconstr
164164

165165
val fterm_of : fconstr -> fterm

Diff for: ‎plugins/nsatz/nsatz.ml

+8-8
Original file line numberDiff line numberDiff line change
@@ -127,14 +127,14 @@ let mul = function
127127

128128
let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
129129

130-
let tpexpr = gen_constant "plugins.setoid_ring.pexpr"
131-
let ttconst = gen_constant "plugins.setoid_ring.const"
132-
let ttvar = gen_constant "plugins.setoid_ring.var"
133-
let ttadd = gen_constant "plugins.setoid_ring.add"
134-
let ttsub = gen_constant "plugins.setoid_ring.sub"
135-
let ttmul = gen_constant "plugins.setoid_ring.mul"
136-
let ttopp = gen_constant "plugins.setoid_ring.opp"
137-
let ttpow = gen_constant "plugins.setoid_ring.pow"
130+
let tpexpr = gen_constant "plugins.ring.pexpr"
131+
let ttconst = gen_constant "plugins.ring.const"
132+
let ttvar = gen_constant "plugins.ring.var"
133+
let ttadd = gen_constant "plugins.ring.add"
134+
let ttsub = gen_constant "plugins.ring.sub"
135+
let ttmul = gen_constant "plugins.ring.mul"
136+
let ttopp = gen_constant "plugins.ring.opp"
137+
let ttpow = gen_constant "plugins.ring.pow"
138138

139139
let tlist = gen_constant "core.list.type"
140140
let lnil = gen_constant "core.list.nil"

Diff for: ‎plugins/ring/dune

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(library
2+
(name ring_plugin)
3+
(public_name coq.plugins.ring)
4+
(synopsis "Coq's ring plugin")
5+
(libraries coq.plugins.ltac))
6+
7+
(coq.pp (modules g_ring))

Diff for: ‎plugins/setoid_ring/g_newring.mlg renamed to ‎plugins/ring/g_ring.mlg

+3-3
Original file line numberDiff line numberDiff line change
@@ -13,16 +13,16 @@
1313
open Ltac_plugin
1414
open Pp
1515
open Util
16-
open Newring_ast
17-
open Newring
16+
open Ring_ast
17+
open Ring
1818
open Stdarg
1919
open Tacarg
2020
open Pcoq.Constr
2121
open Pltac
2222

2323
}
2424

25-
DECLARE PLUGIN "newring_plugin"
25+
DECLARE PLUGIN "ring_plugin"
2626

2727
TACTIC EXTEND protect_fv
2828
| [ "protect_fv" string(map) "in" ident(id) ] ->

Diff for: ‎plugins/setoid_ring/newring.ml renamed to ‎plugins/ring/ring.ml

+5-5
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ open Libobject
2828
open Printer
2929
open Declare
3030
open Entries
31-
open Newring_ast
31+
open Ring_ast
3232
open Proofview.Notations
3333

3434
let error msg = CErrors.user_err Pp.(str msg)
@@ -115,7 +115,7 @@ let closed_term args _ = match args with
115115

116116
let closed_term_ast =
117117
let tacname = {
118-
mltac_plugin = "newring_plugin";
118+
mltac_plugin = "ring_plugin";
119119
mltac_tactic = "closed_term";
120120
} in
121121
let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
@@ -178,7 +178,7 @@ let tactic_res = ref [||]
178178

179179
let get_res =
180180
let open Tacexpr in
181-
let name = { mltac_plugin = "newring_plugin"; mltac_tactic = "get_res"; } in
181+
let name = { mltac_plugin = "ring_plugin"; mltac_tactic = "get_res"; } in
182182
let entry = { mltac_name = name; mltac_index = 0 } in
183183
let tac args ist =
184184
let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in
@@ -212,7 +212,7 @@ let exec_tactic env evd n f args =
212212
let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)))
213213
let gen_reference n = lazy (Coqlib.lib_ref n)
214214

215-
let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory"
215+
let coq_mk_Setoid = gen_constant "plugins.ring.Build_Setoid_Theory"
216216
let coq_None = gen_reference "core.option.None"
217217
let coq_Some = gen_reference "core.option.Some"
218218
let coq_eq = gen_constant "core.eq.type"
@@ -265,7 +265,7 @@ let znew_ring_path =
265265
let zltac s =
266266
lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))
267267

268-
let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s) [@@ocaml.warning "-3"]
268+
let mk_cst l s = lazy (Coqlib.coq_reference "ring" l s) [@@ocaml.warning "-3"]
269269
let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s
270270

271271
(* Ring theory *)

Diff for: ‎plugins/setoid_ring/newring.mli renamed to ‎plugins/ring/ring.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
open Names
1212
open EConstr
1313
open Constrexpr
14-
open Newring_ast
14+
open Ring_ast
1515

1616
val protect_tac_in : string -> Id.t -> unit Proofview.tactic
1717

Diff for: ‎plugins/setoid_ring/newring_ast.ml renamed to ‎plugins/ring/ring_ast.ml

File renamed without changes.

Diff for: ‎plugins/setoid_ring/newring_ast.mli renamed to ‎plugins/ring/ring_ast.mli

File renamed without changes.

Diff for: ‎plugins/ring/ring_plugin.mlpack

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Ring_ast
2+
Ring
3+
G_ring

Diff for: ‎plugins/setoid_ring/dune

-7
This file was deleted.

Diff for: ‎plugins/setoid_ring/newring_plugin.mlpack

-3
This file was deleted.

Diff for: ‎theories/Setoids/Setoid.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ Require Coq.ssr.ssrsetoid.
1919
Definition Setoid_Theory := @Equivalence.
2020
Definition Build_Setoid_Theory := @Build_Equivalence.
2121

22-
Register Build_Setoid_Theory as plugins.setoid_ring.Build_Setoid_Theory.
22+
Register Build_Setoid_Theory as plugins.ring.Build_Setoid_Theory.
2323

2424
Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x.
2525
Proof.

Diff for: ‎theories/dune

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
coq.plugins.btauto
2424
coq.plugins.rtauto
2525

26-
coq.plugins.setoid_ring
26+
coq.plugins.ring
2727
coq.plugins.nsatz
2828
coq.plugins.omega
2929

Diff for: ‎theories/setoid_ring/Ring_base.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
ring tactic. Abstract rings need more theory, depending on
1313
ZArith_base. *)
1414

15-
Declare ML Module "newring_plugin".
15+
Declare ML Module "ring_plugin".
1616
Require Export Ring_theory.
1717
Require Export Ring_tac.
1818
Require Import InitialRing.

Diff for: ‎theories/setoid_ring/Ring_polynom.v

+8-8
Original file line numberDiff line numberDiff line change
@@ -919,14 +919,14 @@ Section MakeRingPol.
919919
| PEopp : PExpr -> PExpr
920920
| PEpow : PExpr -> N -> PExpr.
921921

922-
Register PExpr as plugins.setoid_ring.pexpr.
923-
Register PEc as plugins.setoid_ring.const.
924-
Register PEX as plugins.setoid_ring.var.
925-
Register PEadd as plugins.setoid_ring.add.
926-
Register PEsub as plugins.setoid_ring.sub.
927-
Register PEmul as plugins.setoid_ring.mul.
928-
Register PEopp as plugins.setoid_ring.opp.
929-
Register PEpow as plugins.setoid_ring.pow.
922+
Register PExpr as plugins.ring.pexpr.
923+
Register PEc as plugins.ring.const.
924+
Register PEX as plugins.ring.var.
925+
Register PEadd as plugins.ring.add.
926+
Register PEsub as plugins.ring.sub.
927+
Register PEmul as plugins.ring.mul.
928+
Register PEopp as plugins.ring.opp.
929+
Register PEpow as plugins.ring.pow.
930930

931931
(** evaluation of polynomial expressions towards R *)
932932
Definition mk_X j := mkPinj_pred j mkX.

Diff for: ‎theories/setoid_ring/Ring_tac.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Require Import Ring_polynom.
1515
Require Import BinList.
1616
Require Export ListTactics.
1717
Require Import InitialRing.
18-
Declare ML Module "newring_plugin".
18+
Declare ML Module "ring_plugin".
1919

2020

2121
(* adds a definition t' on the normal form of t and an hypothesis id

0 commit comments

Comments
 (0)