diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 8 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 16 |
2 files changed, 22 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 805b2cee0..a1ca53244 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4505,6 +4505,7 @@ integers. This tactic must be loaded by the command \texttt{Require Import \tacindex{ring} \tacindex{ring\_simplify} \comindex{Add Ring} +\comindex{Print Rings} The {\tt ring} tactic solves equations upon polynomial expressions of a ring (or semi-ring) structure. It proceeds by normalizing both hand @@ -4519,7 +4520,8 @@ forms. If no term is given, then the conclusion should be an equation and both hand sides are normalized. See Chapter~\ref{ring} for more information on the tactic and how to -declare new ring structures. +declare new ring structures. All declared field structures can be +printed with the {\tt Print Rings} command. \subsection{{\tt field}, {\tt field\_simplify \term$_1$ \mbox{\dots} \term$_n$}, and \tt field\_simplify\_eq} @@ -4527,6 +4529,7 @@ declare new ring structures. \tacindex{field\_simplify} \tacindex{field\_simplify\_eq} \comindex{Add Field} +\comindex{Print Fields} The {\tt field} tactic is built on the same ideas as {\tt ring}: this is a reflexive tactic that solves or simplifies equations in a field @@ -4545,7 +4548,8 @@ All of these 3 tactics may generate a subgoal in order to prove that denominators are different from zero. See Chapter~\ref{ring} for more information on the tactic and how to -declare new field structures. +declare new field structures. All declared field structures can be +printed with the {\tt Print Fields} command. \Example \begin{coq_example*} diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 9614d74e2..355a18005 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -754,6 +754,14 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in add_theory id (ic t) set k cst (pre,post) power sign div] + | [ "Print" "Rings" ] => [Vernacexpr.VtQuery true, Vernacexpr.VtLater] -> [ + msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.ring_req)) + ) !from_name ] END (*****************************************************************************) @@ -1081,6 +1089,14 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] +| [ "Print" "Fields" ] => [Vernacexpr.VtQuery true, Vernacexpr.VtLater] -> [ + msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.field_req)) + ) !field_from_name ] END |