aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/g_newring.mlg (renamed from plugins/setoid_ring/g_newring.ml4)82
-rw-r--r--plugins/setoid_ring/newring.ml13
2 files changed, 58 insertions, 37 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.mlg
index 4ea0b30bd7..3ddea7eb30 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Ltac_plugin
open Pp
open Util
@@ -20,15 +22,19 @@ open Tacarg
open Pcoq.Constr
open Pltac
+}
+
DECLARE PLUGIN "newring_plugin"
TACTIC EXTEND protect_fv
- [ "protect_fv" string(map) "in" ident(id) ] ->
- [ protect_tac_in map id ]
+| [ "protect_fv" string(map) "in" ident(id) ] ->
+ { protect_tac_in map id }
| [ "protect_fv" string(map) ] ->
- [ protect_tac map ]
+ { protect_tac map }
END
+{
+
open Pptactic
open Ppconstr
@@ -46,35 +52,41 @@ let pr_ring_mod = function
| Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t
| Div_spec t -> str "div" ++ pr_arg pr_constr_expr t
+}
+
VERNAC ARGUMENT EXTEND ring_mod
- PRINTED BY pr_ring_mod
- | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
- | [ "abstract" ] -> [ Ring_kind Abstract ]
- | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
- | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
- | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
- | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
- | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ]
- | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ]
- | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ]
+ PRINTED BY { pr_ring_mod }
+ | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) }
+ | [ "abstract" ] -> { Ring_kind Abstract }
+ | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) }
+ | [ "constants" "[" tactic(cst_tac) "]" ] -> { Const_tac(CstTac cst_tac) }
+ | [ "closed" "[" ne_global_list(l) "]" ] -> { Const_tac(Closed l) }
+ | [ "preprocess" "[" tactic(pre) "]" ] -> { Pre_tac pre }
+ | [ "postprocess" "[" tactic(post) "]" ] -> { Post_tac post }
+ | [ "setoid" constr(sth) constr(ext) ] -> { Setoid(sth,ext) }
+ | [ "sign" constr(sign_spec) ] -> { Sign_spec sign_spec }
| [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] ->
- [ Pow_spec (Closed l, pow_spec) ]
+ { Pow_spec (Closed l, pow_spec) }
| [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
- [ Pow_spec (CstTac cst_tac, pow_spec) ]
- | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ]
+ { Pow_spec (CstTac cst_tac, pow_spec) }
+ | [ "div" constr(div_spec) ] -> { Div_spec div_spec }
END
+{
+
let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l)
+}
+
VERNAC ARGUMENT EXTEND ring_mods
- PRINTED BY pr_ring_mods
- | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> [ mods ]
+ PRINTED BY { pr_ring_mods }
+ | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods }
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]
- | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
+ { let l = match l with None -> [] | Some l -> l in add_theory id t l }
+ | [ "Print" "Rings" ] => {Vernac_classifier.classify_as_query} -> {
Feedback.msg_notice (strbrk "The following ring structures have been declared:");
Spmap.iter (fun fn fi ->
let sigma, env = Pfedit.get_current_context () in
@@ -82,35 +94,43 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
(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 ]
+ ) !from_name }
END
TACTIC EXTEND ring_lookup
| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
- [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ]
+ { let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t }
END
+{
+
let pr_field_mod = function
| Ring_mod m -> pr_ring_mod m
| Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj
+}
+
VERNAC ARGUMENT EXTEND field_mod
- PRINTED BY pr_field_mod
- | [ ring_mod(m) ] -> [ Ring_mod m ]
- | [ "completeness" constr(inj) ] -> [ Inject inj ]
+ PRINTED BY { pr_field_mod }
+ | [ ring_mod(m) ] -> { Ring_mod m }
+ | [ "completeness" constr(inj) ] -> { Inject inj }
END
+{
+
let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l)
+}
+
VERNAC ARGUMENT EXTEND field_mods
- PRINTED BY pr_field_mods
- | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> [ mods ]
+ PRINTED BY { pr_field_mods }
+ | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods }
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 ]
-| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
+ { let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
+| [ "Print" "Fields" ] => {Vernac_classifier.classify_as_query} -> {
Feedback.msg_notice (strbrk "The following field structures have been declared:");
Spmap.iter (fun fn fi ->
let sigma, env = Pfedit.get_current_context () in
@@ -118,10 +138,10 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
(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 ]
+ ) !field_from_name }
END
TACTIC EXTEND field_lookup
| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
- [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
+ { let (t,l) = List.sep_last lt in field_lookup f lH l t }
END
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 85e759d152..a2dce621d9 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -8,6 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+module CVars = Vars
open Ltac_plugin
open Pp
open Util
@@ -150,8 +151,8 @@ let ic_unsafe c = (*FIXME remove *)
let decl_constant na univs c =
let open Constr in
- let vars = Univops.universes_of_constr c in
- let univs = Univops.restrict_universe_context univs vars in
+ let vars = CVars.universes_of_constr c in
+ let univs = UState.restrict_universe_context univs vars in
let univs = Monomorphic_const_entry univs in
mkConst(declare_constant (Id.of_string na)
(DefinitionEntry (definition_entry ~opaque:true ~univs c),
@@ -163,7 +164,7 @@ let ltac_call tac (args:glob_tactic_arg list) =
let dummy_goal env sigma =
let (gl,_,sigma) =
- Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
+ Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in
{Evd.it = gl; Evd.sigma = sigma}
let constr_of evd v = match Value.to_constr v with
@@ -205,7 +206,7 @@ let exec_tactic env evd n f args =
let nf c = constr_of evd c in
Array.map nf !tactic_res, Evd.universe_context_set evd
-let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n)))
+let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)))
let gen_reference n = lazy (Coqlib.lib_ref n)
let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory"
@@ -250,7 +251,7 @@ let plugin_modules =
]
let my_constant c =
- lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
+ lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
[@@ocaml.warning "-3"]
let my_reference c =
lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
@@ -900,7 +901,7 @@ let ftheory_to_obj : field_info -> obj =
let field_equality evd r inv req =
match EConstr.kind !evd req with
| App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
- let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in
+ let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in
let c = EConstr.of_constr c in
mkApp(c,[|r;r;inv|])
| _ ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 02:59:37 +0000