aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/g_ground.mlg2
-rw-r--r--plugins/ltac/coretactics.mlg8
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg10
-rw-r--r--plugins/ltac/g_tactic.mlg124
-rw-r--r--plugins/ltac/pptactic.ml32
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/tacentries.ml10
-rw-r--r--plugins/ltac/tacexpr.ml10
-rw-r--r--plugins/ltac/tacexpr.mli10
-rw-r--r--plugins/ltac/tacintern.ml26
-rw-r--r--plugins/ltac/tacinterp.ml16
-rw-r--r--plugins/ltac/tacsubst.ml14
-rw-r--r--plugins/ltac/tactic_debug.ml2
-rw-r--r--plugins/ltac/tauto.ml6
-rw-r--r--plugins/setoid_ring/newring.ml10
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrparser.mlg10
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
20 files changed, 150 insertions, 150 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 1128a78093..a212d13453 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -66,7 +66,7 @@ let default_intuition_tac =
let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
Tacenv.register_ml_tactic name [| tac |];
- Tacexpr.TacML (Loc.tag (entry, []))
+ Tacexpr.TacML (CAst.make (entry, []))
let (set_default_solver, default_solver, print_default_solver) =
Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index 6388906f5e..d9338f0421 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -333,7 +333,7 @@ open Tacexpr
let initial_atomic () =
let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
let iter (s, t) =
- let body = TacAtom (Loc.tag t) in
+ let body = TacAtom (CAst.make t) in
Tacenv.register_ltac false false (Names.Id.of_string s) body
in
let () = List.iter iter
@@ -348,7 +348,7 @@ let initial_atomic () =
List.iter iter
[ "idtac",TacId [];
"fail", TacFail(TacLocal,ArgArg 0,[]);
- "fresh", TacArg(Loc.tag @@ TacFreshId [])
+ "fresh", TacArg(CAst.make @@ TacFreshId [])
]
let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
@@ -379,8 +379,8 @@ let initial_tacticals () =
let varn n = Reference (ArgVar (CAst.make (idn n))) in
let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
List.iter iter [
- "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
- "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
+ "first", TacFun ([Name (idn 0)], TacML (CAst.make (initial_entry "first", [varn 0])));
+ "solve", TacFun ([Name (idn 0)], TacML (CAst.make (initial_entry "solve", [varn 0])));
]
let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 70e5ab38bc..04a8ae1746 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -767,7 +767,7 @@ let case_eq_intros_rewrite x =
let rec find_a_destructable_match sigma t =
let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in
let cl = [cl, (None, None), None], None in
- let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in
+ let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
match EConstr.kind sigma t with
| Case (_,_,x,_) when closed0 sigma x ->
if isVar sigma x then
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c58c8556c5..9730fc7fd8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -33,7 +33,7 @@ open Pltac
let fail_default_value = Locus.ArgArg 0
let arg_of_expr = function
- TacArg (loc,a) -> a
+ TacArg { CAst.v } -> v
| e -> Tacexp (e:raw_tactic_expr)
let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
@@ -162,9 +162,9 @@ GRAMMAR EXTEND Gram
| g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
l = LIST0 message_token -> { TacFail (g,n,l) }
| st = simple_tactic -> { st }
- | a = tactic_arg -> { TacArg(Loc.tag ~loc a) }
+ | a = tactic_arg -> { TacArg(CAst.make ~loc a) }
| r = reference; la = LIST0 tactic_arg_compat ->
- { TacArg(Loc.tag ~loc @@ TacCall (Loc.tag ~loc (r,la))) } ]
+ { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ]
| "0"
[ "("; a = tactic_expr; ")" -> { a }
| "["; ">"; tg = tactic_then_gen; "]" -> {
@@ -173,7 +173,7 @@ GRAMMAR EXTEND Gram
| Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
| None -> TacDispatch tf
end }
- | a = tactic_atom -> { TacArg (Loc.tag ~loc a) } ] ]
+ | a = tactic_atom -> { TacArg (CAst.make ~loc a) } ] ]
;
failkw:
[ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
@@ -223,7 +223,7 @@ GRAMMAR EXTEND Gram
;
tactic_atom:
[ [ n = integer -> { TacGeneric (genarg_of_int n) }
- | r = reference -> { TacCall (Loc.tag ~loc (r,[])) }
+ | r = reference -> { TacCall (CAst.make ~loc (r,[])) }
| "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
;
match_key:
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 571595be70..0ce0fbd0cd 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -529,178 +529,178 @@ GRAMMAR EXTEND Gram
[ [
(* Basic tactics *)
IDENT "intros"; pl = ne_intropatterns ->
- { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,pl)) }
+ { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,pl)) }
| IDENT "intros" ->
- { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
+ { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
| IDENT "eintros"; pl = ne_intropatterns ->
- { TacAtom (Loc.tag ~loc @@ TacIntroPattern (true,pl)) }
+ { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) }
| IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,false,cl,inhyp)) }
+ inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) }
| IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,true,cl,inhyp)) }
+ inhyp = in_hyp_as -> { TacAtom (CAst.make ~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 @@ TacApply (false,false,cl,inhyp)) }
+ inhyp = in_hyp_as -> { TacAtom (CAst.make ~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 @@ TacApply (false,true,cl,inhyp)) }
+ inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (false,true,cl,inhyp)) }
| IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- { TacAtom (Loc.tag ~loc @@ TacElim (false,cl,el)) }
+ { TacAtom (CAst.make ~loc @@ TacElim (false,cl,el)) }
| IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- { 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) }
+ { TacAtom (CAst.make ~loc @@ TacElim (true,cl,el)) }
+ | IDENT "case"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase false icl) }
+ | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase true icl) }
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
- { TacAtom (Loc.tag ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
+ { TacAtom (CAst.make ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
| "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
- { TacAtom (Loc.tag ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
+ { TacAtom (CAst.make ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
| 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)) }
+ { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "pose"; b = constr; na = as_name ->
- { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
+ { TacAtom (CAst.make ~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)) }
+ { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
| IDENT "epose"; b = constr; na = as_name ->
- { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
+ { TacAtom (CAst.make ~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)) }
+ { let (id,c) = bl in TacAtom (CAst.make ~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 @@ TacLetTac (false,na,c,p,true,None)) }
+ { TacAtom (CAst.make ~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)) }
+ { let (id,c) = bl in TacAtom (CAst.make ~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 @@ TacLetTac (true,na,c,p,true,None)) }
+ { TacAtom (CAst.make ~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 @@ TacLetTac (false,na,c,p,false,e)) }
+ { TacAtom (CAst.make ~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 @@ TacLetTac (true,na,c,p,false,e)) }
+ { TacAtom (CAst.make ~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)) }
+ TacAtom (CAst.make ?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)) }
+ TacAtom (CAst.make ?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)) }
+ TacAtom (CAst.make ?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)) }
+ TacAtom (CAst.make ?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)) }
+ TacAtom (CAst.make ?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)) }
+ TacAtom (CAst.make ?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 @@ TacAssert (false,true,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
| IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,None,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) }
| IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,None,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (true,true,None,ipat,c)) }
| IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- { TacAtom (Loc.tag ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
| IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- { TacAtom (Loc.tag ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
+ { TacAtom (CAst.make ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
| IDENT "generalize"; c = constr ->
- { TacAtom (Loc.tag ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
+ { TacAtom (CAst.make ~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 @@ TacGeneralize (List.map gen_everywhere (c::l))) }
+ TacAtom (CAst.make ~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 @@ TacGeneralize (((nl,c),na)::l)) }
+ { TacAtom (CAst.make ~loc @@ TacGeneralize (((nl,c),na)::l)) }
(* Derived basic tactics *)
| IDENT "induction"; ic = induction_clause_list ->
- { TacAtom (Loc.tag ~loc @@ TacInductionDestruct (true,false,ic)) }
+ { TacAtom (CAst.make ~loc @@ TacInductionDestruct (true,false,ic)) }
| IDENT "einduction"; ic = induction_clause_list ->
- { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(true,true,ic)) }
+ { TacAtom (CAst.make ~loc @@ TacInductionDestruct(true,true,ic)) }
| IDENT "destruct"; icl = induction_clause_list ->
- { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,false,icl)) }
+ { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,false,icl)) }
| IDENT "edestruct"; icl = induction_clause_list ->
- { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,true,icl)) }
+ { TacAtom (CAst.make ~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 @@ TacRewrite (false,l,cl,t)) }
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (false,l,cl,t)) }
| IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (true,l,cl,t)) }
+ cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (true,l,cl,t)) }
| IDENT "dependent"; k =
[ 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 @@ TacInversion (DepInversion (k,co,ids),hyp)) }
+ { TacAtom (CAst.make ~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 @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
+ { TacAtom (CAst.make ~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 @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
+ { TacAtom (CAst.make ~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 @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
+ { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
| IDENT "inversion"; hyp = quantified_hypothesis;
"using"; c = constr; cl = in_hyp_list ->
- { TacAtom (Loc.tag ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
+ { TacAtom (CAst.make ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
(* Conversion *)
| IDENT "red"; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Red false, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Red false, cl)) }
| IDENT "hnf"; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Hnf, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Hnf, cl)) }
| IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Simpl (all_with d, po), cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Simpl (all_with d, po), cl)) }
| IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv s, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Cbv s, cl)) }
| IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Cbn s, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Cbn s, cl)) }
| IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Lazy s, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Lazy s, cl)) }
| IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv (all_with delta), cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Cbv (all_with delta), cl)) }
| IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (CbvVm po, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (CbvVm po, cl)) }
| IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (CbvNative po, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (CbvNative po, cl)) }
| IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Unfold ul, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Unfold ul, cl)) }
| IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Fold l, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Fold l, cl)) }
| IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
- { TacAtom (Loc.tag ~loc @@ TacReduce (Pattern pl, cl)) }
+ { TacAtom (CAst.make ~loc @@ TacReduce (Pattern pl, cl)) }
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
| 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)) }
+ TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) }
] ]
;
END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b219ee25ca..50cfb6d004 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -294,7 +294,7 @@ let string_of_genarg_arg (ArgumentType arg) =
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))
+ let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg))
let is_genarg tag wit =
let ArgT.Any tag = tag in
@@ -350,9 +350,9 @@ let string_of_genarg_arg (ArgumentType arg) =
pr_extend_gen (pr_farg prtac)
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
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) 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
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args
(**********************************************************************)
(* The tactic printer *)
@@ -579,7 +579,7 @@ let pr_goal_selector ~toplevel s =
pr_gen arg
else
str name ++ str ":" ++ surround (pr_gen arg)
- | _ -> pr_arg (TacArg (Loc.tag t)) in
+ | _ -> pr_arg (TacArg (CAst.make t)) in
hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++
str " :=" ++ brk (1,1) ++ pr t)
@@ -1045,30 +1045,30 @@ let pr_goal_selector ~toplevel s =
| TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
- | TacAtom (loc,t) ->
+ | TacAtom { CAst.loc; v=t } ->
pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
- | TacArg(_,Tacexp e) ->
+ | TacArg { CAst.v=Tacexp e } ->
pr_tac inherited e, latom
- | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
+ | TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } ->
keyword "constr:" ++ pr.pr_constr c, latom
- | TacArg(_,ConstrMayEval c) ->
+ | TacArg { CAst.v=ConstrMayEval c } ->
pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
- | TacArg(_,TacFreshId l) ->
+ | TacArg { CAst.v=TacFreshId l } ->
primitive "fresh" ++ pr_fresh_ids l, latom
- | TacArg(_,TacGeneric arg) ->
+ | TacArg { CAst.v=TacGeneric arg } ->
pr.pr_generic arg, latom
- | TacArg(_,TacCall(_,(f,[]))) ->
+ | TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
pr.pr_reference f, latom
- | TacArg(_,TacCall(loc,(f,l))) ->
+ | TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
pr_with_comments ?loc (hov 1 (
pr.pr_reference f ++ spc ()
++ prlist_with_sep spc pr_tacarg l)),
lcall
- | TacArg (_,a) ->
+ | TacArg { CAst.v=a } ->
pr_tacarg a, latom
- | TacML (loc,(s,l)) ->
+ | TacML { CAst.loc; v=(s,l) } ->
pr_with_comments ?loc (pr.pr_extend 1 s l), lcall
- | TacAlias (loc,(kn,l)) ->
+ | TacAlias { CAst.loc; v=(kn,l) } ->
pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom
)
in
@@ -1087,7 +1087,7 @@ let pr_goal_selector ~toplevel s =
| TacNumgoals ->
keyword "numgoals"
| (TacCall _|Tacexp _ | TacGeneric _) as a ->
- hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.tag a))))
+ hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (CAst.make a))))
in pr_tac
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index db7dcfa6ef..3eb049dbab 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -251,7 +251,7 @@ let string_of_call ck =
| Tacexpr.LtacVarCall (id, t) -> Names.Id.print id
| Tacexpr.LtacAtomCall te ->
(Pptactic.pr_glob_tactic (Global.env ())
- (Tacexpr.TacAtom (Loc.tag te)))
+ (Tacexpr.TacAtom (CAst.make te)))
| Tacexpr.LtacConstrInterp (c, _) ->
pr_glob_constr_env (Global.env ()) c
| Tacexpr.LtacMLCall te ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7d917c58fe..16cb75ea2f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1958,7 +1958,7 @@ let add_setoid atts binders a aeq t n =
let make_tactic name =
let open Tacexpr in
let tacqid = Libnames.qualid_of_string name in
- TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, []))))
+ TacArg (CAst.make @@ (TacCall (CAst.make (tacqid, []))))
let warn_add_morphism_deprecated =
CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 1b212334ce..188d5de7de 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -177,7 +177,7 @@ let add_tactic_entry (kn, ml, tg) state =
TacGeneric arg
in
let l = List.map map l in
- (TacAlias (Loc.tag ~loc (kn,l)):raw_tactic_expr)
+ (TacAlias (CAst.make ~loc (kn,l)):raw_tactic_expr)
in
let () =
if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
@@ -349,7 +349,7 @@ let extend_atomic_tactic name entries =
| TacNonTerm (_, (symb, _)) ->
let EntryName (typ, e) = prod_item_of_symbol 0 symb in
let Genarg.Rawwit wit = typ in
- let inj x = TacArg (Loc.tag @@ TacGeneric (Genarg.in_gen typ x)) in
+ let inj x = TacArg (CAst.make @@ TacGeneric (Genarg.in_gen typ x)) in
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
@@ -363,7 +363,7 @@ let extend_atomic_tactic name entries =
| Some (id, args) ->
let args = List.map (fun a -> Tacexp a) args in
let entry = { mltac_name = name; mltac_index = i } in
- let body = TacML (Loc.tag (entry, args)) in
+ let body = TacML (CAst.make (entry, args)) in
Tacenv.register_ltac false false (Names.Id.of_string id) body
in
List.iteri add_atomic entries
@@ -379,7 +379,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
let ids = List.map_filter get_id prods in
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
+ let tac = TacML (CAst.make (entry, List.map map ids)) in
add_glob_tactic_notation false ~level ?deprecation prods true ids tac
in
List.iteri iter (List.rev prods);
@@ -664,7 +664,7 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
(** Arguments are not passed directly to the ML tactic in the TacML node,
the ML tactic retrieves its arguments in the [ist] environment instead.
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 body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, [])))in
let id = Names.Id.of_string name in
let obj () = Tacenv.register_ltac true false id body ?deprecation in
let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 8731cbf60d..9435d0b911 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -167,7 +167,7 @@ type 'a gen_tactic_arg =
| TacGeneric of 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
- | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located
+ | TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
| TacFreshId of string or_var list
| Tacexp of 'tacexpr
| TacPretype of 'trm
@@ -189,7 +189,7 @@ constraint 'a = <
'r : ltac refs, 'n : idents, 'l : levels *)
and 'a gen_tactic_expr =
- | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
+ | TacAtom of ('a gen_atomic_tactic_expr) CAst.t
| TacThen of
'a gen_tactic_expr *
'a gen_tactic_expr
@@ -245,12 +245,12 @@ and 'a gen_tactic_expr =
| TacMatchGoal of lazy_flag * direction_flag *
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
- | TacArg of 'a gen_tactic_arg located
+ | TacArg of 'a gen_tactic_arg CAst.t
| TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
- | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
+ | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) CAst.t
(* For syntax extensions *)
- | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
+ | TacAlias of (KerName.t * 'a gen_tactic_arg list) CAst.t
constraint 'a = <
term:'t;
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9958d6dcda..1527724420 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -167,7 +167,7 @@ type 'a gen_tactic_arg =
| TacGeneric of 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
- | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located
+ | TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
| TacFreshId of string or_var list
| Tacexp of 'tacexpr
| TacPretype of 'trm
@@ -189,7 +189,7 @@ constraint 'a = <
'r : ltac refs, 'n : idents, 'l : levels *)
and 'a gen_tactic_expr =
- | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
+ | TacAtom of ('a gen_atomic_tactic_expr) CAst.t
| TacThen of
'a gen_tactic_expr *
'a gen_tactic_expr
@@ -245,12 +245,12 @@ and 'a gen_tactic_expr =
| TacMatchGoal of lazy_flag * direction_flag *
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
- | TacArg of 'a gen_tactic_arg located
+ | TacArg of 'a gen_tactic_arg CAst.t
| TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
- | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
+ | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) CAst.t
(* For syntax extensions *)
- | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
+ | TacAlias of (KerName.t * 'a gen_tactic_arg list) CAst.t
constraint 'a = <
term:'t;
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ebec3c887c..85c6348b52 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -137,7 +137,7 @@ let intern_isolated_global_tactic_reference 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),[]))
+ TacCall (CAst.make ?loc (ArgArg (loc,kn),[]))
let intern_isolated_tactic_reference strict ist qid =
(* An ltac reference *)
@@ -587,10 +587,10 @@ let rec intern_atomic lf ist x =
and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
and intern_tactic_seq onlytac ist = function
- | TacAtom (loc,t) ->
+ | TacAtom { loc; v=t } ->
let lf = ref ist.ltacvars in
let t = intern_atomic lf ist t in
- !lf, TacAtom (Loc.tag ?loc:(adjust_loc loc) t)
+ !lf, TacAtom (CAst.make ?loc:(adjust_loc loc) t)
| TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
| TacLetIn (isrec,l,u) ->
let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in
@@ -659,27 +659,27 @@ and intern_tactic_seq onlytac ist = function
| TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l)
| TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
| TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
- | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+ | TacArg { loc; v=a } -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
| TacSelect (sel, tac) ->
ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac)
(* For extensions *)
- | TacAlias (loc,(s,l)) ->
+ | TacAlias { loc; v=(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)) ->
+ ist.ltacvars, TacAlias (CAst.make ?loc (s,l))
+ | TacML { loc; v=(opn,l) } ->
let _ignore = Tacenv.interp_ml_tactic opn in
- ist.ltacvars, TacML (loc, (opn,List.map (intern_tacarg !strict_check false ist) l))
+ ist.ltacvars, TacML CAst.(make ?loc (opn,List.map (intern_tacarg !strict_check false ist) l))
and intern_tactic_as_arg loc onlytac ist a =
match intern_tacarg !strict_check onlytac ist a with
| TacCall _ | Reference _
- | TacGeneric _ as a -> TacArg (loc,a)
+ | TacGeneric _ as a -> TacArg CAst.(make ?loc a)
| Tacexp a -> a
| ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
- if onlytac then error_tactic_expected ?loc else TacArg (loc,a)
+ if onlytac then error_tactic_expected ?loc else TacArg CAst.(make ?loc a)
and intern_tactic_or_tacarg ist = intern_tactic false ist
@@ -692,9 +692,9 @@ and intern_tactic_fun ist (var,body) =
and intern_tacarg strict onlytac ist = function
| Reference r -> intern_non_tactic_reference strict ist r
| ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
- | TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f
- | TacCall (loc,(f,l)) ->
- TacCall (Loc.tag ?loc (
+ | TacCall { loc; v=(f,[]) } -> intern_isolated_tactic_reference strict ist f
+ | TacCall { loc; v=(f,l) } ->
+ TacCall (CAst.make ?loc (
intern_applied_tactic_reference ist f,
List.map (intern_tacarg !strict_check false ist) l))
| TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 5bfb0f79fb..cb3a0aaed9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1018,7 +1018,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
| TacLetIn (false,l,u) -> interp_letin ist l u
| TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
| TacMatch (lz,c,lmr) -> interp_match ist lz c lmr
- | TacArg (loc,a) -> interp_tacarg ist a
+ | TacArg {loc;v} -> interp_tacarg ist v
| t ->
(** Delayed evaluation *)
Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t)))
@@ -1036,7 +1036,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
and eval_tactic ist tac : unit Proofview.tactic = match tac with
- | TacAtom (loc,t) ->
+ | TacAtom {loc;v=t} ->
let call = LtacAtomCall t in
push_trace(loc,call) ist >>= fun trace ->
Profile_ltac.do_profile "eval_tactic:2" trace
@@ -1116,7 +1116,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
eval_tactic ist tac
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
- | TacAlias (loc,(s,l)) ->
+ | TacAlias {loc; v=(s,l)} ->
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
@@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
in
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
- | TacML (loc,(opn,l)) ->
+ | TacML {loc; v=(opn,l)} ->
push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist >>= fun trace ->
let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
let tac = Tacenv.interp_ml_tactic opn in
@@ -1201,9 +1201,9 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Ftactic.return (Value.of_constr c_interp))
end
- | TacCall (loc,(r,[])) ->
+ | TacCall { v=(r,[]) } ->
interp_ltac_reference true ist r
- | TacCall (loc,(f,l)) ->
+ | TacCall { loc; v=(f,l) } ->
let (>>=) = Ftactic.bind in
interp_ltac_reference true ist f >>= fun fv ->
Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs ->
@@ -1337,7 +1337,7 @@ and interp_letrec ist llc u =
Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
let lref = ref ist.lfun in
let fold accu ({v=na}, b) =
- let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
+ let v = of_tacvalue (VRec (lref, TacArg (CAst.make b))) in
Name.fold_right (fun id -> Id.Map.add id v) na accu
in
let lfun = List.fold_left fold ist.lfun llc in
@@ -1875,7 +1875,7 @@ module Value = struct
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
+ let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
eval_tactic_ist ist tac
end
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 9173e23b89..caaa547a07 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -173,7 +173,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp)
and subst_tactic subst (t:glob_tactic_expr) = match t with
- | TacAtom (_loc,t) -> TacAtom (Loc.tag @@ subst_atomic subst t)
+ | TacAtom { CAst.v=t } -> TacAtom (CAst.make @@ subst_atomic subst t)
| TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
| TacLetIn (r,l,u) ->
let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
@@ -220,22 +220,22 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
| TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
| TacComplete tac -> TacComplete (subst_tactic subst tac)
- | TacArg (_,a) -> TacArg (Loc.tag @@ subst_tacarg subst a)
+ | TacArg { CAst.v=a } -> TacArg (CAst.make @@ subst_tacarg subst a)
| TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac)
(* For extensions *)
- | TacAlias (_,(s,l)) ->
+ | TacAlias { CAst.v=(s,l) } ->
let s = subst_kn subst s in
- TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l))
- | TacML (loc,(opn,l)) -> TacML (loc, (opn,List.map (subst_tacarg subst) l))
+ TacAlias (CAst.make (s,List.map (subst_tacarg subst) l))
+ | TacML { CAst.loc; v=(opn,l)} -> TacML CAst.(make ?loc (opn,List.map (subst_tacarg subst) l))
and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
and subst_tacarg subst = function
| Reference r -> Reference (subst_reference subst r)
| ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
- | TacCall (loc,(f,l)) ->
- TacCall (Loc.tag ?loc (subst_reference subst f, List.map (subst_tacarg subst) l))
+ | TacCall { CAst.loc; v=(f,l) } ->
+ TacCall CAst.(make ?loc (subst_reference subst f, List.map (subst_tacarg subst) l))
| TacFreshId _ as x -> x
| TacPretype c -> TacPretype (subst_glob_constr subst c)
| TacNumgoals -> TacNumgoals
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 6bab8d0353..877d4ee758 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -365,7 +365,7 @@ let explain_ltac_call_trace last trace loc =
Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
| Tacexpr.LtacAtomCall te ->
quote (Pptactic.pr_glob_tactic (Global.env())
- (Tacexpr.TacAtom (Loc.tag te)))
+ (Tacexpr.TacAtom (CAst.make te)))
| Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
quote (Printer.pr_glob_constr_env (Global.env()) c) ++
(if not (Id.Map.is_empty vars) then
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 299bc7ea4d..561bfc5d7c 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -191,7 +191,7 @@ let make_unfold name =
let u_not = make_unfold "not"
let reduction_not_iff _ ist =
- let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
+ let make_reduce c = TacAtom (CAst.make @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
let tac = match !negation_unfolding with
| true -> make_reduce [u_not]
| false -> TacId []
@@ -244,7 +244,7 @@ let with_flags flags _ ist =
let x = CAst.make @@ Id.of_string "x" in
let arg = Val.Dyn (tag_tauto_flags, flags) in
let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
- eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
+ eval_tactic_ist ist (TacArg (CAst.make @@ TacCall (CAst.make (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
let register_tauto_tactic tac name0 args =
let ids = List.map (fun id -> Id.of_string id) args in
@@ -252,7 +252,7 @@ let register_tauto_tactic tac name0 args =
let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in
let entry = { mltac_name = name; mltac_index = 0 } in
let () = Tacenv.register_ml_tactic name [| tac |] in
- let tac = TacFun (ids, TacML (Loc.tag (entry, []))) in
+ let tac = TacFun (ids, TacML (CAst.make (entry, []))) in
let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in
Mltop.declare_cache_obj obj tauto_plugin
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a2dce621d9..4109e9cf38 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -129,7 +129,7 @@ let closed_term_ast =
fun l ->
let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
TacFun([Name(Id.of_string"t")],
- TacML(Loc.tag (tacname,
+ TacML(CAst.make (tacname,
[TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
(*
@@ -160,7 +160,7 @@ let decl_constant na univs c =
(* Calling a global tactic *)
let ltac_call tac (args:glob_tactic_arg list) =
- TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args)))
+ TacArg(CAst.make @@ TacCall (CAst.make (ArgArg(Loc.tag @@ Lazy.force tac),args)))
let dummy_goal env sigma =
let (gl,_,sigma) =
@@ -197,7 +197,7 @@ let exec_tactic env evd n f args =
(** Build the getter *)
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
- let get_res = TacML (Loc.tag (get_res, [TacGeneric n])) in
+ let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in
let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
(** Evaluate the whole result *)
let gl = dummy_goal env evd in
@@ -557,7 +557,7 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
closed_term_ast (List.map Smartlocate.global_with_alias lc)
| None ->
let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
- TacArg(Loc.tag (TacCall(Loc.tag (t,[]))))
+ TacArg(CAst.make (TacCall(CAst.make (t,[]))))
let make_hyp env evd c =
let t = Retyping.get_type_of env !evd c in
@@ -582,7 +582,7 @@ let interp_power env evdref pow =
match pow with
| None ->
let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
- (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|])
+ (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|])
| Some (tac, spec) ->
let tac =
match tac with
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ddfd4c101f..80d421b9fc 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -859,7 +859,7 @@ let ssr_n_tac seed n gl =
with Not_found ->
if n = -1 then fail "The ssreflect library was not loaded"
else fail ("The tactic "^name^" was not found") in
- let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+ let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
Proofview.V82.of_tactic (Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)) gl
let donetac n gl = ssr_n_tac "done" n gl
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 52240f5896..7c91860228 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1545,9 +1545,9 @@ let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
let swaptacarg (loc, b) = (b, []), Some (TacId [])
let check_seqtacarg dir arg = match snd arg, dir with
- | ((true, []), Some (TacAtom (loc, _))), L2R ->
+ | ((true, []), Some (TacAtom { CAst.loc })), L2R ->
CErrors.user_err ?loc (str "expected \"last\"")
- | ((false, []), Some (TacAtom (loc, _))), R2L ->
+ | ((false, []), Some (TacAtom { CAst.loc })), R2L ->
CErrors.user_err ?loc (str "expected \"first\"")
| _, _ -> arg
@@ -1677,7 +1677,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (*
| ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in
let tacname = ssrtac_name name in () *)
-let ssrtac_atom ?loc name args = TacML (Loc.tag ?loc (ssrtac_entry name 0, args))
+let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args))
let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args
let tclintros_expr ?loc tac ipats =
@@ -1704,7 +1704,7 @@ END
GRAMMAR EXTEND Gram
GLOBAL: tactic_expr;
- ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { Loc.tag ~loc (Tacexp tac) } ]];
+ ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
END
@@ -1724,7 +1724,7 @@ let ssrautoprop gl =
let tacname =
try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
- let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+ let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
with Not_found -> V82.of_tactic (Auto.full_trivial []) gl
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 5dcbf9b3ef..142d1ac790 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1388,7 +1388,7 @@ let () =
let () = Tacenv.register_ml_tactic name [|mltac|] in
let tac =
TacFun ([Name (Id.of_string "pattern")],
- TacML (Loc.tag ({ mltac_name = name; mltac_index = 0 }, []))) in
+ TacML (CAst.make ({ mltac_name = name; mltac_index = 0 }, []))) in
let obj () =
Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
Mltop.declare_cache_obj obj "ssrmatching_plugin"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:40:49 +0000