aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_ltac.ml417
-rw-r--r--plugins/ltac/g_obligations.ml42
-rw-r--r--plugins/ltac/g_tactic.ml451
-rw-r--r--plugins/ltac/ltac_plugin.mlpack1
-rw-r--r--plugins/ltac/pltac.mli3
-rw-r--r--plugins/ltac/pptactic.ml17
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/rewrite.ml37
-rw-r--r--plugins/ltac/taccoerce.ml18
-rw-r--r--plugins/ltac/tacentries.ml5
-rw-r--r--plugins/ltac/tacexpr.ml397
-rw-r--r--plugins/ltac/tacexpr.mli24
-rw-r--r--plugins/ltac/tacintern.ml105
-rw-r--r--plugins/ltac/tacinterp.ml72
-rw-r--r--plugins/ltac/tacsubst.ml17
16 files changed, 583 insertions, 187 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 61632e388e..2e90ce90cc 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -264,7 +264,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
(Declare.declare_universe_context false ctx;
Univ.ContextSet.empty)
in
- Loc.tag ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
+ CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
let eqs = List.map f lcsr in
let add_hints base = add_rew_rules base eqs in
List.iter add_hints bases
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 66268f9f9b..0c42a8bb28 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -38,11 +38,11 @@ let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat
let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
-let reference_to_id = function
- | Libnames.Ident (loc, id) -> CAst.make ?loc id
- | Libnames.Qualid (loc,_) ->
+let reference_to_id = CAst.map_with_loc (fun ?loc -> function
+ | Libnames.Ident id -> id
+ | Libnames.Qualid _ ->
CErrors.user_err ?loc
- (str "This expression should be a simple identifier.")
+ (str "This expression should be a simple identifier."))
let tactic_mode = Gram.entry_create "vernac:tactic_command"
@@ -198,7 +198,8 @@ GEXTEND Gram
verbose most of the time. *)
fresh_id:
[ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
- | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (CAst.make ~loc:!@loc id) ] ]
+ | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in
+ ArgVar (CAst.make ~loc:!@loc id) ] ]
;
constr_eval:
[ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -472,7 +473,7 @@ END
VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
| [ "Print" "Ltac" reference(r) ] ->
- [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
+ [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ]
END
VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
@@ -507,8 +508,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
VtSideff (List.map (function
| TacticDefinition ({CAst.v=r},_) -> r
- | TacticRedefinition (Ident (_,r),_) -> r
- | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
+ | TacticRedefinition ({CAst.v=Ident r},_) -> r
+ | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater
] -> [ fun ~atts ~st -> let open Vernacinterp in
Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
st
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 54e2ba960d..352e92c2a3 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -49,7 +49,7 @@ module Tactic = Pltac
open Pcoq
-let sigref = mkRefC (Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig"))
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 1b8a852d96..7534e27999 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -154,8 +154,7 @@ let mkTacCase with_evar = function
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
| [(clear,ElimOnIdent id),(None,None),None],None ->
- let id = CAst.(id.loc, id.v) in
- TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings)))
+ TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings)))
| ic ->
if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
then
@@ -175,7 +174,7 @@ let mkCLambdaN_simple bl c = match bl with
let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in
mkCLambdaN_simple_loc ?loc bl c
-let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
+let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc
let map_int_or_var f = function
| ArgArg x -> ArgArg (f x)
@@ -297,7 +296,7 @@ GEXTEND Gram
(* (A & B & C) is translated into (A,(B,C)) *)
let rec pairify = function
| ([]|[_]|[_;_]) as l -> l
- | t::q -> [t; Loc.tag ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+ | t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
in IntroAndPattern (pairify (si::tc)) ] ]
;
equality_intropattern:
@@ -312,28 +311,28 @@ GEXTEND Gram
;
nonsimple_intropattern:
[ [ l = simple_intropattern -> l
- | "*" -> Loc.tag ~loc:!@loc @@ IntroForthcoming true
- | "**" -> Loc.tag ~loc:!@loc @@ IntroForthcoming false ]]
+ | "*" -> CAst.make ~loc:!@loc @@ IntroForthcoming true
+ | "**" -> CAst.make ~loc:!@loc @@ IntroForthcoming false ]]
;
simple_intropattern:
[ [ pat = simple_intropattern_closed;
l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
- let loc0,pat = pat in
+ 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 ((loc1,c),(loc,pat))) in
- Loc.tag ~loc:!@loc @@ List.fold_right f l pat ] ]
+ IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in
+ CAst.make ~loc:!@loc @@ List.fold_right f l pat ] ]
;
simple_intropattern_closed:
- [ [ pat = or_and_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat)
- | pat = equality_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction pat
- | "_" -> Loc.tag ~loc:!@loc @@ IntroAction IntroWildcard
- | pat = naming_intropattern -> Loc.tag ~loc:!@loc @@ IntroNaming pat ] ]
+ [ [ 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 ] ]
;
simple_binding:
- [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c)
- | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ]
+ [ [ "("; id = ident; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (NamedHyp id, c)
+ | "("; n = natural; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (AnonHyp n, c) ] ]
;
bindings:
[ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
@@ -470,7 +469,7 @@ GEXTEND Gram
| -> None ] ]
;
or_and_intropattern_loc:
- [ [ ipat = or_and_intropattern -> ArgArg (Loc.tag ~loc:!@loc ipat)
+ [ [ ipat = or_and_intropattern -> ArgArg (CAst.make ~loc:!@loc ipat)
| locid = identref -> ArgVar locid ] ]
;
as_or_and_ipat:
@@ -478,13 +477,13 @@ GEXTEND Gram
| -> None ] ]
;
eqn_ipat:
- [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (Loc.tag ~loc:!@loc pat)
+ [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (CAst.make ~loc:!@loc pat)
| IDENT "_eqn"; ":"; pat = naming_intropattern ->
let loc = !@loc in
- warn_deprecated_eqn_syntax ~loc "H"; Some (Loc.tag ~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 (Loc.tag ~loc IntroAnonymous)
+ warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous)
| -> None ] ]
;
as_name:
@@ -525,7 +524,7 @@ GEXTEND Gram
IDENT "intros"; pl = ne_intropatterns ->
TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl))
| IDENT "intros" ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[Loc.tag ~loc:!@loc @@IntroForthcoming false]))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[CAst.make ~loc:!@loc @@IntroForthcoming false]))
| IDENT "eintros"; pl = ne_intropatterns ->
TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl))
@@ -577,31 +576,31 @@ GEXTEND Gram
| 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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ 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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ 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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ 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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ 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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ 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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ 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))
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index 3972b7aac3..ec96e1bbdd 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -1,3 +1,4 @@
+Tacexpr
Tacarg
Tacsubst
Tacenv
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 699e231106..6637de745e 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -10,7 +10,6 @@
(** Ltac parsing entries *)
-open Loc
open Pcoq
open Libnames
open Constrexpr
@@ -29,7 +28,7 @@ val quantified_hypothesis : quantified_hypothesis Gram.entry
val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
val int_or_var : int or_var Gram.entry
val simple_tactic : raw_tactic_expr Gram.entry
-val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
+val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
val in_clause : lident Locus.clause_expr Gram.entry
val clause_dft_concl : lident Locus.clause_expr Gram.entry
val tactic_arg : raw_tactic_arg Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fbb70cca68..11bb7a2341 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -14,11 +14,9 @@ open Namegen
open CErrors
open Util
open Constrexpr
-open Tacexpr
open Genarg
open Geninterp
open Stdarg
-open Tacarg
open Libnames
open Notation_term
open Misctypes
@@ -29,6 +27,9 @@ open Pputils
open Ppconstr
open Printer
+open Tacexpr
+open Tacarg
+
module Tag =
struct
@@ -181,9 +182,9 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_and_short_name pr (c,_) = pr c
- let pr_or_by_notation f = function
+ let pr_or_by_notation f = CAst.with_val (function
| AN v -> f v
- | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+ | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
let pr_located pr (loc,x) = pr x
@@ -382,9 +383,9 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_as_disjunctive_ipat prc ipatl =
keyword "as" ++ spc () ++
- pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
+ pr_or_var (fun {CAst.loc;v=p} -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
- let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
+ let pr_eqn_ipat {CAst.v=ipat} = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
let pr_with_induction_names prc = function
| None, None -> mt ()
@@ -426,7 +427,7 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_assumption prc prdc prlc ipat c = match ipat with
(* Use this "optimisation" or use only the general case ?*)
(* it seems that this "optimisation" is somehow more natural *)
- | Some (_,IntroNaming (IntroIdentifier id)) ->
+ | Some {CAst.v=IntroNaming (IntroIdentifier id)} ->
spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
| ipat ->
spc() ++ prc c ++ pr_as_ipat prdc ipat
@@ -744,7 +745,7 @@ let pr_goal_selector ~toplevel s =
| TacIntroPattern (ev,(_::_ as p)) ->
hov 1 (primitive (if ev then "eintros" else "intros") ++
(match p with
- | [_,Misctypes.IntroForthcoming false] -> mt ()
+ | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt ()
| _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p))
| TacApply (a,ev,cb,inhyp) ->
hov 1 (
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 7e6c6b20ee..5951f2b119 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,8 +17,8 @@ open Names
open Misctypes
open Environ
open Constrexpr
-open Tacexpr
open Notation_term
+open Tacexpr
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e0368153e5..d32a2faefc 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1773,12 +1773,11 @@ let rec strategy_of_ast = function
(* By default the strategy for "rewrite_db" is top-down *)
-let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l)
let declare_an_instance n s args =
(((CAst.make @@ Name n),None), Explicit,
- CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None),
- args))
+ CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args))
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
@@ -1792,17 +1791,17 @@ let anew_instance global binders instance fields =
let declare_instance_refl global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
in anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "reflexivity"),lemma)]
+ [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)]
let declare_instance_sym global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
in anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "symmetry"),lemma)]
+ [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)]
let declare_instance_trans global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
in anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)]
+ [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)]
let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
@@ -1826,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1);
- (Ident (Loc.tag @@ Id.of_string "PreOrder_Transitive"),lemma3)])
+ [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+ (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)])
| (None, Some lemma2, Some lemma3) ->
let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2);
- (Ident (Loc.tag @@ Id.of_string "PER_Transitive"),lemma3)])
+ [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2);
+ (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)])
| (Some lemma1, Some lemma2, Some lemma3) ->
let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1843,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), lemma1);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)])
+ [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)])
let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
@@ -1951,16 +1950,16 @@ let add_setoid global binders a aeq t n =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+ [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
let make_tactic name =
let open Tacexpr in
let tacpath = Libnames.qualid_of_string name in
- let tacname = Qualid (Loc.tag tacpath) in
- TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, [])))
+ let tacname = CAst.make @@ Qualid tacpath in
+ TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, []))))
let warn_add_morphism_deprecated =
CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
@@ -2010,7 +2009,7 @@ let add_morphism glob binders m s n =
let instance =
(((CAst.make @@ Name instance_id),None), Explicit,
CAst.make @@ CAppExpl (
- (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
+ (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 2c7ebb7458..3812a2ba29 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -147,7 +147,7 @@ let coerce_var_to_ident fresh env sigma v =
let fail () = raise (CannotCoerceTo "a fresh identifier") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> id
+ | { CAst.v=IntroNaming (IntroIdentifier id)} -> id
| _ -> fail ()
else if has_type v (topwit wit_var) then
out_gen (topwit wit_var) v
@@ -171,7 +171,7 @@ let id_of_name = function
let fail () = raise (CannotCoerceTo "an identifier") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> id
+ | {CAst.v=IntroNaming (IntroIdentifier id)} -> id
| _ -> fail ()
else if has_type v (topwit wit_var) then
out_gen (topwit wit_var) v
@@ -207,7 +207,7 @@ let id_of_name = function
let coerce_to_intro_pattern env sigma v =
if has_type v (topwit wit_intro_pattern) then
- snd (out_gen (topwit wit_intro_pattern) v)
+ (out_gen (topwit wit_intro_pattern) v).CAst.v
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
IntroNaming (IntroIdentifier id)
@@ -226,7 +226,7 @@ let coerce_to_intro_pattern_naming env sigma v =
let coerce_to_hint_base v =
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
+ | {CAst.v=IntroNaming (IntroIdentifier id)} -> Id.to_string id
| _ -> raise (CannotCoerceTo "a hint base name")
else raise (CannotCoerceTo "a hint base name")
@@ -239,7 +239,7 @@ let coerce_to_constr env v =
let fail () = raise (CannotCoerceTo "a term") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) ->
+ | {CAst.v=IntroNaming (IntroIdentifier id)} ->
(try ([], constr_of_id env id) with Not_found -> fail ())
| _ -> fail ()
else if has_type v (topwit wit_constr) then
@@ -268,7 +268,7 @@ let coerce_to_evaluable_ref env sigma v =
let ev =
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
+ | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> EvalVarRef id
| _ -> fail ()
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
@@ -300,14 +300,14 @@ let coerce_to_intro_pattern_list ?loc env sigma v =
match Value.to_list v with
| None -> raise (CannotCoerceTo "an intro pattern list")
| Some l ->
- let map v = Loc.tag ?loc @@ coerce_to_intro_pattern env sigma v in
+ let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in
List.map map l
let coerce_to_hyp env sigma v =
let fail () = raise (CannotCoerceTo "a variable") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
+ | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> id
| _ -> fail ()
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
@@ -340,7 +340,7 @@ let coerce_to_quantified_hypothesis sigma v =
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
match v with
- | _, IntroNaming (IntroIdentifier id) -> NamedHyp id
+ | {CAst.v=IntroNaming (IntroIdentifier id)} -> NamedHyp id
| _ -> raise (CannotCoerceTo "a quantified hypothesis")
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 566fc28733..e510b9f591 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -450,11 +450,10 @@ let register_ltac local tacl =
let () = if is_shadowed then warn_unusable_identifier id in
NewTac id, body
| Tacexpr.TacticRedefinition (ident, body) ->
- let loc = loc_of_reference ident in
let kn =
- try Tacenv.locate_tactic (snd (qualid_of_reference ident))
+ try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v
with Not_found ->
- CErrors.user_err ?loc
+ CErrors.user_err ?loc:ident.CAst.loc
(str "There is no Ltac named " ++ pr_reference ident ++ str ".")
in
UpdateTac kn, body
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
new file mode 100644
index 0000000000..8b0c44041f
--- /dev/null
+++ b/plugins/ltac/tacexpr.ml
@@ -0,0 +1,397 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Loc
+open Names
+open Constrexpr
+open Libnames
+open Genredexpr
+open Genarg
+open Pattern
+open Misctypes
+open Locus
+
+type ltac_constant = KerName.t
+
+type direction_flag = bool (* true = Left-to-right false = right-to-right *)
+type lazy_flag =
+ | General (* returns all possible successes *)
+ | Select (* returns all successes of the first matching branch *)
+ | Once (* returns the first success in a maching branch
+ (not necessarily the first) *)
+type global_flag = (* [gfail] or [fail] *)
+ | TacGlobal
+ | TacLocal
+type evars_flag = bool (* true = pose evars false = fail on evars *)
+type rec_flag = bool (* true = recursive false = not recursive *)
+type advanced_flag = bool (* true = advanced false = basic *)
+type letin_flag = bool (* true = use local def false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type goal_selector = Vernacexpr.goal_selector =
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of lident
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
+
+type inversion_kind = Misctypes.inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
+type ('c,'d,'id) inversion_strength =
+ | NonDepInversion of
+ inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
+ | DepInversion of
+ inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
+ | InversionUsing of 'c * 'id list
+
+type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
+
+type 'id message_token =
+ | MsgString of string
+ | MsgInt of int
+ | MsgIdent of 'id
+
+type ('dconstr,'id) induction_clause =
+ 'dconstr with_bindings destruction_arg *
+ (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+ * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
+ * 'id clause_expr option (* in ... *)
+
+type ('constr,'dconstr,'id) induction_clause_list =
+ ('dconstr,'id) induction_clause list
+ * 'constr with_bindings option (* using ... *)
+
+type 'a with_bindings_arg = clear_flag * 'a with_bindings
+
+(* Type of patterns *)
+type 'a match_pattern =
+ | Term of 'a
+ | Subterm of Id.t option * 'a
+
+(* Type of hypotheses for a Match Context rule *)
+type 'a match_context_hyps =
+ | Hyp of lname * 'a match_pattern
+ | Def of lname * 'a match_pattern * 'a match_pattern
+
+(* Type of a Match rule for Match Context and Match *)
+type ('a,'t) match_rule =
+ | Pat of 'a match_context_hyps list * 'a match_pattern * 't
+ | All of 't
+
+(** Extension indentifiers for the TACTIC EXTEND mechanism. *)
+type ml_tactic_name = {
+ (** Name of the plugin where the tactic is defined, typically coming from a
+ DECLARE PLUGIN statement in the source. *)
+ mltac_plugin : string;
+ (** Name of the tactic entry where the tactic is defined, typically found
+ after the TACTIC EXTEND statement in the source. *)
+ mltac_tactic : string;
+}
+
+type ml_tactic_entry = {
+ mltac_name : ml_tactic_name;
+ mltac_index : int;
+}
+
+(** Composite types *)
+
+type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+
+type open_constr_expr = unit * constr_expr
+type open_glob_constr = unit * glob_constr_and_expr
+
+type binding_bound_vars = Constr_matching.binding_bound_vars
+type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
+
+type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
+
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
+
+type delayed_open_constr = EConstr.constr delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
+type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
+type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+
+(** Generic expressions for atomic tactics *)
+
+type 'a gen_atomic_tactic_expr =
+ (* Basic tactics *)
+ | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
+ | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+ | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
+ | TacCase of evars_flag * 'trm with_bindings_arg
+ | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
+ | TacMutualCofix of Id.t * (Id.t * 'trm) list
+ | TacAssert of
+ evars_flag * bool * 'tacexpr option option *
+ 'dtrm intro_pattern_expr CAst.t option * 'trm
+ | TacGeneralize of ('trm with_occurrences * Name.t) list
+ | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
+ intro_pattern_naming_expr CAst.t option
+
+ (* Derived basic tactics *)
+ | TacInductionDestruct of
+ rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
+
+ (* Conversion *)
+ | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
+ | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+
+ (* Equality and inversion *)
+ | TacRewrite of evars_flag *
+ (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+ (* spiwack: using ['dtrm] here is a small hack, may not be
+ stable by a change in the representation of delayed
+ terms. Because, in fact, it is the whole "with_bindings"
+ which is delayed. But because the "t" level for ['dtrm] is
+ uninterpreted, it works fine here too, and avoid more
+ disruption of this file. *)
+ 'tacexpr option
+ | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis
+
+constraint 'a = <
+ term:'trm;
+ dterm: 'dtrm;
+ pattern:'pat;
+ constant:'cst;
+ reference:'ref;
+ name:'nam;
+ tacexpr:'tacexpr;
+ level:'lev
+>
+
+(** Possible arguments of a tactic definition *)
+
+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
+ | TacFreshId of string or_var list
+ | Tacexp of 'tacexpr
+ | TacPretype of 'trm
+ | TacNumgoals
+
+constraint 'a = <
+ term:'trm;
+ dterm: 'dtrm;
+ pattern:'pat;
+ constant:'cst;
+ reference:'ref;
+ name:'nam;
+ tacexpr:'tacexpr;
+ level:'lev
+>
+
+(** Generic ltac expressions.
+ 't : terms, 'p : patterns, 'c : constants, 'i : inductive,
+ 'r : ltac refs, 'n : idents, 'l : levels *)
+
+and 'a gen_tactic_expr =
+ | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
+ | TacThen of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacDispatch of
+ 'a gen_tactic_expr list
+ | TacExtendTac of
+ 'a gen_tactic_expr array *
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr array
+ | TacThens of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr list
+ | TacThens3parts of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr array *
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr array
+ | TacFirst of 'a gen_tactic_expr list
+ | TacComplete of 'a gen_tactic_expr
+ | TacSolve of 'a gen_tactic_expr list
+ | TacTry of 'a gen_tactic_expr
+ | TacOr of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacOnce of
+ 'a gen_tactic_expr
+ | TacExactlyOnce of
+ 'a gen_tactic_expr
+ | TacIfThenCatch of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacOrelse of
+ 'a gen_tactic_expr *
+ 'a gen_tactic_expr
+ | TacDo of int or_var * 'a gen_tactic_expr
+ | TacTimeout of int or_var * 'a gen_tactic_expr
+ | TacTime of string option * 'a gen_tactic_expr
+ | TacRepeat of 'a gen_tactic_expr
+ | TacProgress of 'a gen_tactic_expr
+ | TacShowHyps of 'a gen_tactic_expr
+ | TacAbstract of
+ 'a gen_tactic_expr * Id.t option
+ | TacId of 'n message_token list
+ | TacFail of global_flag * int or_var * 'n message_token list
+ | TacInfo of 'a gen_tactic_expr
+ | TacLetIn of rec_flag *
+ (lname * 'a gen_tactic_arg) list *
+ 'a gen_tactic_expr
+ | TacMatch of lazy_flag *
+ 'a gen_tactic_expr *
+ ('p,'a gen_tactic_expr) match_rule list
+ | 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
+ | TacSelect of goal_selector * 'a gen_tactic_expr
+ (* For ML extensions *)
+ | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
+ (* For syntax extensions *)
+ | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
+
+constraint 'a = <
+ term:'t;
+ dterm: 'dtrm;
+ pattern:'p;
+ constant:'c;
+ reference:'r;
+ name:'n;
+ tacexpr:'tacexpr;
+ level:'l
+>
+
+and 'a gen_tactic_fun_ast =
+ Name.t list * 'a gen_tactic_expr
+
+constraint 'a = <
+ term:'t;
+ dterm: 'dtrm;
+ pattern:'p;
+ constant:'c;
+ reference:'r;
+ name:'n;
+ tacexpr:'te;
+ level:'l
+>
+
+(** Globalized tactics *)
+
+type g_trm = glob_constr_and_expr
+type g_pat = glob_constr_pattern_and_expr
+type g_cst = evaluable_global_reference and_short_name or_var
+type g_ref = ltac_constant located or_var
+type g_nam = lident
+
+type g_dispatch = <
+ term:g_trm;
+ dterm:g_trm;
+ pattern:g_pat;
+ constant:g_cst;
+ reference:g_ref;
+ name:g_nam;
+ tacexpr:glob_tactic_expr;
+ level:glevel
+>
+
+and glob_tactic_expr =
+ g_dispatch gen_tactic_expr
+
+type glob_atomic_tactic_expr =
+ g_dispatch gen_atomic_tactic_expr
+
+type glob_tactic_arg =
+ g_dispatch gen_tactic_arg
+
+(** Raw tactics *)
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = reference or_by_notation
+type r_ref = reference
+type r_nam = lident
+type r_lev = rlevel
+
+type r_dispatch = <
+ term:r_trm;
+ dterm:r_trm;
+ pattern:r_pat;
+ constant:r_cst;
+ reference:r_ref;
+ name:r_nam;
+ tacexpr:raw_tactic_expr;
+ level:rlevel
+>
+
+and raw_tactic_expr =
+ r_dispatch gen_tactic_expr
+
+type raw_atomic_tactic_expr =
+ r_dispatch gen_atomic_tactic_expr
+
+type raw_tactic_arg =
+ r_dispatch gen_tactic_arg
+
+(** Interpreted tactics *)
+
+type t_trm = EConstr.constr
+type t_pat = constr_pattern
+type t_cst = evaluable_global_reference
+type t_ref = ltac_constant located
+type t_nam = Id.t
+
+type t_dispatch = <
+ term:t_trm;
+ dterm:g_trm;
+ pattern:t_pat;
+ constant:t_cst;
+ reference:t_ref;
+ name:t_nam;
+ tacexpr:unit;
+ level:tlevel
+>
+
+type atomic_tactic_expr =
+ t_dispatch gen_atomic_tactic_expr
+
+(** Misc *)
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
+
+(** Traces *)
+
+type ltac_call_kind =
+ | LtacMLCall of glob_tactic_expr
+ | LtacNotationCall of KerName.t
+ | LtacNameCall of ltac_constant
+ | LtacAtomCall of glob_atomic_tactic_expr
+ | LtacVarCall of Id.t * glob_tactic_expr
+ | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
+
+type ltac_trace = ltac_call_kind Loc.located list
+
+type tacdef_body =
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 6db808dd66..8b0c44041f 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -56,9 +56,9 @@ type inversion_kind = Misctypes.inversion_kind =
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
- inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option
+ inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
| DepInversion of
- inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option
+ inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
| InversionUsing of 'c * 'id list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -70,8 +70,8 @@ type 'id message_token =
type ('dconstr,'id) induction_clause =
'dconstr with_bindings destruction_arg *
- (intro_pattern_naming_expr located option (* eqn:... *)
- * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *)
+ (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+ * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
* 'id clause_expr option (* in ... *)
type ('constr,'dconstr,'id) induction_clause_list =
@@ -126,28 +126,28 @@ type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_op
type delayed_open_constr = EConstr.constr delayed_open
-type intro_pattern = delayed_open_constr intro_pattern_expr located
-type intro_patterns = delayed_open_constr intro_pattern_expr located list
-type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
-type intro_pattern_naming = intro_pattern_naming_expr located
+type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
+type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
+type intro_pattern_naming = intro_pattern_naming_expr CAst.t
(** Generic expressions for atomic tactics *)
type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
- | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr located list
+ | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- ('nam * 'dtrm intro_pattern_expr located option) option
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) option
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
| TacMutualCofix of Id.t * (Id.t * 'trm) list
| TacAssert of
evars_flag * bool * 'tacexpr option option *
- 'dtrm intro_pattern_expr located option * 'trm
+ 'dtrm intro_pattern_expr CAst.t option * 'trm
| TacGeneralize of ('trm with_occurrences * Name.t) list
| TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
- intro_pattern_naming_expr located option
+ intro_pattern_naming_expr CAst.t option
(* Derived basic tactics *)
| TacInductionDestruct of
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 121075f728..9ad9e1520e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -92,36 +92,36 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n)
let intern_string_or_var = intern_or_var (fun (s : string) -> s)
let intern_global_reference ist = function
- | Ident (loc,id) when find_var id ist ->
- ArgVar CAst.(make ?loc id)
+ | {CAst.loc;v=Ident id} when find_var id ist ->
+ ArgVar (make ?loc id)
| r ->
- let loc,_ as lqid = qualid_of_reference r in
- try ArgArg (loc,locate_global_with_alias lqid)
- with Not_found -> error_global_not_found (snd lqid)
+ let {CAst.loc} as lqid = qualid_of_reference r in
+ try ArgArg (loc,locate_global_with_alias lqid)
+ with Not_found -> error_global_not_found lqid
let intern_ltac_variable ist = function
- | Ident (loc,id) ->
+ | {loc;v=Ident id} ->
if find_var id ist then
(* A local variable of any type *)
- ArgVar CAst.(make ?loc id)
+ ArgVar (make ?loc id)
else raise Not_found
| _ ->
raise Not_found
let intern_constr_reference strict ist = function
- | Ident (_,id) as r when not strict && find_hyp id ist ->
- (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
- | Ident (_,id) as r when find_var id ist ->
- (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
+ | {v=Ident id} as r when not strict && find_hyp id ist ->
+ (DAst.make @@ GVar id), Some (make @@ CRef (r,None))
+ | {v=Ident id} as r when find_var id ist ->
+ (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None))
| r ->
- let loc,_ as lqid = qualid_of_reference r in
+ let {loc} as lqid = qualid_of_reference r in
DAst.make @@ GRef (locate_global_with_alias lqid,None),
- if strict then None else Some (CAst.make @@ CRef (r,None))
+ if strict then None else Some (make @@ CRef (r,None))
(* Internalize an isolated reference in position of tactic *)
let intern_isolated_global_tactic_reference r =
- let (loc,qid) = qualid_of_reference r in
+ let {loc;v=qid} = qualid_of_reference r in
TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
let intern_isolated_tactic_reference strict ist r =
@@ -135,12 +135,12 @@ let intern_isolated_tactic_reference strict ist r =
try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
with Not_found ->
(* Reference not found *)
- error_global_not_found (snd (qualid_of_reference r))
+ error_global_not_found (qualid_of_reference r)
(* Internalize an applied tactic reference *)
let intern_applied_global_tactic_reference r =
- let (loc,qid) = qualid_of_reference r in
+ let {loc;v=qid} = qualid_of_reference r in
ArgArg (loc,Tacenv.locate_tactic qid)
let intern_applied_tactic_reference ist r =
@@ -151,7 +151,7 @@ let intern_applied_tactic_reference ist r =
try intern_applied_global_tactic_reference r
with Not_found ->
(* Reference not found *)
- error_global_not_found (snd (qualid_of_reference r))
+ error_global_not_found (qualid_of_reference r)
(* Intern a reference parsed in a non-tactic entry *)
@@ -167,12 +167,12 @@ let intern_non_tactic_reference strict ist r =
with Not_found ->
(* By convention, use IntroIdentifier for unbound ident, when not in a def *)
match r with
- | Ident (loc,id) when not strict ->
- let ipat = in_gen (glbwit wit_intro_pattern) (loc, IntroNaming (IntroIdentifier id)) in
+ | {loc;v=Ident id} when not strict ->
+ let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in
TacGeneric ipat
| _ ->
(* Reference not found *)
- error_global_not_found (snd (qualid_of_reference r))
+ error_global_not_found (qualid_of_reference r)
let intern_message_token ist = function
| (MsgString _ | MsgInt _ as x) -> x
@@ -209,8 +209,8 @@ let intern_constr = intern_constr_gen false false
let intern_type = intern_constr_gen false true
(* Globalize bindings *)
-let intern_binding ist (loc,(b,c)) =
- (loc,(intern_binding_name ist b,intern_constr ist c))
+let intern_binding ist = map (fun (b,c) ->
+ intern_binding_name ist b,intern_constr ist c)
let intern_bindings ist = function
| NoBindings -> NoBindings
@@ -223,12 +223,12 @@ let intern_constr_with_bindings ist (c,bl) =
let intern_constr_with_bindings_arg ist (clear,c) =
(clear,intern_constr_with_bindings ist c)
-let rec intern_intro_pattern lf ist = function
- | loc, IntroNaming pat ->
- loc, IntroNaming (intern_intro_pattern_naming lf ist pat)
- | loc, IntroAction pat ->
- loc, IntroAction (intern_intro_pattern_action lf ist pat)
- | loc, IntroForthcoming _ as x -> x
+let rec intern_intro_pattern lf ist = map (function
+ | IntroNaming pat ->
+ IntroNaming (intern_intro_pattern_naming lf ist pat)
+ | IntroAction pat ->
+ IntroAction (intern_intro_pattern_action lf ist pat)
+ | IntroForthcoming _ as x -> x)
and intern_intro_pattern_naming lf ist = function
| IntroIdentifier id ->
@@ -239,12 +239,12 @@ and intern_intro_pattern_naming lf ist = function
and intern_intro_pattern_action lf ist = function
| IntroOrAndPattern l ->
- IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
+ IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
| IntroInjection l ->
- IntroInjection (List.map (intern_intro_pattern lf ist) l)
+ IntroInjection (List.map (intern_intro_pattern lf ist) l)
| IntroWildcard | IntroRewrite _ as x -> x
- | IntroApplyOn ((loc,c),pat) ->
- IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat)
+ | IntroApplyOn ({loc;v=c},pat) ->
+ IntroApplyOn (make ?loc @@ intern_constr ist c, intern_intro_pattern lf ist pat)
and intern_or_and_intro_pattern lf ist = function
| IntroAndPattern l ->
@@ -256,10 +256,10 @@ let intern_or_and_intro_pattern_loc lf ist = function
| ArgVar {v=id} as x ->
if find_var id ist then x
else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
- | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
+ | ArgArg ll -> ArgArg (map (fun l -> intern_or_and_intro_pattern lf ist l) ll)
-let intern_intro_pattern_naming_loc lf ist (loc,pat) =
- (loc,intern_intro_pattern_naming lf ist pat)
+let intern_intro_pattern_naming_loc lf ist = map (fun pat ->
+ intern_intro_pattern_naming lf ist pat)
(* TODO: catch ltac vars *)
let intern_destruction_arg ist = function
@@ -268,15 +268,15 @@ let intern_destruction_arg ist = function
| clear,ElimOnIdent {loc;v=id} ->
if !strict_check then
(* If in a defined tactic, no intros-until *)
- let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in
+ let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in
match DAst.get c with
- | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id)
+ | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id)
| _ -> clear,ElimOnConstr ((c, p), NoBindings)
else
- clear,ElimOnIdent CAst.(make ?loc id)
+ clear,ElimOnIdent (make ?loc id)
let short_name = function
- | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id)
+ | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id)
| _ -> None
let intern_evaluable_global_reference ist r =
@@ -284,21 +284,21 @@ let intern_evaluable_global_reference ist r =
try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid)
with Not_found ->
match r with
- | Ident (loc,id) when not !strict_check -> EvalVarRef id
- | _ -> error_global_not_found (snd lqid)
+ | {loc;v=Ident id} when not !strict_check -> EvalVarRef id
+ | _ -> error_global_not_found lqid
let intern_evaluable_reference_or_by_notation ist = function
- | AN r -> intern_evaluable_global_reference ist r
- | ByNotation (loc,(ntn,sc)) ->
+ | {v=AN r} -> intern_evaluable_global_reference ist r
+ | {v=ByNotation (ntn,sc);loc} ->
evaluable_of_global_reference ist.genv
(Notation.interp_notation_as_global_reference ?loc
(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
(* Globalize a reduction expression *)
let intern_evaluable ist = function
- | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id)
- | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist ->
- ArgArg (EvalVarRef id, Some CAst.(make ?loc id))
+ | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id)
+ | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist ->
+ ArgArg (EvalVarRef id, Some (make ?loc id))
| r ->
let e = intern_evaluable_reference_or_by_notation ist r in
let na = short_name r in
@@ -353,10 +353,9 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
ref or a pattern seems interesting, with "head" reduction
in case of an evaluable ref, and "strong" reduction in the
subterm matched when a pattern *)
- let loc = loc_of_smart_reference r in
let r = match r with
- | AN r -> r
- | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
+ | {v=AN r} -> r
+ | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in
let sign = {
Constrintern.ltac_vars = ist.ltacvars;
ltac_bound = Id.Set.empty;
@@ -376,7 +375,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
| Inl r -> interp_ref r
| Inr { v = CAppExpl((None,r,None),[]) } ->
(* We interpret similarly @ref and ref *)
- interp_ref (AN r)
+ interp_ref (make @@ AN r)
| Inr c ->
Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c)))
@@ -385,13 +384,13 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let dump_glob_red_expr = function
| Unfold occs -> List.iter (fun (_, r) ->
try
- Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
+ Dumpglob.add_glob ?loc:r.loc
(Smartlocate.smart_global r)
with e when CErrors.noncritical e -> ()) occs
| Cbv grf | Lazy grf ->
List.iter (fun r ->
try
- Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
+ Dumpglob.add_glob ?loc:r.loc
(Smartlocate.smart_global r)
with e when CErrors.noncritical e -> ()) grf.rConst
| _ -> ()
@@ -817,7 +816,7 @@ let notation_subst bindings tac =
let fold id c accu =
let loc = Glob_ops.loc_of_glob_constr (fst c) in
let c = ConstrMayEval (ConstrTerm c) in
- (CAst.make ?loc @@ Name id, c) :: accu
+ (make ?loc @@ Name id, c) :: accu
in
let bindings = Id.Map.fold fold bindings [] in
(** This is theoretically not correct due to potential variable capture, but
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 991afe9c60..6a4bf577b1 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -247,7 +247,7 @@ let coerce_to_tactic loc id v =
| _ -> fail ()
else fail ()
-let intro_pattern_of_ident id = (Loc.tag @@ IntroNaming (IntroIdentifier id))
+let intro_pattern_of_ident id = make @@ IntroNaming (IntroIdentifier id)
let value_of_ident id =
in_gen (topwit wit_intro_pattern) (intro_pattern_of_ident id)
@@ -360,7 +360,7 @@ let interp_reference ist env sigma = function
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
- with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
+ with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -376,14 +376,14 @@ let interp_evaluable ist env sigma = function
with Not_found ->
match r with
| EvalConstRef _ -> r
- | _ -> error_global_not_found ?loc (qualid_of_ident id)
+ | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id)
end
| ArgArg (r,None) -> r
| ArgVar {loc;v=id} ->
try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try try_interp_evaluable env (loc, id)
- with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
+ with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -423,7 +423,7 @@ let extract_ltac_constr_values ist env =
could barely be defined as a feature... *)
(* Extract the identifier list from lfun: join all branches (what to do else?)*)
-let rec intropattern_ids accu (loc,pat) = match pat with
+let rec intropattern_ids accu {loc;v=pat} = match pat with
| IntroNaming (IntroIdentifier id) -> Id.Set.add id accu
| IntroAction (IntroOrAndPattern (IntroAndPattern l)) ->
List.fold_left intropattern_ids accu l
@@ -431,7 +431,7 @@ let rec intropattern_ids accu (loc,pat) = match pat with
List.fold_left intropattern_ids accu (List.flatten ll)
| IntroAction (IntroInjection l) ->
List.fold_left intropattern_ids accu l
- | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat
+ | IntroAction (IntroApplyOn ({v=c},pat)) -> intropattern_ids accu pat
| IntroNaming (IntroAnonymous | IntroFresh _)
| IntroAction (IntroWildcard | IntroRewrite _)
| IntroForthcoming _ -> accu
@@ -439,9 +439,9 @@ let rec intropattern_ids accu (loc,pat) = match pat with
let extract_ids ids lfun accu =
let fold id v accu =
if has_type v (topwit wit_intro_pattern) then
- let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
+ let {v=ipat} = out_gen (topwit wit_intro_pattern) v in
if Id.List.mem id ids then accu
- else intropattern_ids accu (Loc.tag ipat)
+ else intropattern_ids accu (make ipat)
else accu
in
Id.Map.fold fold lfun accu
@@ -642,7 +642,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
- error_global_not_found ?loc (qualid_of_ident id))
+ error_global_not_found (make ?loc @@ qualid_of_ident id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (interp_typed_pattern ist env sigma c) in
interp_occurrences ist occs, p
@@ -762,15 +762,15 @@ let interp_message ist l =
Ftactic.List.map (interp_message_token ist) l >>= fun l ->
Ftactic.return (prlist_with_sep spc (fun x -> x) l)
-let rec interp_intro_pattern ist env sigma = function
- | loc, IntroAction pat ->
- let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in
- sigma, (loc, IntroAction pat)
- | loc, IntroNaming (IntroIdentifier id) ->
- sigma, (loc, interp_intro_pattern_var loc ist env sigma id)
- | loc, IntroNaming pat ->
- sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env sigma pat))
- | loc, IntroForthcoming _ as x -> sigma, x
+let rec interp_intro_pattern ist env sigma = with_loc_val (fun ?loc -> function
+ | IntroAction pat ->
+ let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in
+ sigma, make ?loc @@ IntroAction pat
+ | IntroNaming (IntroIdentifier id) ->
+ sigma, make ?loc @@ interp_intro_pattern_var loc ist env sigma id
+ | IntroNaming pat ->
+ sigma, make ?loc @@ IntroNaming (interp_intro_pattern_naming loc ist env sigma pat)
+ | IntroForthcoming _ as x -> sigma, make ?loc x)
and interp_intro_pattern_naming loc ist env sigma = function
| IntroFresh id -> IntroFresh (interp_ident ist env sigma id)
@@ -784,10 +784,10 @@ and interp_intro_pattern_action ist env sigma = function
| IntroInjection l ->
let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
sigma, IntroInjection l
- | IntroApplyOn ((loc,c),ipat) ->
+ | IntroApplyOn ({loc;v=c},ipat) ->
let c env sigma = interp_open_constr ist env sigma c in
let sigma,ipat = interp_intro_pattern ist env sigma ipat in
- sigma, IntroApplyOn ((loc,c),ipat)
+ sigma, IntroApplyOn (make ?loc c,ipat)
| IntroWildcard | IntroRewrite _ as x -> sigma, x
and interp_or_and_intro_pattern ist env sigma = function
@@ -799,7 +799,7 @@ and interp_or_and_intro_pattern ist env sigma = function
sigma, IntroOrPattern ll
and interp_intro_pattern_list_as_list ist env sigma = function
- | [loc,IntroNaming (IntroIdentifier id)] as l ->
+ | [{loc;v=IntroNaming (IntroIdentifier id)}] as l ->
(try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
List.fold_left_map (interp_intro_pattern ist env) sigma l)
@@ -807,18 +807,18 @@ and interp_intro_pattern_list_as_list ist env sigma = function
let interp_intro_pattern_naming_option ist env sigma = function
| None -> None
- | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env sigma pat)
+ | Some lpat -> Some (map_with_loc (fun ?loc pat -> interp_intro_pattern_naming loc ist env sigma pat) lpat)
let interp_or_and_intro_pattern_option ist env sigma = function
| None -> sigma, None
| Some (ArgVar {loc;v=id}) ->
(match interp_intro_pattern_var loc ist env sigma id with
- | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
+ | IntroAction (IntroOrAndPattern l) -> sigma, Some (make ?loc l)
| _ ->
user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
- | Some (ArgArg (loc,l)) ->
+ | Some (ArgArg {loc;v=l}) ->
let sigma,l = interp_or_and_intro_pattern ist env sigma l in
- sigma, Some (loc,l)
+ sigma, Some (make ?loc l)
let interp_intro_pattern_option ist env sigma = function
| None -> sigma, None
@@ -846,9 +846,9 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
(coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
with Not_found -> NamedHyp id
-let interp_binding ist env sigma (loc,(b,c)) =
+let interp_binding ist env sigma {loc;v=(b,c)} =
let sigma, c = interp_open_constr ist env sigma c in
- sigma, (loc,(interp_binding_name ist env sigma b,c))
+ sigma, (make ?loc (interp_binding_name ist env sigma b,c))
let interp_bindings ist env sigma = function
| NoBindings ->
@@ -873,7 +873,7 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
let loc_of_bindings = function
| NoBindings -> None
| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
-| ExplicitBindings l -> fst (List.last l)
+| ExplicitBindings l -> (List.last l).loc
let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
let loc1 = loc_of_glob_constr c in
@@ -896,7 +896,7 @@ let interp_destruction_arg ist gl arg =
in
let try_cast_id id' =
if Tactics.is_quantified_hypothesis id' gl
- then keep,ElimOnIdent CAst.(make ?loc id')
+ then keep,ElimOnIdent (make ?loc id')
else
(keep, ElimOnConstr begin fun env sigma ->
try (sigma, (constr_of_id env id', NoBindings))
@@ -911,7 +911,7 @@ let interp_destruction_arg ist gl arg =
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
match v with
- | _, IntroNaming (IntroIdentifier id) -> try_cast_id id
+ | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id
| _ -> error ()
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
@@ -924,9 +924,9 @@ let interp_destruction_arg ist gl arg =
with Not_found ->
(* We were in non strict (interactive) mode *)
if Tactics.is_quantified_hypothesis id gl then
- keep,ElimOnIdent CAst.(make ?loc id)
+ keep,ElimOnIdent (make ?loc id)
else
- let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
+ let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in
let f env sigma =
let (sigma,c) = interp_open_constr ist env sigma c in
(sigma, (c,NoBindings))
@@ -1221,7 +1221,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
| TacFreshId l ->
Ftactic.enter begin fun gl ->
let id = interp_fresh_id ist (pf_env gl) (project gl) l in
- Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id)))
+ Ftactic.return (in_gen (topwit wit_intro_pattern) (make @@ IntroNaming (IntroIdentifier id)))
end
| TacPretype c ->
Ftactic.enter begin fun gl ->
@@ -1576,7 +1576,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let sigma = project gl in
let l = List.map (fun (k,c) ->
let loc, f = interp_open_constr_with_bindings_loc ist c in
- (k,(loc,f))) cb
+ (k,(make ?loc f))) cb
in
let sigma,tac = match cl with
| None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
@@ -1677,7 +1677,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let flags = open_constr_use_classes_flags () in
let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
let let_tac b na c cl eqpat =
- let id = Option.default (Loc.tag IntroAnonymous) eqpat in
+ let id = Option.default (make IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
Tactics.letin_tac with_eq na c None cl
in
@@ -1689,7 +1689,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
else
(* We try to keep the pattern structure as much as possible *)
let let_pat_tac b na c cl eqpat =
- let id = Option.default (Loc.tag IntroAnonymous) eqpat in
+ let id = Option.default (make IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
Tactics.letin_pat_tac ev with_eq na c cl
in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 927139c1af..a1d8b087e8 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -33,8 +33,9 @@ let subst_glob_constr_and_expr subst (c, e) =
let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
-let subst_binding subst (loc,(b,c)) =
- (loc,(subst_quantified_hypothesis subst b,subst_glob_constr subst c))
+let subst_binding subst =
+ CAst.map (fun (b,c) ->
+ subst_quantified_hypothesis subst b,subst_glob_constr subst c)
let subst_bindings subst = function
| NoBindings -> NoBindings
@@ -47,13 +48,13 @@ let subst_glob_with_bindings subst (c,bl) =
let subst_glob_with_bindings_arg subst (clear,c) =
(clear,subst_glob_with_bindings subst c)
-let rec subst_intro_pattern subst = function
- | loc,IntroAction p -> loc, IntroAction (subst_intro_pattern_action subst p)
- | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x
+let rec subst_intro_pattern subst = CAst.map (function
+ | IntroAction p -> IntroAction (subst_intro_pattern_action subst p)
+ | IntroNaming _ | IntroForthcoming _ as x -> x)
-and subst_intro_pattern_action subst = function
- | IntroApplyOn ((loc,t),pat) ->
- IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat)
+and subst_intro_pattern_action subst = let open CAst in function
+ | IntroApplyOn ({loc;v=t},pat) ->
+ IntroApplyOn (make ?loc @@ subst_glob_constr subst t,subst_intro_pattern subst pat)
| IntroOrAndPattern l ->
IntroOrAndPattern (subst_intro_or_and_pattern subst l)
| IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 05:26:50 +0000