aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/g_ltac.ml45
-rw-r--r--plugins/ltac/ltac_plugin.mlpack4
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/rewrite.ml10
-rw-r--r--plugins/ltac/tacentries.ml35
-rw-r--r--plugins/ltac/tacentries.mli3
-rw-r--r--plugins/ltac/tacenv.ml44
-rw-r--r--plugins/ltac/tacenv.mli10
-rw-r--r--plugins/ltac/tacexpr.mli3
-rw-r--r--plugins/ltac/tacintern.ml6
-rw-r--r--plugins/micromega/EnvRing.v16
-rw-r--r--plugins/setoid_ring/Field_theory.v24
-rw-r--r--plugins/setoid_ring/InitialRing.v50
-rw-r--r--plugins/setoid_ring/Ring_polynom.v16
-rw-r--r--plugins/setoid_ring/Ring_theory.v39
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrparser.ml44
18 files changed, 211 insertions, 66 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 86c983bdd9..d639dd0e1c 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -482,6 +482,11 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
[ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
END
+VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
+| [ "Locate" "Ltac" reference(r) ] ->
+ [ Tacentries.print_located_tactic r ]
+END
+
let pr_ltac_ref = Libnames.pr_reference
let pr_tacdef_body tacdef_body =
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index 12b4c81fc4..3972b7aac3 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -1,9 +1,9 @@
Tacarg
+Tacsubst
+Tacenv
Pptactic
Pltac
Taccoerce
-Tacsubst
-Tacenv
Tactic_debug
Tacintern
Tacentries
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d8bd166208..d588c888c4 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -336,7 +336,7 @@ type 'a extra_genarg_printer =
let pr_ltac_constant kn =
if !Flags.in_debugger then KerName.print kn
else try
- pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+ pr_qualid (Tacenv.shortest_qualid_of_tactic kn)
with Not_found -> (* local tactic not accessible anymore *)
str "<" ++ KerName.print kn ++ str ">"
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index c79d5b389f..d9da954fe6 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -93,7 +93,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t
val pr_alias : (Val.t -> Pp.t) ->
int -> Names.KerName.t -> Val.t list -> Pp.t
-val pr_ltac_constant : Nametab.ltac_constant -> Pp.t
+val pr_ltac_constant : ltac_constant -> Pp.t
val pr_raw_tactic : raw_tactic_expr -> Pp.t
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fd791a9101..1809f0fcdb 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1935,7 +1935,12 @@ let default_morphism sign m =
let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
mor, proper_projection sigma mor morph
+let warn_add_setoid_deprecated =
+ CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
+ Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
+
let add_setoid global binders a aeq t n =
+ warn_add_setoid_deprecated ?loc:a.CAst.loc ();
init_setoid ();
let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
@@ -1954,7 +1959,12 @@ let make_tactic name =
let tacname = Qualid (Loc.tag tacpath) in
TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, [])))
+let warn_add_morphism_deprecated =
+ CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
+ Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
+
let add_morphism_infer glob m n =
+ warn_add_morphism_deprecated ?loc:m.CAst.loc ();
init_setoid ();
let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a8d518fbd8..bcd5b388a1 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -409,7 +409,7 @@ let create_ltac_quotation name cast (e, l) =
type tacdef_kind =
| NewTac of Id.t
- | UpdateTac of Nametab.ltac_constant
+ | UpdateTac of Tacexpr.ltac_constant
let is_defined_tac kn =
try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
@@ -441,7 +441,7 @@ let register_ltac local tacl =
| Tacexpr.TacticRedefinition (ident, body) ->
let loc = loc_of_reference ident in
let kn =
- try Nametab.locate_tactic (snd (qualid_of_reference ident))
+ try Tacenv.locate_tactic (snd (qualid_of_reference ident))
with Not_found ->
CErrors.user_err ?loc
(str "There is no Ltac named " ++ pr_reference ident ++ str ".")
@@ -464,7 +464,7 @@ let register_ltac local tacl =
let defs () =
(** Register locally the tactic to handle recursivity. This function affects
the whole environment, so that we transactify it afterwards. *)
- let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
+ let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in
let () = List.iter iter_rec recvars in
List.map map rfun
in
@@ -475,7 +475,7 @@ let register_ltac local tacl =
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
| UpdateTac kn ->
Tacenv.redefine_ltac local kn tac;
- let name = Nametab.shortest_qualid_of_tactic kn in
+ let name = Tacenv.shortest_qualid_of_tactic kn in
Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
in
List.iter iter defs
@@ -488,7 +488,7 @@ let print_ltacs () =
let entries = List.sort sort entries in
let map (kn, entry) =
let qid =
- try Some (Nametab.shortest_qualid_of_tactic kn)
+ try Some (Tacenv.shortest_qualid_of_tactic kn)
with Not_found -> None
in
match qid with
@@ -506,6 +506,31 @@ let print_ltacs () =
in
Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
+let locatable_ltac = "Ltac"
+
+let () =
+ let open Prettyp in
+ let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
+ let locate_all = Tacenv.locate_extended_all_tactic in
+ let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
+ let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+ let print kn =
+ let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
+ Tacintern.print_ltac qid
+ in
+ let about = name in
+ register_locatable locatable_ltac {
+ locate;
+ locate_all;
+ shortest_qualid;
+ name;
+ print;
+ about;
+ }
+
+let print_located_tactic qid =
+ Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+
(** Grammar *)
let () =
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index aa8f4efe65..ab2c6b3073 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -62,3 +62,6 @@ val create_ltac_quotation : string ->
val print_ltacs : unit -> unit
(** Display the list of ltac definitions currently available. *)
+
+val print_located_tactic : Libnames.reference -> unit
+(** Display the absolute name of a tactic. *)
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 13b44f0e2c..8c59a36fa6 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -11,6 +11,42 @@ open Pp
open Names
open Tacexpr
+(** Nametab for tactics *)
+
+(** TODO: Share me somewhere *)
+module FullPath =
+struct
+ open Libnames
+ type t = full_path
+ let equal = eq_full_path
+ let to_string = string_of_path
+ let repr sp =
+ let dir,id = repr_path sp in
+ id, (DirPath.repr dir)
+end
+
+module KnTab = Nametab.Make(FullPath)(KerName)
+
+let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty)
+
+let push_tactic vis sp kn =
+ let (tab, revtab) = !tactic_tab in
+ let tab = KnTab.push vis sp kn tab in
+ let revtab = KNmap.add kn sp revtab in
+ tactic_tab := (tab, revtab)
+
+let locate_tactic qid = KnTab.locate qid (fst !tactic_tab)
+
+let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab)
+
+let exists_tactic kn = KnTab.exists kn (fst !tactic_tab)
+
+let path_of_tactic kn = KNmap.find kn (snd !tactic_tab)
+
+let shortest_qualid_of_tactic kn =
+ let sp = KNmap.find kn (snd !tactic_tab) in
+ KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab)
+
(** Tactic notations (TacAlias) *)
type alias = KerName.t
@@ -103,19 +139,19 @@ let replace kn path t =
let load_md i ((sp, kn), (local, id, b, t)) = match id with
| None ->
- let () = if not local then Nametab.push_tactic (Until i) sp kn in
+ let () = if not local then push_tactic (Until i) sp kn in
add kn b t
| Some kn0 -> replace kn0 kn t
let open_md i ((sp, kn), (local, id, b, t)) = match id with
| None ->
- let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
+ let () = if not local then push_tactic (Exactly i) sp kn in
add kn b t
| Some kn0 -> replace kn0 kn t
let cache_md ((sp, kn), (local, id ,b, t)) = match id with
| None ->
- let () = Nametab.push_tactic (Until 1) sp kn in
+ let () = push_tactic (Until 1) sp kn in
add kn b t
| Some kn0 -> replace kn0 kn t
@@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) =
let classify_md (local, _, _, _ as o) = Substitute o
-let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 958109e5a7..4ecc978fea 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -7,11 +7,21 @@
(************************************************************************)
open Names
+open Libnames
open Tacexpr
open Geninterp
(** This module centralizes the various ways of registering tactics. *)
+(** {5 Tactic naming} *)
+
+val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit
+val locate_tactic : qualid -> ltac_constant
+val locate_extended_all_tactic : qualid -> ltac_constant list
+val exists_tactic : full_path -> bool
+val path_of_tactic : ltac_constant -> full_path
+val shortest_qualid_of_tactic : ltac_constant -> qualid
+
(** {5 Tactic notations} *)
type alias = KerName.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 64da097deb..2c36faeff4 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -10,13 +10,14 @@ open Loc
open Names
open Constrexpr
open Libnames
-open Nametab
open Genredexpr
open Genarg
open Pattern
open Misctypes
open Locus
+type ltac_constant = KerName.t
+
type direction_flag = bool (* true = Left-to-right false = right-to-right *)
type lazy_flag =
| General (* returns all possible successes *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index fc6ee6aab6..99d7684d36 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,7 +118,7 @@ let intern_constr_reference strict ist = function
let intern_isolated_global_tactic_reference r =
let (loc,qid) = qualid_of_reference r in
- TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[]))
+ TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
let intern_isolated_tactic_reference strict ist r =
(* An ltac reference *)
@@ -137,7 +137,7 @@ let intern_isolated_tactic_reference strict ist r =
let intern_applied_global_tactic_reference r =
let (loc,qid) = qualid_of_reference r in
- ArgArg (loc,locate_tactic qid)
+ ArgArg (loc,Tacenv.locate_tactic qid)
let intern_applied_tactic_reference ist r =
(* An ltac reference *)
@@ -722,7 +722,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n
let print_ltac id =
try
- let kn = Nametab.locate_tactic id in
+ let kn = Tacenv.locate_tactic id in
let entries = Tacenv.ltac_entries () in
let tac = KNmap.find kn entries in
let filter mp =
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 56b3d480eb..ae4857a77c 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -56,10 +56,18 @@ Section MakeRingPol.
Infix "?=!" := ceqb. Notation "[ x ]" := (phi x).
(* Useful tactics *)
- Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
- Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
+ Proof. exact (Radd_ext Reqe). Qed.
+
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
+ Proof. exact (Rmul_ext Reqe). Qed.
+
+ Add Morphism ropp with signature (req ==> req) as ropp_ext.
+ Proof. exact (Ropp_ext Reqe). Qed.
+
+ Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
+ Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
+
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 56b985aa34..88e2cb1da5 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -56,11 +56,16 @@ Let rI_neq_rO := AFth.(AF_1_neq_0).
Let rdiv_def := AFth.(AFdiv_def).
Let rinv_l := AFth.(AFinv_l).
-Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed.
-Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed.
-Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed.
-Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
-Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed.
+Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
+Proof. exact (Radd_ext Reqe). Qed.
+Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
+Proof. exact (Rmul_ext Reqe). Qed.
+Add Morphism ropp with signature (req ==> req) as ropp_ext.
+Proof. exact (Ropp_ext Reqe). Qed.
+Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
+Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
+Add Morphism rinv with signature (req ==> req) as rinv_ext.
+Proof. exact SRinv_ext. Qed.
Let eq_trans := Setoid.Seq_trans _ _ Rsth.
Let eq_sym := Setoid.Seq_sym _ _ Rsth.
@@ -1609,9 +1614,12 @@ Section Complete.
Variable Rsth : Setoid_Theory R req.
Add Setoid R req Rsth as R_setoid3.
Variable Reqe : ring_eq_ext radd rmul ropp req.
- Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
+ Proof. exact (Radd_ext Reqe). Qed.
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
+ Proof. exact (Rmul_ext Reqe). Qed.
+ Add Morphism ropp with signature (req ==> req) as ropp_ext3.
+ Proof. exact (Ropp_ext Reqe). Qed.
Section AlmostField.
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 98ffff4322..bd4e94687d 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -51,9 +51,12 @@ Section ZMORPHISM.
Add Setoid R req Rsth as R_setoid3.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
- Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
+ Proof. exact (Radd_ext Reqe). Qed.
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
+ Proof. exact (Rmul_ext Reqe). Qed.
+ Add Morphism ropp with signature (req ==> req) as ropp_ext3.
+ Proof. exact (Ropp_ext Reqe). Qed.
Fixpoint gen_phiPOS1 (p:positive) : R :=
match p with
@@ -103,7 +106,8 @@ Section ZMORPHISM.
Section ALMOST_RING.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
- Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3.
+ Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
@@ -151,7 +155,8 @@ Section ZMORPHISM.
Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
Let ARth := Rth_ARth Rsth Reqe Rth.
- Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4.
+ Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
@@ -265,8 +270,10 @@ Section NMORPHISM.
Let rsub := (@SRsub R radd).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
- Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext4.
+ Proof. exact (Radd_ext Reqe). Qed.
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4.
+ Proof. exact (Rmul_ext Reqe). Qed.
Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
Definition gen_phiN1 x :=
@@ -377,12 +384,16 @@ Section NWORDMORPHISM.
Add Setoid R req Rsth as R_setoid5.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
- Add Morphism radd : radd_ext5. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext5. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext5. exact (Ropp_ext Reqe). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
+ Proof. exact (Radd_ext Reqe). Qed.
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5.
+ Proof. exact (Rmul_ext Reqe). Qed.
+ Add Morphism ropp with signature (req ==> req) as ropp_ext5.
+ Proof. exact (Ropp_ext Reqe). Qed.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
- Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7.
+ Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
@@ -557,10 +568,14 @@ Section GEN_DIV.
(* Useful tactics *)
Add Setoid R req Rsth as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
- Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
- Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
+ Proof. exact (Radd_ext Reqe). Qed.
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
+ Proof. exact (Rmul_ext Reqe). Qed.
+ Add Morphism ropp with signature (req ==> req) as ropp_ext.
+ Proof. exact (Ropp_ext Reqe). Qed.
+ Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
+ Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Definition triv_div x y :=
@@ -859,8 +874,3 @@ Ltac isZcst t :=
(* *)
| _ => constr:(false)
end.
-
-
-
-
-
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index ac54d862c9..a94f8d8df6 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -59,10 +59,18 @@ Section MakeRingPol.
Infix "?=!" := ceqb. Notation "[ x ]" := (phi x).
(* Useful tactics *)
- Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
- Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
+ Proof. exact (Radd_ext Reqe). Qed.
+
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
+ Proof. exact (Rmul_ext Reqe). Qed.
+
+ Add Morphism ropp with signature (req ==> req) as ropp_ext.
+ Proof. exact (Ropp_ext Reqe). Qed.
+
+ Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
+ Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
+
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 8dda5ecd34..335a68d70f 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -254,8 +254,12 @@ Section ALMOST_RING.
Section SEMI_RING.
Variable SReqe : sring_eq_ext radd rmul req.
- Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed.
- Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext1.
+ Proof. exact (SRadd_ext SReqe). Qed.
+
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext1.
+ Proof. exact (SRmul_ext SReqe). Qed.
+
Variable SRth : semi_ring_theory 0 1 radd rmul req.
(** Every semi ring can be seen as an almost ring, by taking :
@@ -323,9 +327,15 @@ Section ALMOST_RING.
Notation "- x" := (ropp x).
Variable Reqe : ring_eq_ext radd rmul ropp req.
- Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed.
+
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext2.
+ Proof. exact (Radd_ext Reqe). Qed.
+
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext2.
+ Proof. exact (Rmul_ext Reqe). Qed.
+
+ Add Morphism ropp with signature (req ==> req) as ropp_ext2.
+ Proof. exact (Ropp_ext Reqe). Qed.
Section RING.
Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
@@ -393,14 +403,25 @@ Section ALMOST_RING.
Notation "?=!" := ceqb. Notation "[ x ]" := (phi x).
Variable Csth : Equivalence ceq.
Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
+
Add Setoid C ceq Csth as C_setoid.
- Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed.
- Add Morphism cmul : cmul_ext. exact (Rmul_ext Ceqe). Qed.
- Add Morphism copp : copp_ext. exact (Ropp_ext Ceqe). Qed.
+
+ Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext.
+ Proof. exact (Radd_ext Ceqe). Qed.
+
+ Add Morphism cmul with signature (ceq ==> ceq ==> ceq) as cmul_ext.
+ Proof. exact (Rmul_ext Ceqe). Qed.
+
+ Add Morphism copp with signature (ceq ==> ceq) as copp_ext.
+ Proof. exact (Ropp_ext Ceqe). Qed.
+
Variable Cth : ring_theory cO cI cadd cmul csub copp ceq.
Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi.
Variable phi_ext : forall x y, ceq x y -> [x] == [y].
- Add Morphism phi : phi_ext1. exact phi_ext. Qed.
+
+ Add Morphism phi with signature (ceq ==> req) as phi_ext1.
+ Proof. exact phi_ext. Qed.
+
Lemma Smorph_opp x : [-!x] == -[x].
Proof.
rewrite <- (Rth.(Radd_0_l) [-!x]).
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index cf5fdf3184..d37c676e38 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -814,8 +814,8 @@ let ssr_n_tac seed n gl =
let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in
let fail msg = CErrors.user_err (Pp.str msg) in
let tacname =
- try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name))
- with Not_found -> try Nametab.locate_tactic (ssrqid name)
+ try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name))
+ with Not_found -> try Tacenv.locate_tactic (ssrqid name)
with Not_found ->
if n = -1 then fail "The ssreflect library was not loaded"
else fail ("The tactic "^name^" was not found") in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 1e1a986daa..7b591feada 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1554,8 +1554,8 @@ END
let ssrautoprop gl =
try
let tacname =
- try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
- with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in
+ try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
+ with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:56:01 +0000