aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/InitialRing.v2
-rw-r--r--plugins/setoid_ring/Ring_polynom.v2
-rw-r--r--plugins/setoid_ring/g_newring.mlg38
-rw-r--r--plugins/setoid_ring/newring.ml30
-rw-r--r--plugins/setoid_ring/newring.mli5
5 files changed, 39 insertions, 38 deletions
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 4886c8b9aa..9be2535a3f 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -105,7 +105,7 @@ Section ZMORPHISM.
Proof.
constructor.
destruct c;intros;try discriminate.
- injection H as <-.
+ injection H as [= <-].
simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
Qed.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index f7cb6b688b..c5d396427b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -894,7 +894,7 @@ Section MakeRingPol.
revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
- discriminate.
- assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
- * injection H as <-. rewrite <- PSubstL1_ok; intuition.
+ * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition.
* now apply IH.
Qed.
diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg
index 6be556b2ae..5dfead2d7e 100644
--- a/plugins/setoid_ring/g_newring.mlg
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -13,8 +13,6 @@
open Ltac_plugin
open Pp
open Util
-open Libnames
-open Printer
open Newring_ast
open Newring
open Stdarg
@@ -85,21 +83,10 @@ END
VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
| [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
- { let l = match l with None -> [] | Some l -> l in add_theory id t l }
- | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
- fun ~pstate ->
- Feedback.msg_notice (strbrk "The following ring structures have been declared:");
- Spmap.iter (fun fn fi ->
- (* We should use the global env here as this shouldn't contain proof
- data, however preserving behavior as requested in review. *)
- let sigma, env = Option.cata Pfedit.get_current_context
- (let e = Global.env () in Evd.from_env e, e) pstate in
- Feedback.msg_notice (hov 2
- (Ppconstr.pr_id (Libnames.basename fn)++spc()++
- str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
- str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
- ) !from_name;
- pstate }
+ { add_theory id t (Option.default [] l) }
+ | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
+ print_rings ()
+ }
END
TACTIC EXTEND ring_lookup
@@ -135,20 +122,9 @@ END
VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
| [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
{ let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
-| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
- fun ~pstate ->
- Feedback.msg_notice (strbrk "The following field structures have been declared:");
- Spmap.iter (fun fn fi ->
- (* We should use the global env here as this shouldn't
- contain proof data. *)
- let sigma, env = Option.cata Pfedit.get_current_context
- (let e = Global.env () in Evd.from_env e, e) pstate in
- Feedback.msg_notice (hov 2
- (Ppconstr.pr_id (Libnames.basename fn)++spc()++
- str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
- str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
- ) !field_from_name;
- pstate }
+| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
+ print_fields ()
+ }
END
TACTIC EXTEND field_lookup
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b02b97f656..8e7b045b8e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,9 +153,11 @@ let decl_constant na univs c =
let open Constr in
let vars = CVars.universes_of_constr c in
let univs = UState.restrict_universe_context univs vars in
- let univs = Monomorphic_entry univs in
+ let () = Declare.declare_universe_context false univs in
+ let types = (Typeops.infer (Global.env ()) c).uj_type in
+ let univs = Monomorphic_entry Univ.ContextSet.empty in
mkConst(declare_constant (Id.of_string na)
- (DefinitionEntry (definition_entry ~opaque:true ~univs c),
+ (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
IsProof Lemma))
(* Calling a global tactic *)
@@ -327,6 +329,18 @@ module Cmap = Map.Make(Constr)
let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
+let print_rings () =
+ Feedback.msg_notice (strbrk "The following ring structures have been declared:");
+ Spmap.iter (fun fn fi ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Feedback.msg_notice
+ (hov 2
+ (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+ str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
+ str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
+ ) !from_name
+
let ring_for_carrier r = Cmap.find r !from_carrier
let find_ring_structure env sigma l =
@@ -824,6 +838,18 @@ let dest_field env evd th_spec =
let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
+let print_fields () =
+ Feedback.msg_notice (strbrk "The following field structures have been declared:");
+ Spmap.iter (fun fn fi ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Feedback.msg_notice
+ (hov 2
+ (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+ str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
+ str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
+ ) !field_from_name
+
let field_for_carrier r = Cmap.find r !field_from_carrier
let find_field_structure env sigma l =
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index fcd04a2e73..3a21a82c5c 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -10,7 +10,6 @@
open Names
open EConstr
-open Libnames
open Constrexpr
open Newring_ast
@@ -23,7 +22,7 @@ val add_theory :
constr_expr ->
constr_expr ring_mod list -> unit
-val from_name : ring_info Spmap.t ref
+val print_rings : unit -> unit
val ring_lookup :
Geninterp.Val.t ->
@@ -35,7 +34,7 @@ val add_field_theory :
constr_expr ->
constr_expr field_mod list -> unit
-val field_from_name : field_info Spmap.t ref
+val print_fields : unit -> unit
val field_lookup :
Geninterp.Val.t ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 13:43:00 +0000