aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg52
-rw-r--r--plugins/ltac/g_auto.mlg5
-rw-r--r--plugins/ltac/g_ltac.mlg18
-rw-r--r--plugins/ltac/g_obligations.mlg5
-rw-r--r--plugins/ltac/g_rewrite.mlg94
-rw-r--r--plugins/ltac/rewrite.ml94
-rw-r--r--plugins/ltac/rewrite.mli11
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--plugins/ltac/tacenv.ml6
-rw-r--r--plugins/ltac/tacenv.mli4
-rw-r--r--plugins/ltac/tacintern.ml17
-rw-r--r--plugins/ltac/tacintern.mli5
-rw-r--r--plugins/ltac/tacinterp.ml6
14 files changed, 160 insertions, 161 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index b660865e8b..85fb0c73c9 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -30,7 +30,7 @@ open Namegen
open Tactypes
open Tactics
open Proofview.Notations
-open Vernacinterp
+open Attributes
let wit_hyp = wit_var
@@ -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:atts.polymorphic 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:atts.polymorphic bl o (Some t) l }
-| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
- { add_rewrite_hint ~poly:atts.polymorphic ["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: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,45 +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 }
-> {
- let open Vernacinterp in
- add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
-> {
- let open Vernacinterp in
- add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
-> {
- let open Vernacinterp in
- add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
-> {
- let open Vernacinterp in
- add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
-> {
- let open Vernacinterp in
- add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
-> {
- let open Vernacinterp in
- add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac }
+ add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac }
END
(**********************************************************************)
@@ -855,9 +849,9 @@ END
TACTIC EXTEND transparent_abstract
| [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl ->
- Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end }
+ Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end }
| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl ->
- Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end }
+ Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end }
END
(* ********************************************************************* *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index c07b653f3a..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 Vernacinterp 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 atts.locality)
+ 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 d62f985350..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,12 +499,12 @@ 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 open Vernacinterp 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
+ Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
}
END
@@ -545,13 +546,12 @@ 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 open Vernacinterp in
- let deprecation = atts.deprecated in
- Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
+ } -> {
+ 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 26f2b08d3a..aa78fb5d1e 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -131,10 +131,9 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
- let open Vernacinterp in
+| #[ locality = Attributes.locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
set_default_tactic
- (Locality.make_section_locality atts.locality)
+ (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 3e47724c4c..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 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 a aeq n (Some lemma1) None None }
- | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] ->
- { declare_relation 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 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 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 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 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 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 ~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 ~binders:b a aeq n (Some lemma1) None None }
- | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
- { declare_relation ~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 ~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 ~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 ~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 ~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 ~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) ] ->
- { let open Vernacinterp in
- add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+ | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ {
+ add_setoid atts [] a aeq t n;
}
- | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
- { let open Vernacinterp in
- add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(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 }
- -> { let open Vernacinterp in
- add_morphism_infer (not (Locality.make_section_locality atts.locality)) 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) }
- -> { let open Vernacinterp in
- add_morphism (not (Locality.make_section_locality atts.locality)) [] 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) }
- -> { let open Vernacinterp in
- add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+ -> {
+ add_morphism atts binders m s n;
}
END
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9f7669f1d5..7d917c58fe 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -43,6 +43,14 @@ module NamedDecl = Context.Named.Declaration
(** Typeclass-based generalized rewriting. *)
+type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }
+
+let rewrite_attributes =
+ let open Attributes.Notations in
+ Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
+ let global = not (Locality.make_section_locality locality) in
+ Attributes.Notations.return { polymorphic; program; global }
+
(** Constants used by the tactic. *)
let classes_dirpath =
@@ -1492,7 +1500,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
if not (Evd.is_defined acc ev) then
user_err ~hdr:"rewrite"
(str "Unsolved constraint remaining: " ++ spc () ++
- Termops.pr_evar_info (Evd.find acc ev))
+ Termops.pr_evar_info env acc (Evd.find acc ev))
else Evd.remove acc ev)
cstrs evars'
in
@@ -1776,67 +1784,65 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
-let anew_instance global binders instance fields =
- let program_mode = Flags.is_program_mode () in
- let poly = Flags.is_universe_polymorphism () in
- new_instance ~program_mode poly
+let anew_instance atts binders instance fields =
+ let program_mode = atts.program in
+ new_instance ~program_mode atts.polymorphic
binders instance (Some (true, CAst.make @@ CRecord (fields)))
- ~global ~generalize:false ~refine:false Hints.empty_hint_info
+ ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
-let declare_instance_refl global binders a aeq n lemma =
+let declare_instance_refl atts binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
- in anew_instance global binders instance
+ in anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
-let declare_instance_sym global binders a aeq n lemma =
+let declare_instance_sym atts binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
- in anew_instance global binders instance
+ in anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "symmetry"),lemma)]
-let declare_instance_trans global binders a aeq n lemma =
+let declare_instance_trans atts binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
- in anew_instance global binders instance
+ in anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "transitivity"),lemma)]
-let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
- let global = not (Locality.make_section_locality locality) in
let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
- in ignore(anew_instance global binders instance []);
+ in ignore(anew_instance atts binders instance []);
match (refl,symm,trans) with
(None, None, None) -> ()
| (Some lemma1, None, None) ->
- ignore (declare_instance_refl global binders a aeq n lemma1)
+ ignore (declare_instance_refl atts binders a aeq n lemma1)
| (None, Some lemma2, None) ->
- ignore (declare_instance_sym global binders a aeq n lemma2)
+ ignore (declare_instance_sym atts binders a aeq n lemma2)
| (None, None, Some lemma3) ->
- ignore (declare_instance_trans global binders a aeq n lemma3)
+ ignore (declare_instance_trans atts binders a aeq n lemma3)
| (Some lemma1, Some lemma2, None) ->
- ignore (declare_instance_refl global binders a aeq n lemma1);
- ignore (declare_instance_sym global binders a aeq n lemma2)
+ ignore (declare_instance_refl atts binders a aeq n lemma1);
+ ignore (declare_instance_sym atts binders a aeq n lemma2)
| (Some lemma1, None, Some lemma3) ->
- let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
- let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+ let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+ let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
in ignore(
- anew_instance global binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
(qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)])
| (None, Some lemma2, Some lemma3) ->
- let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
- let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+ let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+ let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
in ignore(
- anew_instance global binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
(qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)])
| (Some lemma1, Some lemma2, Some lemma3) ->
- let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
- let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
- let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+ let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+ let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+ let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
- anew_instance global binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)])
@@ -1935,15 +1941,15 @@ 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 =
+let add_setoid atts 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
- let _lemma_trans = declare_instance_trans global binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+ let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+ let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+ let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
- anew_instance global binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
@@ -1958,26 +1964,26 @@ 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 =
+let add_morphism_infer atts m n =
warn_add_morphism_deprecated ?loc:m.CAst.loc ();
init_setoid ();
- let poly = Flags.is_universe_polymorphism () in
+ (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
let instance_id = add_suffix n "_Proper" in
let env = Global.env () in
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
if Lib.is_modtype () then
- let uctx = UState.const_univ_entry ~poly uctx in
+ let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
(None,(instance,uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
else
- let kind = Decl_kinds.Global, poly,
+ let kind = Decl_kinds.Global, atts.polymorphic,
Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -1985,7 +1991,7 @@ let add_morphism_infer glob m n =
| Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance
(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
- glob (ConstRef cst));
+ atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
in
@@ -1995,9 +2001,8 @@ let add_morphism_infer glob m n =
Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
ignore (Pfedit.by (Tacinterp.interp tac))) ()
-let add_morphism glob binders m s n =
+let add_morphism atts binders m s n =
init_setoid ();
- let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
let instance =
(((CAst.make @@ Name instance_id),None), Explicit,
@@ -2006,8 +2011,7 @@ let add_morphism glob binders m s n =
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- let program_mode = Flags.is_program_mode () in
- ignore(new_instance ~program_mode ~global:glob poly binders instance
+ ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
(Some (true, CAst.make @@ CRecord []))
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 0d014a0bf3..4f46e78c71 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -19,6 +19,9 @@ open Tacinterp
(** TODO: document and clean me! *)
+type rewrite_attributes
+val rewrite_attributes : rewrite_attributes Attributes.attribute
+
type unary_strategy =
Subterms | Subterm | Innermost | Outermost
| Bottomup | Topdown | Progress | Try | Any | Repeat
@@ -77,18 +80,18 @@ val cl_rewrite_clause :
val is_applied_rewrite_relation :
env -> evar_map -> rel_context -> constr -> types option
-val declare_relation : ?locality:bool ->
+val declare_relation : rewrite_attributes ->
?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
constr_expr option -> constr_expr option -> constr_expr option -> unit
val add_setoid :
- bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
+ rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
Id.t -> unit
-val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit
val add_morphism :
- bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
+ rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 16cff420bd..0f88734caf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -353,7 +353,7 @@ let extend_atomic_tactic name entries =
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
- | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
+ | Some def -> Tacintern.intern_tactic_or_tacarg (Genintern.empty_glob_sign Environ.empty_env) def
in
try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 5b4bedb50a..c93d6251e0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,7 +12,7 @@
open Vernacexpr
open Tacexpr
-open Vernacinterp
+open Attributes
(** {5 Tactic Definitions} *)
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index a88285c9ee..d5f22b2c72 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -55,7 +55,7 @@ type alias = KerName.t
type alias_tactic =
{ alias_args: Id.t list;
alias_body: glob_tactic_expr;
- alias_deprecation: Vernacinterp.deprecation option;
+ alias_deprecation: Attributes.deprecation option;
}
let alias_map = Summary.ref ~name:"tactic-alias"
@@ -121,7 +121,7 @@ type ltac_entry = {
tac_for_ml : bool;
tac_body : glob_tactic_expr;
tac_redef : ModPath.t list;
- tac_deprecation : Vernacinterp.deprecation option
+ tac_deprecation : Attributes.deprecation option
}
let mactab =
@@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) =
let classify_md (local, _, _, _, _ as o) = Substitute o
let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
- Vernacinterp.deprecation option -> obj =
+ Attributes.deprecation option -> 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 d5d36c97fa..5b98daf383 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,7 +12,7 @@ open Names
open Libnames
open Tacexpr
open Geninterp
-open Vernacinterp
+open Attributes
(** This module centralizes the various ways of registering tactics. *)
@@ -33,7 +33,7 @@ type alias = KerName.t
type alias_tactic =
{ alias_args: Id.t list;
alias_body: glob_tactic_expr;
- alias_deprecation: Vernacinterp.deprecation option;
+ alias_deprecation: deprecation option;
}
(** Contents of a tactic notation *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 55412c74bb..ebec3c887c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -44,9 +44,9 @@ type glob_sign = Genintern.glob_sign = {
(* ltac variables and the subset of vars introduced by Intro/Let/... *)
genv : Environ.env;
extra : Genintern.Store.t;
+ intern_sign : Genintern.intern_variable_status;
}
-let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env
let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
(* We have identifier <| global_reference <| constr *)
@@ -83,7 +83,8 @@ let intern_hyp ist ({loc;v=id} as locid) =
else if find_ident id ist then
make id
else
- Pretype_errors.error_var_not_found ?loc id
+ CErrors.user_err ?loc Pp.(str "Hypothesis" ++ spc () ++ Id.print id ++ spc() ++
+ str "was not found in the current environment.")
let intern_or_var f ist = function
| ArgVar locid -> ArgVar (intern_hyp ist locid)
@@ -121,15 +122,15 @@ let warn_deprecated_tactic =
CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
(fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
strbrk " is deprecated" ++
- pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
- str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+ pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+ str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
let warn_deprecated_alias =
CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
(fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
strbrk " is deprecated since" ++
- pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
- str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+ pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+ str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
let intern_isolated_global_tactic_reference qid =
let loc = qid.CAst.loc in
@@ -209,7 +210,7 @@ let intern_binding_name ist x =
and if a term w/o ltac vars, check the name is indeed quantified *)
x
-let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
+let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra; intern_sign} c =
let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
let ltacvars = {
@@ -218,7 +219,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
ltac_extra = extra;
} in
let c' =
- warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c
+ warn (Constrintern.intern_core scope ~pattern_mode ~ltacvars env Evd.(from_env env) intern_sign) c
in
(c',if !strict_check then None else Some c)
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 9146fced2d..178f6af71d 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -21,12 +21,11 @@ type glob_sign = Genintern.glob_sign = {
ltacvars : Id.Set.t;
genv : Environ.env;
extra : Genintern.Store.t;
+ intern_sign : Genintern.intern_variable_status;
}
-val fully_empty_glob_sign : glob_sign
-
val make_empty_glob_sign : unit -> glob_sign
- (** same as [fully_empty_glob_sign], but with [Global.env()] as
+ (** build an empty [glob_sign] using [Global.env()] as
environment *)
(** Main globalization functions *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b60b77595b..2a046a3e65 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -686,7 +686,7 @@ let interp_may_eval f ist env sigma = function
| ConstrContext ({loc;v=s},c) ->
(try
let (sigma,ic) = f ist env sigma c in
- let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
+ let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in
let ctxt = EConstr.Unsafe.to_constr ctxt in
let ic = EConstr.Unsafe.to_constr ic in
let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
@@ -1078,7 +1078,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
push_trace(None,call) ist >>= fun trace ->
Profile_ltac.do_profile "eval_tactic:TacAbstract" trace
(catch_error_tac trace begin
- Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT
+ Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT
(Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t)
end end)
| TacThen (t1,t) ->
@@ -2024,7 +2024,7 @@ let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k
let interp_redexp env sigma r =
let ist = default_ist () in
- let gist = { fully_empty_glob_sign with genv = env; } in
+ let gist = Genintern.empty_glob_sign env in
interp_red_expr ist env sigma (intern_red_expr gist r)
(***************************************************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 11:15:13 +0000