aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg40
-rw-r--r--plugins/ltac/g_auto.mlg5
-rw-r--r--plugins/ltac/g_ltac.mlg8
-rw-r--r--plugins/ltac/g_obligations.mlg4
-rw-r--r--plugins/ltac/g_rewrite.mlg84
5 files changed, 70 insertions, 71 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index cab7281719..73ec94f75f 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -321,15 +321,15 @@ 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:(only_polymorphism atts) bl o None l }
-| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
+| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
+ { add_rewrite_hint ~poly:polymorphic bl o None l }
+| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident_list(bl) ] ->
- { add_rewrite_hint ~poly:(only_polymorphism atts) bl o (Some t) l }
-| [ "Hint" "Rewrite" orient(o) ne_constr_list(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:(only_polymorphism atts) ["core"] o (Some t) l }
+ { add_rewrite_hint ~poly:polymorphic bl o (Some t) l }
+| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+ { add_rewrite_hint ~poly:polymorphic ["core"] o None l }
+| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+ { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l }
END
(**********************************************************************)
@@ -411,39 +411,39 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
END*)
VERNAC COMMAND EXTEND DeriveInversionClear
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_clear_tac }
+ add_inversion_lemma_exn ~poly:polymorphic na c s false inv_clear_tac }
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
+| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
-> {
- add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_clear_tac }
+ add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_clear_tac }
END
VERNAC COMMAND EXTEND DeriveInversion
-| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_tac }
+ add_inversion_lemma_exn ~poly:polymorphic na c s false inv_tac }
-| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
+| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
-> {
- add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_tac }
+ add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_tac }
END
VERNAC COMMAND EXTEND DeriveDependentInversion
-| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_tac }
+ add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_tac }
END
VERNAC COMMAND EXTEND DeriveDependentInversionClear
-| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> { seff na }
-> {
- add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_clear_tac }
+ add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac }
END
(**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index e8b5e900dd..5af393a3e5 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -239,10 +239,9 @@ ARGUMENT EXTEND opthints
END
VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
- let open Attributes in
+| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
- Hints.add_hints ~local:(Locality.make_section_locality (only_locality atts))
+ Hints.add_hints ~local:(Locality.make_section_locality locality)
(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 f8842b201c..c58c8556c5 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -22,6 +22,7 @@ open Genarg
open Genredexpr
open Tok (* necessary for camlp5 *)
open Names
+open Attributes
open Pcoq
open Pcoq.Prim
@@ -498,11 +499,11 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item
END
VERNAC COMMAND EXTEND VernacTacticNotation
-| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
+| #[ deprecation; locality; ]
+ [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
{ VtSideff [], VtNow } ->
{
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
@@ -545,12 +546,11 @@ PRINTED BY { pr_tacdef_body }
END
VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
-| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
+| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
VtSideff (List.map (function
| TacticDefinition ({CAst.v=r},_) -> r
| TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
} -> {
- 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 030b1b5410..aa78fb5d1e 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -131,9 +131,9 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
+| #[ locality = Attributes.locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
set_default_tactic
- (Locality.make_section_locality (Attributes.only_locality atts))
+ (Locality.make_section_locality locality)
(Tacintern.glob_tactic t);
}
END
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 6a8368d863..1c7220ddc0 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -180,36 +180,36 @@ TACTIC EXTEND setoid_rewrite
END
VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
- | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) (Some lemma2) None }
+ { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
- | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) None None }
- | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None None None }
+ { declare_relation atts a aeq n (Some lemma1) None None }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] ->
+ { declare_relation atts a aeq n None None None }
END
VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
- | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None (Some lemma2) None }
- | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None (Some lemma2) (Some lemma3) }
+ { declare_relation atts a aeq n None (Some lemma2) None }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+ { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
- | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) None (Some lemma3) }
- | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
- | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+ { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None None (Some lemma3) }
+ { declare_relation atts a aeq n None None (Some lemma3) }
END
{
@@ -236,64 +236,64 @@ GRAMMAR EXTEND Gram
END
VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+ { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) None None }
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None None None }
+ { declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
+ { declare_relation atts ~binders:b a aeq n None None None }
END
VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None (Some lemma2) None }
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
+ { declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+ { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+ { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
- { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None None (Some lemma3) }
+ { declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
END
VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
- | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
- add_setoid (Attributes.parse rewrite_attributes atts) [] a aeq t n;
+ add_setoid atts [] a aeq t n;
}
- | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
- add_setoid (Attributes.parse rewrite_attributes atts) binders a aeq t n;
+ add_setoid atts binders a aeq t n;
}
- | [ "Add" "Morphism" constr(m) ":" ident(n) ]
+ | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
(* This command may or may not open a goal *)
=> { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
-> {
- add_morphism_infer (Attributes.parse rewrite_attributes atts) m n;
+ add_morphism_infer atts m n;
}
- | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
+ | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
=> { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-> {
- add_morphism (Attributes.parse rewrite_attributes atts) [] m s n;
+ add_morphism atts [] m s n;
}
- | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
=> { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-> {
- add_morphism (Attributes.parse rewrite_attributes atts) binders m s n;
+ add_morphism atts binders m s n;
}
END
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:06:17 +0000