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/extratactics.ml42
-rw-r--r--plugins/ltac/g_eqdecide.mlg (renamed from plugins/ltac/g_eqdecide.ml4)8
-rw-r--r--plugins/ltac/g_tactic.mlg (renamed from plugins/ltac/g_tactic.ml4)452
-rw-r--r--plugins/ltac/pptactic.ml51
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/taccoerce.ml32
-rw-r--r--plugins/ltac/taccoerce.mli14
-rw-r--r--plugins/ltac/tacentries.ml34
-rw-r--r--plugins/ltac/tacentries.mli4
-rw-r--r--plugins/ltac/tacinterp.ml14
11 files changed, 413 insertions, 384 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/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 660e29ca82..f24ab2bddb 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 }
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_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/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 cc9c2046d8..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
@@ -199,15 +198,16 @@ let id_of_name = function
let basename = Nametab.basename_of_global ref in
basename
| Sort s ->
- begin
+ begin
match ESorts.kind sigma s with
- | Sorts.Prop _ -> Label.to_id (Label.make "Prop")
- | Sorts.Type _ -> Label.to_id (Label.make "Type")
- end
+ | Sorts.Prop -> Label.to_id (Label.make "Prop")
+ | Sorts.Set -> Label.to_id (Label.make "Set")
+ | Sorts.Type _ -> Label.to_id (Label.make "Type")
+ end
| _ -> 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
@@ -220,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")
@@ -254,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
@@ -298,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 =
@@ -327,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
@@ -355,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..fac464a628 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
@@ -398,7 +398,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
@@ -554,13 +554,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,10 +583,11 @@ 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
@@ -604,7 +610,7 @@ 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
@@ -612,7 +618,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
let v' = Taccoerce.Value.cast (topwit (prj 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 +630,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 "_"
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 2bfbbe2e16..9bba9ba71f 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -72,9 +72,9 @@ 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
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9d1cc1643c..d9ac96d894 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -312,11 +312,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 +357,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 +451,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 +474,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 +799,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 +842,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)} =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 08:16:13 +0000