aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/Ncring_initial.v4
-rw-r--r--plugins/setoid_ring/Ring_theory.v5
-rw-r--r--plugins/setoid_ring/g_newring.ml45
-rw-r--r--plugins/setoid_ring/newring.ml27
4 files changed, 22 insertions, 19 deletions
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 96885d2f7a..20022c00ec 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -18,7 +18,6 @@ Require Import BinInt.
Require Import Setoid.
Require Export Ncring.
Require Export Ncring_polynom.
-Import List.
Set Implicit Arguments.
@@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}.
| Z0 => 0
| Zneg p => -(gen_phiPOS p)
end.
- Notation "[ x ]" := (gen_phiZ x).
+ Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Local Open Scope ZMORPHISM.
Definition get_signZ z :=
match z with
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 7fcd6c08a7..f7757a18da 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -238,7 +238,6 @@ Section ALMOST_RING.
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Infix "==" := req. Infix "+" := radd. Infix "* " := rmul.
- Infix "-" := rsub. Notation "- x" := (ropp x).
(** Leibniz equality leads to a setoid theory and is extensional*)
Lemma Eqsth : Equivalence (@eq R).
@@ -263,7 +262,7 @@ Section ALMOST_RING.
-x = x and x - y = x + y *)
Definition SRopp (x:R) := x. Notation "- x" := (SRopp x).
- Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y).
+ Definition SRsub x y := x + -y. Infix "-" := SRsub.
Lemma SRopp_ext : forall x y, x == y -> -x == -y.
Proof. intros x y H; exact H. Qed.
@@ -320,6 +319,8 @@ Section ALMOST_RING.
Qed.
End SEMI_RING.
+ Infix "-" := rsub.
+ Notation "- x" := (ropp x).
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed.
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 216eb8b373..707ff79a6c 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,6 +8,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+open Ltac_plugin
open Pp
open Util
open Libnames
@@ -15,9 +16,9 @@ open Printer
open Newring_ast
open Newring
open Stdarg
-open Constrarg
+open Tacarg
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
DECLARE PLUGIN "newring_plugin"
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 90f5f8e63d..eb35d3f806 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Ltac_plugin
open Pp
open CErrors
open Util
@@ -79,7 +80,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps
let lookup_map map =
try String.Map.find map !protect_maps
with Not_found ->
- errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
+ user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
let protect_red map env sigma c =
kl (create_clos_infos all env)
@@ -122,10 +123,10 @@ let closed_term_ast l =
mltac_index = 0;
} in
let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
- TacFun([Some(Id.of_string"t")],
+ TacFun([Name(Id.of_string"t")],
TacML(Loc.ghost,tacname,
- [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
- TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)]))
+ [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+ TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
@@ -205,7 +206,7 @@ let exec_tactic env evd n f args =
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in
- let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in
+ let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
(** Evaluate the whole result *)
let gl = dummy_goal env evd in
let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
@@ -348,13 +349,13 @@ let find_ring_structure env sigma l =
let check c =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
- errorlabstrm "ring"
+ user_err ~hdr:"ring"
(str"arguments of ring_simplify do not have all the same type")
in
List.iter check cl';
(try ring_for_carrier ty
with Not_found ->
- errorlabstrm "ring"
+ user_err ~hdr:"ring"
(str"cannot find a declared ring structure over"++
spc()++str"\""++pr_constr ty++str"\""))
| [] -> assert false
@@ -722,8 +723,8 @@ let ltac_ring_structure e =
let pow_tac = tacarg e.ring_pow_tac in
let lemma1 = carg e.ring_lemma1 in
let lemma2 = carg e.ring_lemma2 in
- let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in
- let posttac = tacarg (TacFun([None],e.ring_post_tac)) in
+ let pretac = tacarg (TacFun([Anonymous],e.ring_pre_tac)) in
+ let posttac = tacarg (TacFun([Anonymous],e.ring_post_tac)) in
[req;sth;ext;morph;th;cst_tac;pow_tac;
lemma1;lemma2;pretac;posttac]
@@ -828,13 +829,13 @@ let find_field_structure env sigma l =
let check c =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
- errorlabstrm "field"
+ user_err ~hdr:"field"
(str"arguments of field_simplify do not have all the same type")
in
List.iter check cl';
(try field_for_carrier ty
with Not_found ->
- errorlabstrm "field"
+ user_err ~hdr:"field"
(str"cannot find a declared field structure over"++
spc()++str"\""++pr_constr ty++str"\""))
| [] -> assert false
@@ -994,8 +995,8 @@ let ltac_field_structure e =
let field_simpl_eq_ok = carg e.field_simpl_eq_ok in
let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in
let cond_ok = carg e.field_cond in
- let pretac = tacarg (TacFun([None],e.field_pre_tac)) in
- let posttac = tacarg (TacFun([None],e.field_post_tac)) in
+ let pretac = tacarg (TacFun([Anonymous],e.field_pre_tac)) in
+ let posttac = tacarg (TacFun([Anonymous],e.field_post_tac)) in
[req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
field_simpl_eq_in_ok;cond_ok;pretac;posttac]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:03:53 +0000