aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg (renamed from plugins/ltac/coretactics.ml4)184
-rw-r--r--plugins/ltac/extraargs.ml439
-rw-r--r--plugins/ltac/extraargs.mli16
-rw-r--r--plugins/ltac/extratactics.ml421
-rw-r--r--plugins/ltac/g_eqdecide.mlg (renamed from plugins/ltac/g_eqdecide.ml4)8
-rw-r--r--plugins/ltac/g_ltac.ml416
-rw-r--r--plugins/ltac/g_tactic.mlg (renamed from plugins/ltac/g_tactic.ml4)452
-rw-r--r--plugins/ltac/pltac.ml9
-rw-r--r--plugins/ltac/pltac.mli38
-rw-r--r--plugins/ltac/pptactic.ml51
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/taccoerce.ml23
-rw-r--r--plugins/ltac/taccoerce.mli14
-rw-r--r--plugins/ltac/tacentries.ml77
-rw-r--r--plugins/ltac/tacentries.mli19
-rw-r--r--plugins/ltac/tacenv.ml47
-rw-r--r--plugins/ltac/tacenv.mli20
-rw-r--r--plugins/ltac/tacexpr.ml4
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--plugins/ltac/tacintern.ml27
-rw-r--r--plugins/ltac/tacinterp.ml57
-rw-r--r--plugins/ltac/tacinterp.mli1
22 files changed, 596 insertions, 533 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.mlg
index 61525cb49d..6388906f5e 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Util
open Locus
open Tactypes
@@ -18,147 +20,153 @@ open Tacarg
open Names
open Logic
+let wit_hyp = wit_var
+
+}
+
DECLARE PLUGIN "ltac_plugin"
(** Basic tactics *)
TACTIC EXTEND reflexivity
- [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
+| [ "reflexivity" ] -> { Tactics.intros_reflexivity }
END
TACTIC EXTEND exact
- [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
+| [ "exact" casted_constr(c) ] -> { Tactics.exact_no_check c }
END
TACTIC EXTEND assumption
- [ "assumption" ] -> [ Tactics.assumption ]
+| [ "assumption" ] -> { Tactics.assumption }
END
TACTIC EXTEND etransitivity
- [ "etransitivity" ] -> [ Tactics.intros_transitivity None ]
+| [ "etransitivity" ] -> { Tactics.intros_transitivity None }
END
TACTIC EXTEND cut
- [ "cut" constr(c) ] -> [ Tactics.cut c ]
+| [ "cut" constr(c) ] -> { Tactics.cut c }
END
TACTIC EXTEND exact_no_check
- [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
+| [ "exact_no_check" constr(c) ] -> { Tactics.exact_no_check c }
END
TACTIC EXTEND vm_cast_no_check
- [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
+| [ "vm_cast_no_check" constr(c) ] -> { Tactics.vm_cast_no_check c }
END
TACTIC EXTEND native_cast_no_check
- [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
+| [ "native_cast_no_check" constr(c) ] -> { Tactics.native_cast_no_check c }
END
TACTIC EXTEND casetype
- [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
+| [ "casetype" constr(c) ] -> { Tactics.case_type c }
END
TACTIC EXTEND elimtype
- [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ]
+| [ "elimtype" constr(c) ] -> { Tactics.elim_type c }
END
TACTIC EXTEND lapply
- [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
+| [ "lapply" constr(c) ] -> { Tactics.cut_and_apply c }
END
TACTIC EXTEND transitivity
- [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
+| [ "transitivity" constr(c) ] -> { Tactics.intros_transitivity (Some c) }
END
(** Left *)
TACTIC EXTEND left
- [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ]
+| [ "left" ] -> { Tactics.left_with_bindings false NoBindings }
END
TACTIC EXTEND eleft
- [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ]
+| [ "eleft" ] -> { Tactics.left_with_bindings true NoBindings }
END
TACTIC EXTEND left_with
- [ "left" "with" bindings(bl) ] -> [
+| [ "left" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl)
- ]
+ }
END
TACTIC EXTEND eleft_with
- [ "eleft" "with" bindings(bl) ] -> [
+| [ "eleft" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl)
- ]
+ }
END
(** Right *)
TACTIC EXTEND right
- [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ]
+| [ "right" ] -> { Tactics.right_with_bindings false NoBindings }
END
TACTIC EXTEND eright
- [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ]
+| [ "eright" ] -> { Tactics.right_with_bindings true NoBindings }
END
TACTIC EXTEND right_with
- [ "right" "with" bindings(bl) ] -> [
+| [ "right" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl)
- ]
+ }
END
TACTIC EXTEND eright_with
- [ "eright" "with" bindings(bl) ] -> [
+| [ "eright" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl)
- ]
+ }
END
(** Constructor *)
TACTIC EXTEND constructor
- [ "constructor" ] -> [ Tactics.any_constructor false None ]
-| [ "constructor" int_or_var(i) ] -> [
+| [ "constructor" ] -> { Tactics.any_constructor false None }
+| [ "constructor" int_or_var(i) ] -> {
Tactics.constructor_tac false None i NoBindings
- ]
-| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
+ }
+| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac false None i bl in
Tacticals.New.tclDELAYEDWITHHOLES false bl tac
- ]
+ }
END
TACTIC EXTEND econstructor
- [ "econstructor" ] -> [ Tactics.any_constructor true None ]
-| [ "econstructor" int_or_var(i) ] -> [
+| [ "econstructor" ] -> { Tactics.any_constructor true None }
+| [ "econstructor" int_or_var(i) ] -> {
Tactics.constructor_tac true None i NoBindings
- ]
-| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
+ }
+| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac true None i bl in
Tacticals.New.tclDELAYEDWITHHOLES true bl tac
- ]
+ }
END
(** Specialize *)
TACTIC EXTEND specialize
- [ "specialize" constr_with_bindings(c) ] -> [
+| [ "specialize" constr_with_bindings(c) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
- ]
-| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [
+ }
+| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
- ]
+ }
END
TACTIC EXTEND symmetry
- [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
+| [ "symmetry" ] -> { Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} }
END
TACTIC EXTEND symmetry_in
-| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ]
+| [ "symmetry" "in" in_clause(cl) ] -> { Tactics.intros_symmetry cl }
END
(** Split *)
+{
+
let rec delayed_list = function
| [] -> fun _ sigma -> (sigma, [])
| x :: l ->
@@ -167,147 +175,159 @@ let rec delayed_list = function
let (sigma, l) = delayed_list l env sigma in
(sigma, x :: l)
+}
+
TACTIC EXTEND split
- [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
+| [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] }
END
TACTIC EXTEND esplit
- [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
+| [ "esplit" ] -> { Tactics.split_with_bindings true [NoBindings] }
END
TACTIC EXTEND split_with
- [ "split" "with" bindings(bl) ] -> [
+| [ "split" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl])
- ]
+ }
END
TACTIC EXTEND esplit_with
- [ "esplit" "with" bindings(bl) ] -> [
+| [ "esplit" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl])
- ]
+ }
END
TACTIC EXTEND exists
- [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
-| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [
+| [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] }
+| [ "exists" ne_bindings_list_sep(bll, ",") ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll)
- ]
+ }
END
TACTIC EXTEND eexists
- [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
-| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [
+| [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] }
+| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll)
- ]
+ }
END
(** Intro *)
TACTIC EXTEND intros_until
- [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
+| [ "intros" "until" quantified_hypothesis(h) ] -> { Tactics.intros_until h }
END
TACTIC EXTEND intro
-| [ "intro" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ]
-| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ]
-| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ]
-| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ]
-| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ]
-| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ]
+| [ "intro" ] -> { Tactics.intro_move None MoveLast }
+| [ "intro" ident(id) ] -> { Tactics.intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "at" "top" ] -> { Tactics.intro_move (Some id) MoveFirst }
+| [ "intro" ident(id) "at" "bottom" ] -> { Tactics.intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "after" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveAfter h) }
+| [ "intro" ident(id) "before" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveBefore h) }
+| [ "intro" "at" "top" ] -> { Tactics.intro_move None MoveFirst }
+| [ "intro" "at" "bottom" ] -> { Tactics.intro_move None MoveLast }
+| [ "intro" "after" hyp(h) ] -> { Tactics.intro_move None (MoveAfter h) }
+| [ "intro" "before" hyp(h) ] -> { Tactics.intro_move None (MoveBefore h) }
END
(** Move *)
TACTIC EXTEND move
- [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
+| [ "move" hyp(id) "at" "top" ] -> { Tactics.move_hyp id MoveFirst }
+| [ "move" hyp(id) "at" "bottom" ] -> { Tactics.move_hyp id MoveLast }
+| [ "move" hyp(id) "after" hyp(h) ] -> { Tactics.move_hyp id (MoveAfter h) }
+| [ "move" hyp(id) "before" hyp(h) ] -> { Tactics.move_hyp id (MoveBefore h) }
END
(** Rename *)
TACTIC EXTEND rename
-| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ]
+| [ "rename" ne_rename_list_sep(ids, ",") ] -> { Tactics.rename_hyp ids }
END
(** Revert *)
TACTIC EXTEND revert
- [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ]
+| [ "revert" ne_hyp_list(hl) ] -> { Tactics.revert hl }
END
(** Simple induction / destruct *)
+{
+
let simple_induct h =
Tacticals.New.tclTHEN (Tactics.intros_until h)
(Tacticals.New.onLastHyp Tactics.simplest_elim)
+}
+
TACTIC EXTEND simple_induction
- [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ]
+| [ "simple" "induction" quantified_hypothesis(h) ] -> { simple_induct h }
END
+{
+
let simple_destruct h =
Tacticals.New.tclTHEN (Tactics.intros_until h)
(Tacticals.New.onLastHyp Tactics.simplest_case)
+}
+
TACTIC EXTEND simple_destruct
- [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ]
+| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
END
(** Double induction *)
TACTIC EXTEND double_induction
- [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
- [ Elim.h_double_induction h1 h2 ]
+| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
+ { Elim.h_double_induction h1 h2 }
END
(* Admit *)
TACTIC EXTEND admit
- [ "admit" ] -> [ Proofview.give_up ]
+|[ "admit" ] -> { Proofview.give_up }
END
(* Fix *)
TACTIC EXTEND fix
- [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ]
+| [ "fix" ident(id) natural(n) ] -> { Tactics.fix id n }
END
(* Cofix *)
TACTIC EXTEND cofix
- [ "cofix" ident(id) ] -> [ Tactics.cofix id ]
+| [ "cofix" ident(id) ] -> { Tactics.cofix id }
END
(* Clear *)
TACTIC EXTEND clear
- [ "clear" hyp_list(ids) ] -> [
+| [ "clear" hyp_list(ids) ] -> {
if List.is_empty ids then Tactics.keep []
else Tactics.clear ids
- ]
-| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
+ }
+| [ "clear" "-" ne_hyp_list(ids) ] -> { Tactics.keep ids }
END
(* Clearbody *)
TACTIC EXTEND clearbody
- [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ]
+| [ "clearbody" ne_hyp_list(ids) ] -> { Tactics.clear_body ids }
END
(* Generalize dependent *)
TACTIC EXTEND generalize_dependent
- [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
+| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c }
END
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
+{
+
open Tacexpr
let initial_atomic () =
@@ -364,3 +384,5 @@ let initial_tacticals () =
]
let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
+
+}
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dae2582bd4..dbbdbfa396 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -297,25 +297,6 @@ END
(* spiwack: the print functions are incomplete, but I don't know what they are
used for *)
-let pr_r_nat_field natf =
- str "nat " ++
- match natf with
- | Retroknowledge.NatType -> str "type"
- | Retroknowledge.NatPlus -> str "plus"
- | Retroknowledge.NatTimes -> str "times"
-
-let pr_r_n_field nf =
- str "binary N " ++
- match nf with
- | Retroknowledge.NPositive -> str "positive"
- | Retroknowledge.NType -> str "type"
- | Retroknowledge.NTwice -> str "twice"
- | Retroknowledge.NTwicePlusOne -> str "twice plus one"
- | Retroknowledge.NPhi -> str "phi"
- | Retroknowledge.NPhiInv -> str "phi inv"
- | Retroknowledge.NPlus -> str "plus"
- | Retroknowledge.NTimes -> str "times"
-
let pr_r_int31_field i31f =
str "int31 " ++
match i31f with
@@ -353,26 +334,6 @@ let pr_retroknowledge_field f =
| Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
spc () ++ str "in " ++ qs group
-VERNAC ARGUMENT EXTEND retroknowledge_nat
-PRINTED BY pr_r_nat_field
-| [ "nat" "type" ] -> [ Retroknowledge.NatType ]
-| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ]
-| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ]
-END
-
-
-VERNAC ARGUMENT EXTEND retroknowledge_binary_n
-PRINTED BY pr_r_n_field
-| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ]
-| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ]
-| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ]
-| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ]
-| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ]
-| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ]
-| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ]
-| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ]
-END
-
VERNAC ARGUMENT EXTEND retroknowledge_int31
PRINTED BY pr_r_int31_field
| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7371478848..e477b12cd3 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -14,12 +14,12 @@ open Constrexpr
open Glob_term
val wit_orient : bool Genarg.uniform_genarg_type
-val orient : bool Pcoq.Gram.entry
+val orient : bool Pcoq.Entry.t
val pr_orient : bool -> Pp.t
val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
-val occurrences : (int list Locus.or_var) Pcoq.Gram.entry
+val occurrences : (int list Locus.or_var) Pcoq.Entry.t
val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type
val pr_occurrences : int list Locus.or_var -> Pp.t
val occurrences_of : int list -> Locus.occurrences
@@ -46,8 +46,8 @@ val wit_casted_constr :
Tacexpr.glob_constr_and_expr,
EConstr.t) Genarg.genarg_type
-val glob : constr_expr Pcoq.Gram.entry
-val lglob : constr_expr Pcoq.Gram.entry
+val glob : constr_expr Pcoq.Entry.t
+val lglob : constr_expr Pcoq.Entry.t
type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
@@ -55,10 +55,10 @@ type loc_place = lident gen_place
type place = Id.t gen_place
val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
-val hloc : loc_place Pcoq.Gram.entry
+val hloc : loc_place Pcoq.Entry.t
val pr_hloc : loc_place -> Pp.t
-val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t
val wit_by_arg_tac :
(raw_tactic_expr option,
glob_tactic_expr option,
@@ -68,13 +68,13 @@ val pr_by_arg_tac :
(int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
-val test_lpar_id_colon : unit Pcoq.Gram.entry
+val test_lpar_id_colon : unit Pcoq.Entry.t
val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
(** Spiwack: Primitive for retroknowledge registration *)
-val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
+val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
val wit_in_clause :
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 660e29ca82..dc027c4041 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -293,7 +293,7 @@ open Vars
let constr_flags () = {
Pretyping.use_typeclasses = true;
- Pretyping.solve_unification_constraints = true;
+ Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true }
@@ -604,8 +604,11 @@ let subst_var_with_hole occ tid t =
else
(incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
- GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
- IntroAnonymous, None)))
+ GHole (Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=Evar_kinds.Define true;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=None;
+ }, IntroAnonymous, None)))
else x
| _ -> map_glob_constr_left_to_right substrec x in
let t' = substrec t
@@ -616,13 +619,21 @@ let subst_hole_with_term occ tc t =
let locref = ref 0 in
let occref = ref occ in
let rec substrec c = match DAst.get c with
- | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) ->
+ | GHole (Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=Evar_kinds.Define true;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=None;
+ }, IntroAnonymous, s) ->
decr occref;
if Int.equal !occref 0 then tc
else
(incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
- GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s))
+ GHole (Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=Evar_kinds.Define true;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=None;
+ },IntroAnonymous,s))
| _ -> map_glob_constr_left_to_right substrec c
in
substrec t
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.mlg
index 2251a66204..e57afe3e33 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.mlg
@@ -14,15 +14,19 @@
(* by Eduardo Gimenez *)
(************************************************************************)
+{
+
open Eqdecide
open Stdarg
+}
+
DECLARE PLUGIN "ltac_plugin"
TACTIC EXTEND decide_equality
-| [ "decide" "equality" ] -> [ decideEqualityGoal ]
+| [ "decide" "equality" ] -> { decideEqualityGoal }
END
TACTIC EXTEND compare
-| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 }
END
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 620f147077..c13bd69daf 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -46,10 +46,10 @@ let reference_to_id qid =
CErrors.user_err ?loc:qid.CAst.loc
(str "This expression should be a simple identifier.")
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
+let tactic_mode = Entry.create "vernac:tactic_command"
let new_entry name =
- let e = Gram.entry_create name in
+ let e = Entry.create name in
e
let toplevel_selector = new_entry "vernac:toplevel_selector"
@@ -287,12 +287,14 @@ GEXTEND Gram
(* Definitions for tactics *)
tacdef_body:
- [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+ [ [ name = Constr.global; it=LIST1 input_fun;
+ redef = ltac_def_kind; body = tactic_expr ->
if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
else
let id = reference_to_id name in
Tacexpr.TacticDefinition (id, TacFun (it, body))
- | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
+ | name = Constr.global; redef = ltac_def_kind;
+ body = tactic_expr ->
if redef then Tacexpr.TacticRedefinition (name, body)
else
let id = reference_to_id name in
@@ -468,7 +470,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
[ VtSideff [], VtNow ] ->
[ fun ~atts ~st -> let open Vernacinterp in
let n = Option.default 0 n in
- Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
+ let deprecation = atts.deprecated in
+ Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
st
]
END
@@ -512,7 +515,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
| TacticDefinition ({CAst.v=r},_) -> r
| TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
] -> [ fun ~atts ~st -> let open Vernacinterp in
- Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
+ let deprecation = atts.deprecated in
+ Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
st
]
END
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.mlg
index 31bc34a325..2e1ce814aa 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Pp
open CErrors
open Util
@@ -215,486 +217,488 @@ let warn_deprecated_eqn_syntax =
open Pvernac.Vernac_
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
bindings red_expr int_or_var open_constr uconstr
simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
int_or_var:
- [ [ n = integer -> ArgArg n
- | id = identref -> ArgVar id ] ]
+ [ [ n = integer -> { ArgArg n }
+ | id = identref -> { ArgVar id } ] ]
;
nat_or_var:
- [ [ n = natural -> ArgArg n
- | id = identref -> ArgVar id ] ]
+ [ [ n = natural -> { ArgArg n }
+ | id = identref -> { ArgVar id } ] ]
;
(* An identifier or a quotation meta-variable *)
id_or_meta:
- [ [ id = identref -> id ] ]
+ [ [ id = identref -> { id } ] ]
;
open_constr:
- [ [ c = constr -> c ] ]
+ [ [ c = constr -> { c } ] ]
;
uconstr:
- [ [ c = constr -> c ] ]
+ [ [ c = constr -> { c } ] ]
;
destruction_arg:
- [ [ n = natural -> (None,ElimOnAnonHyp n)
+ [ [ n = natural -> { (None,ElimOnAnonHyp n) }
| test_lpar_id_rpar; c = constr_with_bindings ->
- (Some false,destruction_arg_of_constr c)
- | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c
+ { (Some false,destruction_arg_of_constr c) }
+ | c = constr_with_bindings_arg -> { on_snd destruction_arg_of_constr c }
] ]
;
constr_with_bindings_arg:
- [ [ ">"; c = constr_with_bindings -> (Some true,c)
- | c = constr_with_bindings -> (None,c) ] ]
+ [ [ ">"; c = constr_with_bindings -> { (Some true,c) }
+ | c = constr_with_bindings -> { (None,c) } ] ]
;
quantified_hypothesis:
- [ [ id = ident -> NamedHyp id
- | n = natural -> AnonHyp n ] ]
+ [ [ id = ident -> { NamedHyp id }
+ | n = natural -> { AnonHyp n } ] ]
;
conversion:
- [ [ c = constr -> (None, c)
- | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2)
+ [ [ c = constr -> { (None, c) }
+ | c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) }
| c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
- (Some (occs,c1), c2) ] ]
+ { (Some (occs,c1), c2) } ] ]
;
occs_nums:
- [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl
+ [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
| "-"; n = nat_or_var; nl = LIST0 int_or_var ->
(* have used int_or_var instead of nat_or_var for compatibility *)
- AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ]
+ { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ]
;
occs:
- [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ]
+ [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
;
pattern_occ:
- [ [ c = constr; nl = occs -> (nl,c) ] ]
+ [ [ c = constr; nl = occs -> { (nl,c) } ] ]
;
ref_or_pattern_occ:
(* If a string, it is interpreted as a ref
(anyway a Coq string does not reduce) *)
- [ [ c = smart_global; nl = occs -> nl,Inl c
- | c = constr; nl = occs -> nl,Inr c ] ]
+ [ [ c = smart_global; nl = occs -> { nl,Inl c }
+ | c = constr; nl = occs -> { nl,Inr c } ] ]
;
unfold_occ:
- [ [ c = smart_global; nl = occs -> (nl,c) ] ]
+ [ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
;
intropatterns:
- [ [ l = LIST0 nonsimple_intropattern -> l ]]
+ [ [ l = LIST0 nonsimple_intropattern -> { l } ] ]
;
ne_intropatterns:
- [ [ l = LIST1 nonsimple_intropattern -> l ]]
+ [ [ l = LIST1 nonsimple_intropattern -> { l } ] ]
;
or_and_intropattern:
- [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc
- | "()" -> IntroAndPattern []
- | "("; si = simple_intropattern; ")" -> IntroAndPattern [si]
+ [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc }
+ | "()" -> { IntroAndPattern [] }
+ | "("; si = simple_intropattern; ")" -> { IntroAndPattern [si] }
| "("; si = simple_intropattern; ",";
tc = LIST1 simple_intropattern SEP "," ; ")" ->
- IntroAndPattern (si::tc)
+ { IntroAndPattern (si::tc) }
| "("; si = simple_intropattern; "&";
tc = LIST1 simple_intropattern SEP "&" ; ")" ->
(* (A & B & C) is translated into (A,(B,C)) *)
- let rec pairify = function
+ { let rec pairify = function
| ([]|[_]|[_;_]) as l -> l
| t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
- in IntroAndPattern (pairify (si::tc)) ] ]
+ in IntroAndPattern (pairify (si::tc)) } ] ]
;
equality_intropattern:
- [ [ "->" -> IntroRewrite true
- | "<-" -> IntroRewrite false
- | "[="; tc = intropatterns; "]" -> IntroInjection tc ] ]
+ [ [ "->" -> { IntroRewrite true }
+ | "<-" -> { IntroRewrite false }
+ | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
;
naming_intropattern:
- [ [ prefix = pattern_ident -> IntroFresh prefix
- | "?" -> IntroAnonymous
- | id = ident -> IntroIdentifier id ] ]
+ [ [ prefix = pattern_ident -> { IntroFresh prefix }
+ | "?" -> { IntroAnonymous }
+ | id = ident -> { IntroIdentifier id } ] ]
;
nonsimple_intropattern:
- [ [ l = simple_intropattern -> l
- | "*" -> CAst.make ~loc:!@loc @@ IntroForthcoming true
- | "**" -> CAst.make ~loc:!@loc @@ IntroForthcoming false ]]
+ [ [ l = simple_intropattern -> { l }
+ | "*" -> { CAst.make ~loc @@ IntroForthcoming true }
+ | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ]
;
simple_intropattern:
[ [ pat = simple_intropattern_closed;
- l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
- let {CAst.loc=loc0;v=pat} = pat in
+ l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] ->
+ { let {CAst.loc=loc0;v=pat} = pat in
let f c pat =
let loc1 = Constrexpr_ops.constr_loc c in
let loc = Loc.merge_opt loc0 loc1 in
IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in
- CAst.make ~loc:!@loc @@ List.fold_right f l pat ] ]
+ CAst.make ~loc @@ List.fold_right f l pat } ] ]
;
simple_intropattern_closed:
- [ [ pat = or_and_intropattern -> CAst.make ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat)
- | pat = equality_intropattern -> CAst.make ~loc:!@loc @@ IntroAction pat
- | "_" -> CAst.make ~loc:!@loc @@ IntroAction IntroWildcard
- | pat = naming_intropattern -> CAst.make ~loc:!@loc @@ IntroNaming pat ] ]
+ [ [ pat = or_and_intropattern -> { CAst.make ~loc @@ IntroAction (IntroOrAndPattern pat) }
+ | pat = equality_intropattern -> { CAst.make ~loc @@ IntroAction pat }
+ | "_" -> { CAst.make ~loc @@ IntroAction IntroWildcard }
+ | pat = naming_intropattern -> { CAst.make ~loc @@ IntroNaming pat } ] ]
;
simple_binding:
- [ [ "("; id = ident; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (NamedHyp id, c)
- | "("; n = natural; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (AnonHyp n, c) ] ]
+ [ [ "("; id = ident; ":="; c = lconstr; ")" -> { CAst.make ~loc (NamedHyp id, c) }
+ | "("; n = natural; ":="; c = lconstr; ")" -> { CAst.make ~loc (AnonHyp n, c) } ] ]
;
bindings:
[ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
- ExplicitBindings bl
- | bl = LIST1 constr -> ImplicitBindings bl ] ]
+ { ExplicitBindings bl }
+ | bl = LIST1 constr -> { ImplicitBindings bl } ] ]
;
constr_with_bindings:
- [ [ c = constr; l = with_bindings -> (c, l) ] ]
+ [ [ c = constr; l = with_bindings -> { (c, l) } ] ]
;
with_bindings:
- [ [ "with"; bl = bindings -> bl | -> NoBindings ] ]
+ [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ]
;
red_flags:
- [ [ IDENT "beta" -> [FBeta]
- | IDENT "iota" -> [FMatch;FFix;FCofix]
- | IDENT "match" -> [FMatch]
- | IDENT "fix" -> [FFix]
- | IDENT "cofix" -> [FCofix]
- | IDENT "zeta" -> [FZeta]
- | IDENT "delta"; d = delta_flag -> [d]
+ [ [ IDENT "beta" -> { [FBeta] }
+ | IDENT "iota" -> { [FMatch;FFix;FCofix] }
+ | IDENT "match" -> { [FMatch] }
+ | IDENT "fix" -> { [FFix] }
+ | IDENT "cofix" -> { [FCofix] }
+ | IDENT "zeta" -> { [FZeta] }
+ | IDENT "delta"; d = delta_flag -> { [d] }
] ]
;
delta_flag:
- [ [ "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl
- | "["; idl = LIST1 smart_global; "]" -> FConst idl
- | -> FDeltaBut []
+ [ [ "-"; "["; idl = LIST1 smart_global; "]" -> { FDeltaBut idl }
+ | "["; idl = LIST1 smart_global; "]" -> { FConst idl }
+ | -> { FDeltaBut [] }
] ]
;
strategy_flag:
- [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s)
- | d = delta_flag -> all_with d
+ [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) }
+ | d = delta_flag -> { all_with d }
] ]
;
red_expr:
- [ [ IDENT "red" -> Red false
- | IDENT "hnf" -> Hnf
- | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
- | IDENT "cbv"; s = strategy_flag -> Cbv s
- | IDENT "cbn"; s = strategy_flag -> Cbn s
- | IDENT "lazy"; s = strategy_flag -> Lazy s
- | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
- | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
- | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
- | IDENT "fold"; cl = LIST1 constr -> Fold cl
- | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl
- | s = IDENT -> ExtraRedExpr s ] ]
+ [ [ IDENT "red" -> { Red false }
+ | IDENT "hnf" -> { Hnf }
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with d,po) }
+ | IDENT "cbv"; s = strategy_flag -> { Cbv s }
+ | IDENT "cbn"; s = strategy_flag -> { Cbn s }
+ | IDENT "lazy"; s = strategy_flag -> { Lazy s }
+ | IDENT "compute"; delta = delta_flag -> { Cbv (all_with delta) }
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po }
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po }
+ | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul }
+ | IDENT "fold"; cl = LIST1 constr -> { Fold cl }
+ | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> { Pattern pl }
+ | s = IDENT -> { ExtraRedExpr s } ] ]
;
hypident:
[ [ id = id_or_meta ->
- let id : lident = id in
- id,InHyp
+ { let id : lident = id in
+ id,InHyp }
| "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
- let id : lident = id in
- id,InHypTypeOnly
+ { let id : lident = id in
+ id,InHypTypeOnly }
| "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
- let id : lident = id in
- id,InHypValueOnly
+ { let id : lident = id in
+ id,InHypValueOnly }
] ]
;
hypident_occ:
- [ [ (id,l)=hypident; occs=occs ->
+ [ [ h=hypident; occs=occs ->
+ { let (id,l) = h in
let id : lident = id in
- ((occs,id),l) ] ]
+ ((occs,id),l) } ] ]
;
in_clause:
[ [ "*"; occs=occs ->
- {onhyps=None; concl_occs=occs}
+ { {onhyps=None; concl_occs=occs} }
| "*"; "|-"; occs=concl_occ ->
- {onhyps=None; concl_occs=occs}
+ { {onhyps=None; concl_occs=occs} }
| hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
- {onhyps=Some hl; concl_occs=occs}
+ { {onhyps=Some hl; concl_occs=occs} }
| hl=LIST0 hypident_occ SEP"," ->
- {onhyps=Some hl; concl_occs=NoOccurrences} ] ]
+ { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ]
;
clause_dft_concl:
- [ [ "in"; cl = in_clause -> cl
- | occs=occs -> {onhyps=Some[]; concl_occs=occs}
- | -> all_concl_occs_clause ] ]
+ [ [ "in"; cl = in_clause -> { cl }
+ | occs=occs -> { {onhyps=Some[]; concl_occs=occs} }
+ | -> { all_concl_occs_clause } ] ]
;
clause_dft_all:
- [ [ "in"; cl = in_clause -> cl
- | -> {onhyps=None; concl_occs=AllOccurrences} ] ]
+ [ [ "in"; cl = in_clause -> { cl }
+ | -> { {onhyps=None; concl_occs=AllOccurrences} } ] ]
;
opt_clause:
- [ [ "in"; cl = in_clause -> Some cl
- | "at"; occs = occs_nums -> Some {onhyps=Some[]; concl_occs=occs}
- | -> None ] ]
+ [ [ "in"; cl = in_clause -> { Some cl }
+ | "at"; occs = occs_nums -> { Some {onhyps=Some[]; concl_occs=occs} }
+ | -> { None } ] ]
;
concl_occ:
- [ [ "*"; occs = occs -> occs
- | -> NoOccurrences ] ]
+ [ [ "*"; occs = occs -> { occs }
+ | -> { NoOccurrences } ] ]
;
in_hyp_list:
- [ [ "in"; idl = LIST1 id_or_meta -> idl
- | -> [] ] ]
+ [ [ "in"; idl = LIST1 id_or_meta -> { idl }
+ | -> { [] } ] ]
;
in_hyp_as:
- [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
- | -> None ] ]
+ [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
+ | -> { None } ] ]
;
orient:
- [ [ "->" -> true
- | "<-" -> false
- | -> true ]]
+ [ [ "->" -> { true }
+ | "<-" -> { false }
+ | -> { true } ] ]
;
simple_binder:
- [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@
- CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))
- | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
+ [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@
+ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) }
+ | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) }
] ]
;
fixdecl:
[ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot;
- ":"; ty=lconstr; ")" -> (!@loc, id, bl, ann, ty) ] ]
+ ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ]
;
fixannot:
- [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
- | -> None ] ]
+ [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id }
+ | -> { None } ] ]
;
cofixdecl:
[ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" ->
- (!@loc, id, bl, None, ty) ] ]
+ { (loc, id, bl, None, ty) } ] ]
;
bindings_with_parameters:
[ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder;
- ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
+ ":="; c = lconstr; ")" -> { (id, mkCLambdaN_simple bl c) } ] ]
;
eliminator:
- [ [ "using"; el = constr_with_bindings -> el ] ]
+ [ [ "using"; el = constr_with_bindings -> { el } ] ]
;
as_ipat:
- [ [ "as"; ipat = simple_intropattern -> Some ipat
- | -> None ] ]
+ [ [ "as"; ipat = simple_intropattern -> { Some ipat }
+ | -> { None } ] ]
;
or_and_intropattern_loc:
- [ [ ipat = or_and_intropattern -> ArgArg (CAst.make ~loc:!@loc ipat)
- | locid = identref -> ArgVar locid ] ]
+ [ [ ipat = or_and_intropattern -> { ArgArg (CAst.make ~loc ipat) }
+ | locid = identref -> { ArgVar locid } ] ]
;
as_or_and_ipat:
- [ [ "as"; ipat = or_and_intropattern_loc -> Some ipat
- | -> None ] ]
+ [ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat }
+ | -> { None } ] ]
;
eqn_ipat:
- [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (CAst.make ~loc:!@loc pat)
+ [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) }
| IDENT "_eqn"; ":"; pat = naming_intropattern ->
- let loc = !@loc in
- warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat)
+ { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) }
| IDENT "_eqn" ->
- let loc = !@loc in
- warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous)
- | -> None ] ]
+ { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) }
+ | -> { None } ] ]
;
as_name:
- [ [ "as"; id = ident ->Names.Name.Name id | -> Names.Name.Anonymous ] ]
+ [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ]
;
by_tactic:
- [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
- | -> None ] ]
+ [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac }
+ | -> { None } ] ]
;
rewriter :
- [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c)
- | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c)
- | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
- | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c)
- | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
- | c = constr_with_bindings_arg -> (Equality.Precisely 1, c)
+ [ [ "!"; c = constr_with_bindings_arg -> { (Equality.RepeatPlus,c) }
+ | ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.RepeatStar,c) }
+ | n = natural; "!"; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) }
+ | n = natural; ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.UpTo n,c) }
+ | n = natural; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) }
+ | c = constr_with_bindings_arg -> { (Equality.Precisely 1, c) }
] ]
;
oriented_rewriter :
- [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
+ [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
;
induction_clause:
[ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
- cl = opt_clause -> (c,(eq,pat),cl) ] ]
+ cl = opt_clause -> { (c,(eq,pat),cl) } ] ]
;
induction_clause_list:
[ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator;
cl_tolerance = opt_clause ->
(* Condition for accepting "in" at the end by compatibility *)
- match ic,el,cl_tolerance with
+ { match ic,el,cl_tolerance with
| [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el)
| _,_,Some _ -> err ()
- | _,_,None -> (ic,el) ]]
+ | _,_,None -> (ic,el) } ] ]
;
simple_tactic:
[ [
(* Basic tactics *)
IDENT "intros"; pl = ne_intropatterns ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl))
+ { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,pl)) }
| IDENT "intros" ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[CAst.make ~loc:!@loc @@IntroForthcoming false]))
+ { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
| IDENT "eintros"; pl = ne_intropatterns ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl))
+ { TacAtom (Loc.tag ~loc @@ TacIntroPattern (true,pl)) }
| IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,false,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,false,cl,inhyp)) }
| IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,true,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,true,cl,inhyp)) }
| IDENT "simple"; IDENT "apply";
cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,false,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,false,cl,inhyp)) }
| IDENT "simple"; IDENT "eapply";
cl = LIST1 constr_with_bindings_arg SEP",";
- inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,true,cl,inhyp))
+ inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,true,cl,inhyp)) }
| IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacElim (false,cl,el))
+ { TacAtom (Loc.tag ~loc @@ TacElim (false,cl,el)) }
| IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacElim (true,cl,el))
- | IDENT "case"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase false icl)
- | IDENT "ecase"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase true icl)
+ { TacAtom (Loc.tag ~loc @@ TacElim (true,cl,el)) }
+ | IDENT "case"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase false icl) }
+ | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase true icl) }
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd))
+ { TacAtom (Loc.tag ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
| "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
+ { TacAtom (Loc.tag ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
- | IDENT "pose"; (id,b) = bindings_with_parameters ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None))
+ | IDENT "pose"; bl = bindings_with_parameters ->
+ { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "pose"; b = constr; na = as_name ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None))
- | IDENT "epose"; (id,b) = bindings_with_parameters ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
+ | IDENT "epose"; bl = bindings_with_parameters ->
+ { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "epose"; b = constr; na = as_name ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None))
- | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
+ | IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl ->
+ { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) }
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None))
- | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,true,None)) }
+ | IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl ->
+ { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) }
| IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,true,None)) }
| IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
p = clause_dft_all ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,false,e)) }
| IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat;
p = clause_dft_all ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e))
+ { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,false,e)) }
(* Alternative syntax for "pose proof c as id" *)
| IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
c = lconstr; ")" ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
c = lconstr; ")" ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
(* Alternative syntax for "assert c as id by tac" *)
| IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
(* Alternative syntax for "enough c as id by tac" *)
| IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- let { CAst.loc = loc; v = id } = lid in
- TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
| IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,None,ipat,c)) }
| IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,None,ipat,c)) }
| IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
| IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c))
+ { TacAtom (Loc.tag ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
| IDENT "generalize"; c = constr ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)])
+ { TacAtom (Loc.tag ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
| IDENT "generalize"; c = constr; l = LIST1 constr ->
- let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
- TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l)))
+ { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
+ TacAtom (Loc.tag ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) }
| IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
na = as_name;
- l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (((nl,c),na)::l))
+ l = LIST0 [","; c = pattern_occ; na = as_name -> { (c,na) } ] ->
+ { TacAtom (Loc.tag ~loc @@ TacGeneralize (((nl,c),na)::l)) }
(* Derived basic tactics *)
| IDENT "induction"; ic = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct (true,false,ic))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct (true,false,ic)) }
| IDENT "einduction"; ic = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(true,true,ic))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(true,true,ic)) }
| IDENT "destruct"; icl = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,false,icl)) }
| IDENT "edestruct"; icl = induction_clause_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,true,icl))
+ { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,true,icl)) }
(* Equality and inversion *)
| IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (false,l,cl,t))
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (false,l,cl,t)) }
| IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (true,l,cl,t))
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (true,l,cl,t)) }
| IDENT "dependent"; k =
- [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
- | IDENT "inversion" -> FullInversion
- | IDENT "inversion_clear" -> FullInversionClear ];
+ [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion }
+ | IDENT "inversion" -> { FullInversion }
+ | IDENT "inversion_clear" -> { FullInversionClear } ];
hyp = quantified_hypothesis;
- ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (DepInversion (k,co,ids),hyp))
+ ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] ->
+ { TacAtom (Loc.tag ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) }
| IDENT "simple"; IDENT "inversion";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
| IDENT "inversion";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
| IDENT "inversion_clear";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
| IDENT "inversion"; hyp = quantified_hypothesis;
"using"; c = constr; cl = in_hyp_list ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (InversionUsing (c,cl), hyp))
+ { TacAtom (Loc.tag ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
(* Conversion *)
| IDENT "red"; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Red false, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Red false, cl)) }
| IDENT "hnf"; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Hnf, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Hnf, cl)) }
| IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Simpl (all_with d, po), cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Simpl (all_with d, po), cl)) }
| IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv s, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv s, cl)) }
| IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbn s, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Cbn s, cl)) }
| IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Lazy s, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Lazy s, cl)) }
| IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv (all_with delta), cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv (all_with delta), cl)) }
| IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvVm po, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (CbvVm po, cl)) }
| IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvNative po, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (CbvNative po, cl)) }
| IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Unfold ul, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Unfold ul, cl)) }
| IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Fold l, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Fold l, cl)) }
| IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Pattern pl, cl))
+ { TacAtom (Loc.tag ~loc @@ TacReduce (Pattern pl, cl)) }
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
- | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
- let p,cl = merge_occurrences (!@loc) cl oc in
- TacAtom (Loc.tag ~loc:!@loc @@ TacChange (p,c,cl))
+ | IDENT "change"; c = conversion; cl = clause_dft_concl ->
+ { let (oc, c) = c in
+ let p,cl = merge_occurrences loc cl oc in
+ TacAtom (Loc.tag ~loc @@ TacChange (p,c,cl)) }
] ]
;
-END;;
+END
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index e9711268c2..759bb62fdd 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,11 +11,10 @@
open Pcoq
(* Main entry for extensions *)
-let simple_tactic = Gram.entry_create "tactic:simple_tactic"
+let simple_tactic = Entry.create "tactic:simple_tactic"
-let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name)
+let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
-(* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
make_gen_entry utactic "open_constr"
@@ -23,7 +22,7 @@ let constr_with_bindings =
make_gen_entry utactic "constr_with_bindings"
let bindings =
make_gen_entry utactic "bindings"
-let hypident = Gram.entry_create "hypident"
+let hypident = Entry.create "hypident"
let constr_may_eval = make_gen_entry utactic "constr_may_eval"
let constr_eval = make_gen_entry utactic "constr_eval"
let uconstr =
@@ -40,7 +39,7 @@ let clause_dft_concl =
(* Main entries for ltac *)
-let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+let tactic_arg = Entry.create "tactic:tactic_arg"
let tactic_expr = make_gen_entry utactic "tactic_expr"
let binder_tactic = make_gen_entry utactic "binder_tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index c5aa542fd1..9bff98b6c3 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -17,22 +17,22 @@ open Tacexpr
open Genredexpr
open Tactypes
-val open_constr : constr_expr Gram.entry
-val constr_with_bindings : constr_expr with_bindings Gram.entry
-val bindings : constr_expr bindings Gram.entry
-val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
-val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val uconstr : constr_expr Gram.entry
-val quantified_hypothesis : quantified_hypothesis Gram.entry
-val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
-val int_or_var : int Locus.or_var Gram.entry
-val simple_tactic : raw_tactic_expr Gram.entry
-val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : Names.lident Locus.clause_expr Gram.entry
-val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
-val tactic_arg : raw_tactic_arg Gram.entry
-val tactic_expr : raw_tactic_expr Gram.entry
-val binder_tactic : raw_tactic_expr Gram.entry
-val tactic : raw_tactic_expr Gram.entry
-val tactic_eoi : raw_tactic_expr Gram.entry
+val open_constr : constr_expr Entry.t
+val constr_with_bindings : constr_expr with_bindings Entry.t
+val bindings : constr_expr bindings Entry.t
+val hypident : (Names.lident * Locus.hyp_location_flag) Entry.t
+val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val uconstr : constr_expr Entry.t
+val quantified_hypothesis : quantified_hypothesis Entry.t
+val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t
+val int_or_var : int Locus.or_var Entry.t
+val simple_tactic : raw_tactic_expr Entry.t
+val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
+val in_clause : Names.lident Locus.clause_expr Entry.t
+val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
+val tactic_arg : raw_tactic_arg Entry.t
+val tactic_expr : raw_tactic_expr Entry.t
+val binder_tactic : raw_tactic_expr Entry.t
+val tactic : raw_tactic_expr Entry.t
+val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 09179dad34..4357689ee2 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -115,7 +115,7 @@ let string_of_genarg_arg (ArgumentType arg) =
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
- let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+ let has_type (Val.Dyn (tag, _)) t = match Val.eq tag t with
| None -> false
| Some _ -> true
@@ -188,7 +188,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| AN v -> f v
| ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
- let pr_located pr (loc,x) = pr x
+ let pr_located pr (_,x) = pr x
let pr_evaluable_reference = function
| EvalVarRef id -> pr_id id
@@ -240,7 +240,7 @@ let string_of_genarg_arg (ArgumentType arg) =
in
pr_sequence (fun x -> x) l
- let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+ let pr_extend_gen pr_gen _ { mltac_name = s; mltac_index = i } l =
let name =
str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
str "@" ++ int i
@@ -260,7 +260,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| Extend.Uentry tag ->
let ArgT.Any tag = tag in
ArgT.repr tag
- | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+ | Extend.Uentryl (_, lvl) -> "tactic" ^ string_of_int lvl
let pr_alias_key key =
try
@@ -288,7 +288,7 @@ let string_of_genarg_arg (ArgumentType arg) =
let p = pr_tacarg_using_rule pr_gen prods in
if pp.pptac_level > lev then surround p else p
with Not_found ->
- let pr arg = str "_" in
+ let pr _ = str "_" in
KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg))
@@ -341,14 +341,14 @@ let string_of_genarg_arg (ArgumentType arg) =
pr_any_arg pr symb arg
| _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
- let pr_raw_extend_rec prc prlc prtac prpat =
+ let pr_raw_extend_rec prtac =
pr_extend_gen (pr_farg prtac)
- let pr_glob_extend_rec prc prlc prtac prpat =
+ let pr_glob_extend_rec prtac =
pr_extend_gen (pr_farg prtac)
- let pr_raw_alias prc prlc prtac prpat lev key args =
+ let pr_raw_alias prtac lev key args =
pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
- let pr_glob_alias prc prlc prtac prpat lev key args =
+ let pr_glob_alias prtac lev key args =
pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
(**********************************************************************)
@@ -743,7 +743,7 @@ let pr_goal_selector ~toplevel s =
(* Main tactic printer *)
and pr_atom1 a = tag_atom a (match a with
(* Basic tactics *)
- | TacIntroPattern (ev,[]) as t ->
+ | TacIntroPattern (_,[]) as t ->
pr_atom0 t
| TacIntroPattern (ev,(_::_ as p)) ->
hov 1 (primitive (if ev then "eintros" else "intros") ++
@@ -1054,7 +1054,7 @@ let pr_goal_selector ~toplevel s =
primitive "fresh" ++ pr_fresh_ids l, latom
| TacArg(_,TacGeneric arg) ->
pr.pr_generic arg, latom
- | TacArg(_,TacCall(loc,(f,[]))) ->
+ | TacArg(_,TacCall(_,(f,[]))) ->
pr.pr_reference f, latom
| TacArg(_,TacCall(loc,(f,l))) ->
pr_with_comments ?loc (hov 1 (
@@ -1112,8 +1112,8 @@ let pr_goal_selector ~toplevel s =
pr_reference = pr_qualid;
pr_name = pr_lident;
pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
- pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
- pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+ pr_extend = pr_raw_extend_rec pr_raw_tactic_level;
+ pr_alias = pr_raw_alias pr_raw_tactic_level;
} in
make_pr_tac
pr raw_printers
@@ -1142,12 +1142,8 @@ let pr_goal_selector ~toplevel s =
pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
pr_name = pr_lident;
pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg);
- pr_extend = pr_glob_extend_rec
- (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
- prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
- pr_alias = pr_glob_alias
- (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
- prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+ pr_extend = pr_glob_extend_rec prtac;
+ pr_alias = pr_glob_alias prtac;
} in
make_pr_tac
pr glob_printers
@@ -1168,8 +1164,8 @@ let pr_goal_selector ~toplevel s =
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
- let pr_atomic_tactic_level env sigma n t =
- let prtac n (t:atomic_tactic_expr) =
+ let pr_atomic_tactic_level env sigma t =
+ let prtac (t:atomic_tactic_expr) =
let pr = {
pr_tactic = (fun _ _ -> str "<tactic>");
pr_constr = (fun c -> pr_econstr_env env sigma c);
@@ -1188,18 +1184,15 @@ let pr_goal_selector ~toplevel s =
in
pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
in
- prtac n t
+ prtac t
let pr_raw_generic = Pputils.pr_raw_generic
let pr_glb_generic = Pputils.pr_glb_generic
- let pr_raw_extend env = pr_raw_extend_rec
- pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+ let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level
- let pr_glob_extend env = pr_glob_extend_rec
- (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
- (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+ let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
let pr_alias pr lev key args =
pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1207,14 +1200,14 @@ let pr_goal_selector ~toplevel s =
let pr_extend pr lev ml args =
pr_extend_gen pr lev ml args
- let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c
+ let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c
let declare_extra_genarg_pprule wit
(f : 'a raw_extra_genarg_printer)
(g : 'b glob_extra_genarg_printer)
(h : 'c extra_genarg_printer) =
begin match wit with
- | ExtraArg s -> ()
+ | ExtraArg _ -> ()
| _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
end;
let f x =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 01c52c413c..9f8cd2fc4e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -409,7 +409,7 @@ module TypeGlobal = struct
let inverse env (evd,cstrs) car rel =
- let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
+ let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in
app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
end
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 84baea964e..026c00b849 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -165,8 +165,7 @@ let coerce_var_to_ident fresh env sigma v =
(* Interprets, if possible, a constr to an identifier which may not
be fresh but suitable to be given to the fresh tactic. Works for
vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh env sigma v =
-let g = sigma in
+let coerce_to_ident_not_fresh sigma v =
let id_of_name = function
| Name.Anonymous -> Id.of_string "x"
| Name.Name x -> x in
@@ -183,9 +182,9 @@ let id_of_name = function
| Some c ->
match EConstr.kind sigma c with
| Var id -> id
- | Meta m -> id_of_name (Evd.meta_name g m)
+ | Meta m -> id_of_name (Evd.meta_name sigma m)
| Evar (kn,_) ->
- begin match Evd.evar_ident kn g with
+ begin match Evd.evar_ident kn sigma with
| None -> fail ()
| Some id -> id
end
@@ -208,7 +207,7 @@ let id_of_name = function
| _ -> fail()
-let coerce_to_intro_pattern env sigma v =
+let coerce_to_intro_pattern sigma v =
if has_type v (topwit wit_intro_pattern) then
(out_gen (topwit wit_intro_pattern) v).CAst.v
else if has_type v (topwit wit_var) then
@@ -221,8 +220,8 @@ let coerce_to_intro_pattern env sigma v =
IntroNaming (IntroIdentifier (destVar sigma c))
| _ -> raise (CannotCoerceTo "an introduction pattern")
-let coerce_to_intro_pattern_naming env sigma v =
- match coerce_to_intro_pattern env sigma v with
+let coerce_to_intro_pattern_naming sigma v =
+ match coerce_to_intro_pattern sigma v with
| IntroNaming pat -> pat
| _ -> raise (CannotCoerceTo "a naming introduction pattern")
@@ -255,7 +254,7 @@ let coerce_to_constr env v =
(try [], constr_of_id env id with Not_found -> fail ())
else fail ()
-let coerce_to_uconstr env v =
+let coerce_to_uconstr v =
if has_type v (topwit wit_uconstr) then
out_gen (topwit wit_uconstr) v
else
@@ -299,11 +298,11 @@ let coerce_to_constr_list env v =
List.map map l
| None -> raise (CannotCoerceTo "a term list")
-let coerce_to_intro_pattern_list ?loc env sigma v =
+let coerce_to_intro_pattern_list ?loc sigma v =
match Value.to_list v with
| None -> raise (CannotCoerceTo "an intro pattern list")
| Some l ->
- let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in
+ let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in
List.map map l
let coerce_to_hyp env sigma v =
@@ -328,7 +327,7 @@ let coerce_to_hyp_list env sigma v =
| None -> raise (CannotCoerceTo "a variable list")
(* Interprets a qualified name *)
-let coerce_to_reference env sigma v =
+let coerce_to_reference sigma v =
match Value.to_constr v with
| Some c ->
begin
@@ -356,7 +355,7 @@ let coerce_to_quantified_hypothesis sigma v =
(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env sigma v =
+let coerce_to_decl_or_quant_hyp sigma v =
if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
else
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 56f8816840..d2ae92f6ce 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -51,12 +51,12 @@ val coerce_to_constr_context : Value.t -> constr
val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t
-val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
+val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t
-val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
val coerce_to_intro_pattern_naming :
- Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
+ Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
val coerce_to_hint_base : Value.t -> string
@@ -64,7 +64,7 @@ val coerce_to_int : Value.t -> int
val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders
-val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr
+val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr
val coerce_to_closed_constr : Environ.env -> Value.t -> constr
@@ -74,17 +74,17 @@ val coerce_to_evaluable_ref :
val coerce_to_constr_list : Environ.env -> Value.t -> constr list
val coerce_to_intro_pattern_list :
- ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
+ ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list
-val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t
+val coerce_to_reference : Evd.evar_map -> Value.t -> GlobRef.t
val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis
-val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
+val coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> quantified_hypothesis
val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 98d4515367..636cb8ebf8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -45,7 +45,7 @@ let coincide s pat off =
let atactic n =
if n = 5 then Aentry Pltac.binder_tactic
- else Aentryl (Pltac.tactic_expr, n)
+ else Aentryl (Pltac.tactic_expr, string_of_int n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -252,7 +252,7 @@ type tactic_grammar_obj = {
tacobj_key : KerName.t;
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
- tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+ tacobj_body : Tacenv.alias_tactic;
tacobj_forml : bool;
}
@@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) =
extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
- let (ids, body) = tobj.tacobj_body in
+ let open Tacenv in
+ let alias = tobj.tacobj_body in
{ tobj with
tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
- tacobj_body = (ids, Tacsubst.subst_tactic subst body);
+ tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body };
}
let classify_tactic_notation tacobj = Substitute tacobj
@@ -308,25 +309,26 @@ let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, (_, ido)) -> ido
-let add_glob_tactic_notation local ~level prods forml ids tac =
+let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac =
let parule = {
tacgram_level = level;
tacgram_prods = prods;
} in
+ let open Tacenv in
let tacobj = {
tacobj_key = make_fresh_key prods;
tacobj_local = local;
tacobj_tacgram = parule;
- tacobj_body = (ids, tac);
+ tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation };
tacobj_forml = forml;
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
-let add_tactic_notation local n prods e =
+let add_tactic_notation local n ?deprecation prods e =
let ids = List.map_filter cons_production_parameter prods in
let prods = List.map interp_prod_item prods in
let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
- add_glob_tactic_notation local ~level:n prods false ids tac
+ add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac
(**********************************************************************)
(* ML Tactic entries *)
@@ -366,7 +368,7 @@ let extend_atomic_tactic name entries =
in
List.iteri add_atomic entries
-let add_ml_tactic_notation name ~level prods =
+let add_ml_tactic_notation name ~level ?deprecation prods =
let len = List.length prods in
let iter i prods =
let open Tacexpr in
@@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods =
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
let map id = Reference (Locus.ArgVar (CAst.make id)) in
let tac = TacML (Loc.tag (entry, List.map map ids)) in
- add_glob_tactic_notation false ~level prods true ids tac
+ add_glob_tactic_notation false ~level ?deprecation prods true ids tac
in
List.iteri iter (List.rev prods);
(** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
@@ -398,7 +400,7 @@ let create_ltac_quotation name cast (e, l) =
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
| None -> Aentry e
- | Some l -> Aentryl (e, l)
+ | Some l -> Aentryl (e, string_of_int l)
in
(* let level = Some "1" in *)
let level = None in
@@ -430,7 +432,7 @@ let warn_unusable_identifier =
(fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
strbrk "may be unusable because of a conflict with a notation.")
-let register_ltac local tacl =
+let register_ltac local ?deprecation tacl =
let map tactic_body =
match tactic_body with
| Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
@@ -483,10 +485,10 @@ let register_ltac local tacl =
let defs = States.with_state_protection defs () in
let iter (def, tac) = match def with
| NewTac id ->
- Tacenv.register_ltac false local id tac;
+ Tacenv.register_ltac false local id tac ?deprecation;
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
| UpdateTac kn ->
- Tacenv.redefine_ltac local kn tac;
+ Tacenv.redefine_ltac local kn tac ?deprecation;
let name = Tacenv.shortest_qualid_of_tactic kn in
Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
in
@@ -554,13 +556,18 @@ let () =
] in
register_grammars_by_name "tactic" entries
+let get_identifier id =
+ (** Workaround for badly-designed generic arguments lacking a closure *)
+ Names.Id.of_string_soft ("$" ^ id)
+
+
type _ ty_sig =
| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
| TyIdent : string * 'r ty_sig -> 'r ty_sig
| TyArg :
- (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+ ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
| TyAnonArg :
- ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+ ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
@@ -578,23 +585,15 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol
fun sign -> match sign with
| TyNil -> []
| TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
- | TyArg ((loc,(a,id)),sig') ->
- TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
- | TyAnonArg ((loc,a),sig') ->
- TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig'
+ | TyArg (a, id, sig') ->
+ let id = get_identifier id in
+ TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
+ | TyAnonArg (a, sig') ->
+ TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig'
let clause_of_ty_ml = function
| TyML (t,_) -> clause_of_sign t
-let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
- | TUentry a -> ExtraArg a
- | TUentryl (a,l) -> ExtraArg a
- | TUopt(o) -> OptArg (prj o)
- | TUlist1 l -> ListArg (prj l)
- | TUlist1sep (l,_) -> ListArg (prj l)
- | TUlist0 l -> ListArg (prj l)
- | TUlist0sep (l,_) -> ListArg (prj l)
-
let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
fun sign tac ->
match sign with
@@ -604,15 +603,15 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
| _ :: _ -> assert false
end
| TyIdent (s, sig') -> eval_sign sig' tac
- | TyArg ((_loc,(a,id)), sig') ->
+ | TyArg (a, _, sig') ->
let f = eval_sign sig' in
begin fun tac vals ist -> match vals with
| [] -> assert false
| v :: vals ->
- let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+ let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in
f (tac v') vals ist
end tac
- | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac
+ | TyAnonArg (a, sig') -> eval_sign sig' tac
let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
| TyML (t,tac) -> eval_sign t tac
@@ -624,14 +623,14 @@ let is_constr_entry = function
let rec only_constr : type a. a ty_sig -> bool = function
| TyNil -> true
| TyIdent(_,_) -> false
-| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false
-| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false
+| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false
+| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false
let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
| TyNil -> []
| TyIdent (_,s) -> mk_sign_vars s
-| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s
-| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s
+| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s
+| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s
let dummy_id = Id.of_string "_"
@@ -652,7 +651,7 @@ let lift_constr_tac_to_ml_tac vars tac =
end in
tac
-let tactic_extend plugin_name tacname ~level sign =
+let tactic_extend plugin_name tacname ~level ?deprecation sign =
let open Tacexpr in
let ml_tactic_name =
{ mltac_tactic = tacname;
@@ -681,10 +680,10 @@ let tactic_extend plugin_name tacname ~level sign =
This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
let id = Names.Id.of_string name in
- let obj () = Tacenv.register_ltac true false id body in
+ let obj () = Tacenv.register_ltac true false id body ?deprecation in
let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
Mltop.declare_cache_obj obj plugin_name
| _ ->
- let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+ let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 2bfbbe2e16..138a584e01 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,10 +12,12 @@
open Vernacexpr
open Tacexpr
+open Vernacinterp
(** {5 Tactic Definitions} *)
-val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> ?deprecation:deprecation ->
+ Tacexpr.tacdef_body list -> unit
(** Adds new Ltac definitions to the environment. *)
(** {5 Tactic Notations} *)
@@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol
leaves. *)
val add_tactic_notation :
- locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
- raw_tactic_expr -> unit
+ locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+ grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
(** [add_tactic_notation local level prods expr] adds a tactic notation in the
environment at level [level] with locality [local] made of the grammar
productions [prods] and returning the body [expr] *)
@@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
to finding an argument by name (as in {!Genarg}) if there is none
matching. *)
-val add_ml_tactic_notation : ml_tactic_name -> level:int ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation ->
argument grammar_tactic_prod_item_expr list list -> unit
(** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
ML-side macro. *)
@@ -55,7 +57,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int ->
(** {5 Tactic Quotations} *)
val create_ltac_quotation : string ->
- ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
+ ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit
(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
generates an argument using [f] on the entry parsed by [e]. *)
@@ -72,10 +74,11 @@ type _ ty_sig =
| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
| TyIdent : string * 'r ty_sig -> 'r ty_sig
| TyArg :
- (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+ ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
| TyAnonArg :
- ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+ ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
-val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
+val tactic_extend : string -> string -> level:Int.t ->
+ ?deprecation:deprecation -> ty_ml list -> unit
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5ab2d690d..0bb9ccb1d8 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn =
(** Tactic notations (TacAlias) *)
type alias = KerName.t
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+ { alias_args: Id.t list;
+ alias_body: glob_tactic_expr;
+ alias_deprecation: Vernacinterp.deprecation option;
+ }
let alias_map = Summary.ref ~name:"tactic-alias"
(KNmap.empty : alias_tactic KNmap.t)
@@ -118,6 +122,7 @@ type ltac_entry = {
tac_for_ml : bool;
tac_body : glob_tactic_expr;
tac_redef : ModPath.t list;
+ tac_deprecation : Vernacinterp.deprecation option
}
let mactab =
@@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body
let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml
-let add kn b t =
- let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in
+let add ~deprecation kn b t =
+ let entry = { tac_for_ml = b;
+ tac_body = t;
+ tac_redef = [];
+ tac_deprecation = deprecation;
+ } in
mactab := KNmap.add kn entry !mactab
let replace kn path t =
@@ -139,34 +148,38 @@ let replace kn path t =
let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
mactab := KNmap.modify kn entry !mactab
-let load_md i ((sp, kn), (local, id, b, t)) = match id with
+let tac_deprecation kn =
+ try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None
+
+let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
let () = if not local then push_tactic (Until i) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
-let open_md i ((sp, kn), (local, id, b, t)) = match id with
+let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
let () = if not local then push_tactic (Exactly i) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
-let cache_md ((sp, kn), (local, id ,b, t)) = match id with
+let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
| None ->
let () = push_tactic (Until 1) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
let subst_kind subst id = match id with
| None -> None
| Some kn -> Some (Mod_subst.subst_kn subst kn)
-let subst_md (subst, (local, id, b, t)) =
- (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t)
+let subst_md (subst, (local, id, b, t, deprecation)) =
+ (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation)
-let classify_md (local, _, _, _ as o) = Substitute o
+let classify_md (local, _, _, _, _ as o) = Substitute o
-let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
+ Vernacinterp.deprecation option -> obj =
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
@@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
subst_function = subst_md;
classify_function = classify_md}
-let register_ltac for_ml local id tac =
- ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
+let register_ltac for_ml local ?deprecation id tac =
+ ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation)))
-let redefine_ltac local kn tac =
- Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
+let redefine_ltac local ?deprecation kn tac =
+ Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation))
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 3af2f2a460..d5d36c97fa 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,6 +12,7 @@ open Names
open Libnames
open Tacexpr
open Geninterp
+open Vernacinterp
(** This module centralizes the various ways of registering tactics. *)
@@ -29,21 +30,26 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
type alias = KerName.t
(** Type of tactic alias, used in the [TacAlias] node. *)
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+ { alias_args: Id.t list;
+ alias_body: glob_tactic_expr;
+ alias_deprecation: Vernacinterp.deprecation option;
+ }
(** Contents of a tactic notation *)
val register_alias : alias -> alias_tactic -> unit
(** Register a tactic alias. *)
val interp_alias : alias -> alias_tactic
-(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+(** Recover the body of an alias. Raises an anomaly if it does not exist. *)
val check_alias : alias -> bool
(** Returns [true] if an alias is defined, false otherwise. *)
(** {5 Coq tactic definitions} *)
-val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
+val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
+ glob_tactic_expr -> unit
(** Register a new Ltac with the given name and body.
The first boolean indicates whether this is done from ML side, rather than
@@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
definition. It also puts the Ltac name in the nametab, so that it can be
used unqualified. *)
-val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
+val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t ->
+ glob_tactic_expr -> unit
(** Replace a Ltac with the given name and body. If the boolean flag is set
to true, then this is a local redefinition. *)
@@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr
val is_ltac_for_ml_tactic : KerName.t -> bool
(** Whether the tactic is defined from ML-side *)
+val tac_deprecation : KerName.t -> deprecation option
+(** The tactic deprecation notice, if any *)
+
type ltac_entry = {
tac_for_ml : bool;
(** Whether the tactic is defined from ML-side *)
@@ -68,6 +78,8 @@ type ltac_entry = {
(** The current body of the tactic *)
tac_redef : ModPath.t list;
(** List of modules redefining the tactic in reverse chronological order *)
+ tac_deprecation : deprecation option;
+ (** Deprecation notice to be printed when the tactic is used *)
}
val ltac_entries : unit -> ltac_entry KNmap.t
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 06d2711ad1..59b748e25e 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -398,5 +398,5 @@ type ltac_call_kind =
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
- | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
- | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 71e1edfd7d..3a0badb28f 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -398,5 +398,5 @@ type ltac_call_kind =
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
- | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
- | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 481fc30df2..1444800624 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -117,9 +117,26 @@ let intern_constr_reference strict ist qid =
(* Internalize an isolated reference in position of tactic *)
+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)
+
+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)
+
let intern_isolated_global_tactic_reference qid =
let loc = qid.CAst.loc in
- TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
+ let kn = Tacenv.locate_tactic qid in
+ Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+ Tacenv.tac_deprecation kn;
+ TacCall (Loc.tag ?loc (ArgArg (loc,kn),[]))
let intern_isolated_tactic_reference strict ist qid =
(* An ltac reference *)
@@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid =
(* Internalize an applied tactic reference *)
let intern_applied_global_tactic_reference qid =
- ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid)
+ let loc = qid.CAst.loc in
+ let kn = Tacenv.locate_tactic qid in
+ Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+ Tacenv.tac_deprecation kn;
+ ArgArg (loc,kn)
let intern_applied_tactic_reference ist qid =
(* An ltac reference *)
@@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function
(* For extensions *)
| TacAlias (loc,(s,l)) ->
+ let alias = Tacenv.interp_alias s in
+ Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation;
let l = List.map (intern_tacarg !strict_check false ist) l in
ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
| TacML (loc,(opn,l)) ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9d1cc1643c..a0446bd6a0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -141,16 +141,6 @@ let extract_trace ist = match TacStore.get ist.extra f_trace with
| None -> []
| Some l -> l
-module Value = struct
-
- include Taccoerce.Value
-
- let of_closure ist tac =
- let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
- of_tacvalue closure
-
-end
-
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
let catching_error call_trace fail (e, info) =
@@ -312,11 +302,11 @@ let interp_name ist env sigma = function
| Name id -> Name (interp_ident ist env sigma id)
let interp_intro_pattern_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id)
+ try try_interp_ltac_var (coerce_to_intro_pattern sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found -> IntroNaming (IntroIdentifier id)
let interp_intro_pattern_naming_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id)
+ try try_interp_ltac_var (coerce_to_intro_pattern_naming sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found -> IntroIdentifier id
let interp_int ist ({loc;v=id} as locid) =
@@ -357,7 +347,7 @@ let interp_hyp_list ist env sigma l =
let interp_reference ist env sigma = function
| ArgArg (_,r) -> r
| ArgVar {loc;v=id} ->
- try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id)
+ try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
@@ -451,7 +441,7 @@ let default_fresh_id = Id.of_string "H"
let interp_fresh_id ist env sigma l =
let extract_ident ist env sigma id =
- try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
+ try try_interp_ltac_var (coerce_to_ident_not_fresh sigma)
ist (Some (env,sigma)) (make id)
with Not_found -> id in
let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in
@@ -474,7 +464,7 @@ let interp_fresh_id ist env sigma l =
(* Extract the uconstr list from lfun *)
let extract_ltac_constr_context ist env sigma =
let add_uconstr id v map =
- try Id.Map.add id (coerce_to_uconstr env v) map
+ try Id.Map.add id (coerce_to_uconstr v) map
with CannotCoerceTo _ -> map
in
let add_constr id v map =
@@ -799,7 +789,7 @@ and interp_or_and_intro_pattern ist env sigma = function
and interp_intro_pattern_list_as_list ist env sigma = function
| [{loc;v=IntroNaming (IntroIdentifier id)}] as l ->
- (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
+ (try sigma, coerce_to_intro_pattern_list ?loc sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
List.fold_left_map (interp_intro_pattern ist env) sigma l)
| l -> List.fold_left_map (interp_intro_pattern ist env) sigma l
@@ -842,7 +832,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
try try_interp_ltac_var
- (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
+ (coerce_to_decl_or_quant_hyp sigma) ist (Some (env,sigma)) (make id)
with Not_found -> NamedHyp id
let interp_binding ist env sigma {loc;v=(b,c)} =
@@ -1125,17 +1115,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias (loc,(s,l)) ->
- let (ids, body) = Tacenv.interp_alias s in
+ let alias = Tacenv.interp_alias s in
let (>>=) = Ftactic.bind in
let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
let tac l =
let addvar x v accu = Id.Map.add x v accu in
- let lfun = List.fold_right2 addvar ids l ist.lfun in
+ let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
let ist = {
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
- val_interp ist body >>= fun v ->
+ val_interp ist alias.Tacenv.alias_body >>= fun v ->
Ftactic.lift (tactic_of_value ist v)
in
let tac =
@@ -1147,7 +1137,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
some more elaborate solution will have to be used. *)
in
let tac =
- let len1 = List.length ids in
+ let len1 = List.length alias.Tacenv.alias_args in
let len2 = List.length l in
if len1 = len2 then tac
else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
@@ -1860,6 +1850,31 @@ let eval_tactic_ist ist t =
Proofview.tclLIFT db_initialize <*>
interp_tactic ist t
+(** FFI *)
+
+module Value = struct
+
+ include Taccoerce.Value
+
+ let of_closure ist tac =
+ let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
+ of_tacvalue closure
+
+ (** Apply toplevel tactic values *)
+ let apply (f : value) (args: value list) =
+ let fold arg (i, vars, lfun) =
+ let id = Id.of_string ("x" ^ string_of_int i) in
+ let x = Reference (ArgVar CAst.(make id)) in
+ (succ i, x :: vars, Id.Map.add id arg lfun)
+ in
+ let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+ let lfun = Id.Map.add (Id.of_string "F") f lfun in
+ let ist = { (default_ist ()) with lfun = lfun; } in
+ let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+ eval_tactic_ist ist tac
+
+end
+
(* globalization + interpretation *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index fd2d96bd62..f9883e4441 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -28,6 +28,7 @@ sig
val to_list : t -> t list option
val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
+ val apply : t -> t list -> unit Proofview.tactic
end
(** Values for interpretation *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 20:34:15 +0000