aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/g_ground.mlg2
-rw-r--r--plugins/ltac/extratactics.mlg20
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg14
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg10
-rw-r--r--plugins/ssr/ssrvernac.mlg2
-rw-r--r--plugins/syntax/g_numeral.mlg3
8 files changed, 27 insertions, 28 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 5a4cda54b2..14a3acad57 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -76,7 +76,7 @@ VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
let open Attributes in
set_default_solver
- (Locality.make_section_locality atts.locality)
+ (Locality.make_section_locality (only_locality atts))
(Tacintern.glob_tactic t)
}
END
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 11b970d2ef..cab7281719 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -322,14 +322,14 @@ let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater
VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint }
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
- { add_rewrite_hint ~poly:atts.polymorphic bl o None l }
+ { add_rewrite_hint ~poly:(only_polymorphism atts) bl o None l }
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident_list(bl) ] ->
- { add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l }
+ { add_rewrite_hint ~poly:(only_polymorphism atts) bl o (Some t) l }
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
- { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l }
+ { add_rewrite_hint ~poly:(only_polymorphism atts) ["core"] o None l }
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
- { add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l }
+ { add_rewrite_hint ~poly:(only_polymorphism atts) ["core"] o (Some t) l }
END
(**********************************************************************)
@@ -414,36 +414,36 @@ VERNAC COMMAND EXTEND DeriveInversionClear
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac }
+ add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_clear_tac }
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
-> {
- add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac }
+ add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_clear_tac }
END
VERNAC COMMAND EXTEND DeriveInversion
| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac }
+ add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_tac }
| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
-> {
- add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac }
+ add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_tac }
END
VERNAC COMMAND EXTEND DeriveDependentInversion
| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac }
+ add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_tac }
END
VERNAC COMMAND EXTEND DeriveDependentInversionClear
| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac }
+ add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_clear_tac }
END
(**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 65fa34d712..e8b5e900dd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -242,7 +242,7 @@ VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
let open Attributes in
let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
- Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
+ Hints.add_hints ~local:(Locality.make_section_locality (only_locality atts))
(match dbnames with None -> ["core"] | Some l -> l) entry;
}
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index f1f3ae74e5..f8842b201c 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -500,10 +500,10 @@ END
VERNAC COMMAND EXTEND VernacTacticNotation
| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
{ VtSideff [], VtNow } ->
- { let open Attributes in
- let n = Option.default 0 n in
- let deprecation = atts.deprecated in
- Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
+ {
+ let n = Option.default 0 n in
+ let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in
+ Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
}
END
@@ -549,9 +549,9 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
VtSideff (List.map (function
| TacticDefinition ({CAst.v=r},_) -> r
| TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
- } -> { let open Attributes in
- let deprecation = atts.deprecated in
- Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
+ } -> {
+ let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in
+ Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l;
}
END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 32dccf2e83..030b1b5410 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -133,7 +133,7 @@ END
VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
| [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
set_default_tactic
- (Locality.make_section_locality atts.Attributes.locality)
+ (Locality.make_section_locality (Attributes.only_locality atts))
(Tacintern.glob_tactic t);
}
END
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 3f12e0e9f9..7880587366 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -273,28 +273,28 @@ END
VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
| [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
- add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+ add_setoid (not (Locality.make_section_locality (only_locality atts))) [] a aeq t n;
}
| [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
- add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+ add_setoid (not (Locality.make_section_locality (only_locality atts))) binders a aeq t n;
}
| [ "Add" "Morphism" constr(m) ":" ident(n) ]
(* This command may or may not open a goal *)
=> { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
-> {
- add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
+ add_morphism_infer (not (Locality.make_section_locality (only_locality atts))) m n;
}
| [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
=> { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-> {
- add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
+ add_morphism (not (Locality.make_section_locality (only_locality atts))) [] m s n;
}
| [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
=> { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-> {
- add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+ add_morphism (not (Locality.make_section_locality (only_locality atts))) binders m s n;
}
END
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 2f44624d36..2774b843aa 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -173,7 +173,7 @@ VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
| [ "Prenex" "Implicits" ne_global_list(fl) ]
-> {
let open Attributes in
- let locality = Locality.make_section_locality atts.locality in
+ let locality = Locality.make_section_locality (only_locality atts) in
List.iter (declare_one_prenex_implicit locality) fl;
}
END
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 54764d541f..e70edd56cb 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -16,7 +16,6 @@ open Notation
open Numeral
open Pp
open Names
-open Attributes
open Ltac_plugin
open Stdarg
open Pcoq.Prim
@@ -38,5 +37,5 @@ END
VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
| [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
ident(sc) numnotoption(o) ] ->
- { vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o }
+ { vernac_numeral_notation (Locality.make_module_locality (Attributes.only_locality atts)) ty f g (Id.to_string sc) o }
END
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:35:14 +0000