aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-25 11:16:35 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-25 11:16:35 +0200
commitf2fec63025d933f56dabf114a51720b1aae626c1 (patch)
tree7f729302601fef48e6c59534a7904c7dfb92df2d /plugins/ltac
parent28f8da9489463b166391416de86420c15976522f (diff)
parent94e783390ef9ad9d26a54add2287e0a3e58d1b70 (diff)
Merge PR#402: Uniform attribute handling in interfaces
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.ml45
-rw-r--r--plugins/ltac/evar_tactics.ml2
-rw-r--r--plugins/ltac/extraargs.ml46
-rw-r--r--plugins/ltac/extratactics.ml422
-rw-r--r--plugins/ltac/g_ltac.ml430
-rw-r--r--plugins/ltac/g_obligations.ml42
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/g_tactic.ml4154
-rw-r--r--plugins/ltac/pptactic.ml68
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/rewrite.ml49
-rw-r--r--plugins/ltac/taccoerce.ml4
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacentries.ml32
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--plugins/ltac/tacexpr.mli11
-rw-r--r--plugins/ltac/tacintern.ml64
-rw-r--r--plugins/ltac/tacinterp.ml88
-rw-r--r--plugins/ltac/tacinterp.mli2
-rw-r--r--plugins/ltac/tacsubst.ml22
-rw-r--r--plugins/ltac/tactic_debug.ml24
-rw-r--r--plugins/ltac/tactic_debug.mli2
-rw-r--r--plugins/ltac/tauto.ml11
24 files changed, 300 insertions, 310 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 28ff6df83..6890b3198 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -305,10 +305,9 @@ END
open Tacexpr
let initial_atomic () =
- let dloc = Loc.ghost in
let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
let iter (s, t) =
- let body = TacAtom (dloc, t) in
+ let body = TacAtom (Loc.tag t) in
Tacenv.register_ltac false false (Id.of_string s) body
in
let () = List.iter iter
@@ -323,7 +322,7 @@ let initial_atomic () =
List.iter iter
[ "idtac",TacId [];
"fail", TacFail(TacLocal,ArgArg 0,[]);
- "fresh", TacArg(dloc,TacFreshId [])
+ "fresh", TacArg(Loc.tag @@ TacFreshId [])
]
let () = Mltop.declare_cache_obj initial_atomic "coretactics"
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index bc9c300e2..470a93f2b 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -81,7 +81,7 @@ let instantiate_tac_by_name id c =
end
let let_evar name typ =
- let src = (Loc.ghost,Evar_kinds.GoalEvar) in
+ let src = (Loc.tag Evar_kinds.GoalEvar) in
Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index ec3a49df4..a3310c2d8 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -228,11 +228,11 @@ ARGUMENT EXTEND hloc
| [ "in" "|-" "*" ] ->
[ ConclLocation () ]
| [ "in" ident(id) ] ->
- [ HypLocation ((Loc.ghost,id),InHyp) ]
+ [ HypLocation ((Loc.tag id),InHyp) ]
| [ "in" "(" "Type" "of" ident(id) ")" ] ->
- [ HypLocation ((Loc.ghost,id),InHypTypeOnly) ]
+ [ HypLocation ((Loc.tag id),InHypTypeOnly) ]
| [ "in" "(" "Value" "of" ident(id) ")" ] ->
- [ HypLocation ((Loc.ghost,id),InHypValueOnly) ]
+ [ HypLocation ((Loc.tag id),InHypValueOnly) ]
END
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index bd48614db..cbd8a7f0f 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -73,7 +73,7 @@ END
let induction_arg_of_quantified_hyp = function
| AnonHyp n -> None,ElimOnAnonHyp n
- | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id)
+ | NamedHyp id -> None,ElimOnIdent (Loc.tag id)
(* Versions *_main must come first!! so that "1" is interpreted as a
ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
@@ -264,7 +264,7 @@ let add_rewrite_hint bases ort t lcsr =
(Declare.declare_universe_context false ctx;
Univ.ContextSet.empty)
in
- Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in
+ Loc.tag ?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
@@ -628,15 +628,15 @@ let subst_var_with_hole occ tid t =
let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
let locref = ref 0 in
let rec substrec = function
- | GVar (_,id) as x ->
+ | { CAst.v = GVar id } as x ->
if Id.equal id tid
then
(decr occref;
if Int.equal !occref 0 then x
else
(incr locref;
- GHole (Loc.make_loc (!locref,0),
- Evar_kinds.QuestionMark(Evar_kinds.Define true),
+ CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
Misctypes.IntroAnonymous, None)))
else x
| c -> map_glob_constr_left_to_right substrec c in
@@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t =
let locref = ref 0 in
let occref = ref occ in
let rec substrec = function
- | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) ->
+ | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
decr occref;
if Int.equal !occref 0 then tc
else
(incr locref;
- GHole (Loc.make_loc (!locref,0),
- Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
+ CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
| c -> map_glob_constr_left_to_right substrec c
in
substrec t
@@ -676,8 +676,8 @@ let hResolve id c occ t =
with
| Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
let (e, info) = CErrors.push e in
- let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in
- resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
+ let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in
+ resolve_hole (subst_hole_with_term loc_begin c_raw t_hole)
in
let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
let t_constr = EConstr.of_constr t_constr in
@@ -781,7 +781,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.ghost, TacInductionDestruct(false, false, cl)) in
+ let dest = TacAtom (Loc.tag @@ 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.ml4 b/plugins/ltac/g_ltac.ml4
index d717ed0a5..b5028190f 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -41,7 +41,7 @@ let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
let reference_to_id = function
| Libnames.Ident (loc, id) -> (loc, id)
| Libnames.Qualid (loc,_) ->
- CErrors.user_err ~loc
+ CErrors.user_err ?loc
(str "This expression should be a simple identifier.")
let tactic_mode = Gram.entry_create "vernac:tactic_command"
@@ -159,9 +159,9 @@ GEXTEND 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,a)
+ | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a)
| r = reference; la = LIST0 tactic_arg_compat ->
- TacArg(!@loc,TacCall (!@loc,r,la)) ]
+ TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ]
| "0"
[ "("; a = tactic_expr; ")" -> a
| "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
@@ -169,7 +169,7 @@ GEXTEND Gram
| Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
| None -> TacDispatch tf
end
- | a = tactic_atom -> TacArg (!@loc,a) ] ]
+ | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ]
;
failkw:
[ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ]
@@ -187,7 +187,7 @@ GEXTEND Gram
(* Tactic arguments to the right of an application *)
tactic_arg_compat:
[ [ a = tactic_arg -> a
- | c = Constr.constr -> (match c with CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
+ | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c))
(* Unambiguous entries: tolerated w/o "ltac:" modifier *)
| "()" -> TacGeneric (genarg_of_unit ()) ] ]
;
@@ -203,7 +203,7 @@ 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 (!@loc,id) ] ]
+ | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ]
;
constr_eval:
[ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -219,7 +219,7 @@ GEXTEND Gram
;
tactic_atom:
[ [ n = integer -> TacGeneric (genarg_of_int n)
- | r = reference -> TacCall (!@loc,r,[])
+ | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[]))
| "()" -> TacGeneric (genarg_of_unit ()) ] ]
;
match_key:
@@ -255,10 +255,10 @@ GEXTEND Gram
let t, ty =
match mpv with
| Term t -> (match t with
- | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
+ | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty)
| _ -> mpv, None)
| _ -> mpv, None
- in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty)
+ in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty)
] ]
;
match_context_rule:
@@ -353,7 +353,7 @@ GEXTEND Gram
operconstr: LEVEL "0"
[ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
- CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
+ CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ]
;
END
@@ -460,9 +460,9 @@ END
let pr_ltac_production_item = function
| Tacentries.TacTerm s -> quote (str s)
-| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg
-| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false
-| Tacentries.TacNonTerm (_, (arg, sep), Some id) ->
+| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg
+| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false
+| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) ->
let sep = match sep with
| None -> mt ()
| Some sep -> str "," ++ spc () ++ quote (str sep)
@@ -472,9 +472,9 @@ let pr_ltac_production_item = function
VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
| [ string(s) ] -> [ Tacentries.TacTerm s ]
| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
- [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ]
+ [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ]
| [ ident(nt) ] ->
- [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ]
+ [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ]
END
VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 3e6e2db60..7d4075836 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -50,7 +50,7 @@ module Tactic = Pltac
open Pcoq
-let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+let sigref = mkRefC (Qualid (Loc.tag @@ 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_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index ac979bcf8..5adf8475a 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -124,7 +124,7 @@ END
let clsubstitute o c =
Proofview.Goal.enter { enter = begin fun gl ->
- let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
+ let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in
let hyps = Tacmach.New.pf_ids_of_hyps gl in
Tacticals.New.tclMAP
(fun cl ->
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index e33c25cf8..257100b01 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -119,14 +119,14 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
(try List.index Names.Name.equal (snd x) ids
with Not_found -> error "No such fix variable.")
| _ -> error "Cannot guess decreasing argument of fix." in
- (id,n,CProdN(loc,bl,ty))
+ (id,n, CAst.make ~loc @@ CProdN(bl,ty))
let mk_cofix_tac (loc,id,bl,ann,ty) =
let _ = Option.map (fun (aloc,_) ->
user_err ~loc:aloc
~hdr:"Constr:mk_cofix_tac"
(Pp.str"Annotation forbidden in cofix expression.")) ann in
- (id,CProdN(loc,bl,ty))
+ (id,CAst.make ~loc @@ CProdN(bl,ty))
(* Functions overloaded by quotifier *)
let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
@@ -143,32 +143,32 @@ let mkTacCase with_evar = function
(* Reinterpret numbers as a notation for terms *)
| [(clear,ElimOnAnonHyp n),(None,None),None],None ->
TacCase (with_evar,
- (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
+ (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)),
NoBindings)))
(* 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 ->
- TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings)))
+ TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings)))
| ic ->
if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
then
error "Use of numbers as direct arguments of 'case' is not supported.";
TacInductionDestruct (false,with_evar,ic)
-let rec mkCLambdaN_simple_loc loc bll c =
+let rec mkCLambdaN_simple_loc ?loc bll c =
match bll with
| ((loc1,_)::_ as idl,bk,t) :: bll ->
- CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
- | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
+ CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
+ | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
| [] -> c
let mkCLambdaN_simple bl c = match bl with
| [] -> c
| h :: _ ->
- let loc = Loc.merge (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
- mkCLambdaN_simple_loc loc bl c
+ let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
+ mkCLambdaN_simple_loc ?loc bl c
-let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (List.last l))
+let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
let map_int_or_var f = function
| ArgArg x -> ArgArg (f x)
@@ -290,7 +290,7 @@ GEXTEND Gram
(* (A & B & C) is translated into (A,(B,C)) *)
let rec pairify = function
| ([]|[_]|[_;_]) as l -> l
- | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+ | t::q -> [t; Loc.tag ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
in IntroAndPattern (pairify (si::tc)) ] ]
;
equality_intropattern:
@@ -305,8 +305,8 @@ GEXTEND Gram
;
nonsimple_intropattern:
[ [ l = simple_intropattern -> l
- | "*" -> !@loc, IntroForthcoming true
- | "**" -> !@loc, IntroForthcoming false ]]
+ | "*" -> Loc.tag ~loc:!@loc @@ IntroForthcoming true
+ | "**" -> Loc.tag ~loc:!@loc @@ IntroForthcoming false ]]
;
simple_intropattern:
[ [ pat = simple_intropattern_closed;
@@ -314,19 +314,19 @@ GEXTEND Gram
let loc0,pat = pat in
let f c pat =
let loc1 = Constrexpr_ops.constr_loc c in
- let loc = Loc.merge loc0 loc1 in
+ let loc = Loc.merge_opt loc0 loc1 in
IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in
- !@loc, List.fold_right f l pat ] ]
+ Loc.tag ~loc:!@loc @@ List.fold_right f l pat ] ]
;
simple_intropattern_closed:
- [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
- | pat = equality_intropattern -> !@loc, IntroAction pat
- | "_" -> !@loc, IntroAction IntroWildcard
- | pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
+ [ [ 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 ] ]
;
simple_binding:
- [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c)
- | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ]
+ [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c)
+ | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ]
;
bindings:
[ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
@@ -429,7 +429,7 @@ GEXTEND Gram
| -> true ]]
;
simple_binder:
- [ [ na=name -> ([na],Default Explicit,CHole (!@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
+ [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
| "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
] ]
;
@@ -457,7 +457,7 @@ GEXTEND Gram
| -> None ] ]
;
or_and_intropattern_loc:
- [ [ ipat = or_and_intropattern -> ArgArg (!@loc,ipat)
+ [ [ ipat = or_and_intropattern -> ArgArg (Loc.tag ~loc:!@loc ipat)
| locid = identref -> ArgVar locid ] ]
;
as_or_and_ipat:
@@ -465,13 +465,13 @@ GEXTEND Gram
| -> None ] ]
;
eqn_ipat:
- [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
+ [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (Loc.tag ~loc:!@loc pat)
| IDENT "_eqn"; ":"; pat = naming_intropattern ->
let loc = !@loc in
- warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat)
+ warn_deprecated_eqn_syntax ~loc "H"; Some (Loc.tag ~loc pat)
| IDENT "_eqn" ->
let loc = !@loc in
- warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous)
+ warn_deprecated_eqn_syntax ~loc "?"; Some (Loc.tag ~loc IntroAnonymous)
| -> None ] ]
;
as_name:
@@ -510,145 +510,145 @@ GEXTEND Gram
[ [
(* Basic tactics *)
IDENT "intros"; pl = ne_intropatterns ->
- TacAtom (!@loc, TacIntroPattern (false,pl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl))
| IDENT "intros" ->
- TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false]))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[Loc.tag ~loc:!@loc @@IntroForthcoming false]))
| IDENT "eintros"; pl = ne_intropatterns ->
- TacAtom (!@loc, TacIntroPattern (true,pl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl))
| IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
+ inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,false,cl,inhyp))
| IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,true,cl,inhyp))
+ inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,true,cl,inhyp))
| IDENT "simple"; IDENT "apply";
cl = LIST1 constr_with_bindings_arg SEP ",";
- inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,false,cl,inhyp))
+ inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,false,cl,inhyp))
| IDENT "simple"; IDENT "eapply";
cl = LIST1 constr_with_bindings_arg SEP",";
- inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,true,cl,inhyp))
+ inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,true,cl,inhyp))
| IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- TacAtom (!@loc, TacElim (false,cl,el))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacElim (false,cl,el))
| IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
- TacAtom (!@loc, TacElim (true,cl,el))
- | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl)
- | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
+ TacAtom (Loc.tag ~loc:!@loc @@ TacElim (true,cl,el))
+ | IDENT "case"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase false icl)
+ | IDENT "ecase"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase true icl)
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
- TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd))
| "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
- TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
| IDENT "pose"; (id,b) = bindings_with_parameters ->
- TacAtom (!@loc, TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
| IDENT "pose"; b = constr; na = as_name ->
- TacAtom (!@loc, TacLetTac (na,b,Locusops.nowhere,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None))
| IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacAtom (!@loc, TacLetTac (Names.Name id,c,p,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None))
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
- TacAtom (!@loc, TacLetTac (na,c,p,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None))
| IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
p = clause_dft_all ->
- TacAtom (!@loc, TacLetTac (na,c,p,false,e))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e))
(* Alternative syntax for "pose proof c as id" *)
| IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
c = lconstr; ")" ->
- TacAtom (!@loc, TacAssert (true,None,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "assert c as id by tac" *)
| IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (!@loc, TacAssert (true,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "enough c as id by tac" *)
| IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (!@loc, TacAssert (false,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
| IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (!@loc, TacAssert (true,Some tac,ipat,c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c))
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- TacAtom (!@loc, TacAssert (true,None,ipat,c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c))
| IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (!@loc, TacAssert (false,Some tac,ipat,c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c))
| IDENT "generalize"; c = constr ->
- TacAtom (!@loc, TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
+ TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
| IDENT "generalize"; c = constr; l = LIST1 constr ->
let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
- TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l)))
+ TacAtom (Loc.tag ~loc:!@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, TacGeneralize (((nl,c),na)::l))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (((nl,c),na)::l))
(* Derived basic tactics *)
| IDENT "induction"; ic = induction_clause_list ->
- TacAtom (!@loc, TacInductionDestruct (true,false,ic))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct (true,false,ic))
| IDENT "einduction"; ic = induction_clause_list ->
- TacAtom (!@loc, TacInductionDestruct(true,true,ic))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(true,true,ic))
| IDENT "destruct"; icl = induction_clause_list ->
- TacAtom (!@loc, TacInductionDestruct(false,false,icl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl))
| IDENT "edestruct"; icl = induction_clause_list ->
- TacAtom (!@loc, TacInductionDestruct(false,true,icl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,true,icl))
(* Equality and inversion *)
| IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
+ cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (false,l,cl,t))
| IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
- cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
+ cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@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, TacInversion (DepInversion (k,co,ids),hyp))
+ TacAtom (Loc.tag ~loc:!@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, TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
| IDENT "inversion";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (!@loc, TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
| IDENT "inversion_clear";
hyp = quantified_hypothesis; ids = as_or_and_ipat;
cl = in_hyp_list ->
- TacAtom (!@loc, TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
| IDENT "inversion"; hyp = quantified_hypothesis;
"using"; c = constr; cl = in_hyp_list ->
- TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (InversionUsing (c,cl), hyp))
(* Conversion *)
| IDENT "red"; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Red false, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Red false, cl))
| IDENT "hnf"; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Hnf, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Hnf, cl))
| IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Simpl (all_with d, po), cl))
| IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Cbv s, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv s, cl))
| IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Cbn s, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbn s, cl))
| IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Lazy s, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Lazy s, cl))
| IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv (all_with delta), cl))
| IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (CbvVm po, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvVm po, cl))
| IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (CbvNative po, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvNative po, cl))
| IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Unfold ul, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Unfold ul, cl))
| IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Fold l, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Fold l, cl))
| IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
- TacAtom (!@loc, TacReduce (Pattern pl, cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Pattern pl, cl))
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
| IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
let p,cl = merge_occurrences (!@loc) cl oc in
- TacAtom (!@loc, TacChange (p,c,cl))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacChange (p,c,cl))
] ]
;
END;;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a61957559..75ab1c5ee 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t option
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
@@ -149,7 +149,7 @@ type 'a extra_genarg_printer =
let pr_or_by_notation f = 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
@@ -162,8 +162,8 @@ type 'a extra_genarg_printer =
| NamedHyp id -> pr_id id
let pr_binding prc = function
- | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+ | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
let pr_bindings prc prlc = function
| ImplicitBindings l ->
@@ -212,7 +212,7 @@ type 'a extra_genarg_printer =
let rec tacarg_using_rule_token pr_gen = function
| [] -> []
| TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l
- | TacNonTerm (_, (symb, arg), _) :: l ->
+ | TacNonTerm (_, ((symb, arg), _)) :: l ->
pr_gen symb arg :: tacarg_using_rule_token pr_gen l
let pr_tacarg_using_rule pr_gen l =
@@ -252,7 +252,7 @@ type 'a extra_genarg_printer =
let prods = (KNmap.find key !prnotation_tab).pptac_prods in
let pr = function
| TacTerm s -> primitive s
- | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
+ | TacNonTerm (_, (symb, _)) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
in
pr_sequence pr prods
with Not_found ->
@@ -264,9 +264,9 @@ type 'a extra_genarg_printer =
let rec pack prods args = match prods, args with
| [], [] -> []
| TacTerm s :: prods, args -> TacTerm s :: pack prods args
- | TacNonTerm (_, _, None) :: prods, args -> pack prods args
- | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args ->
- TacNonTerm (loc, (symb, arg), ido) :: pack prods args
+ | TacNonTerm (_, (_, None)) :: prods, args -> pack prods args
+ | TacNonTerm (loc, (symb, (Some _ as ido))) :: prods, arg :: args ->
+ TacNonTerm (loc, ((symb, arg), ido)) :: pack prods args
| _ -> raise Not_found
in
let prods = pack pp.pptac_prods l in
@@ -276,7 +276,7 @@ type 'a extra_genarg_printer =
let pr arg = str "_" in
KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
- let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
+ let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg))
let is_genarg tag wit =
let ArgT.Any tag = tag in
@@ -332,17 +332,17 @@ type 'a extra_genarg_printer =
pr_extend_gen (pr_farg prtac)
let pr_raw_alias prc prlc prtac prpat lev key args =
- pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
let pr_glob_alias prc prlc prtac prpat lev key args =
- pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
(**********************************************************************)
(* The tactic printer *)
let strip_prod_binders_expr n ty =
let rec strip_ty acc n ty =
- match ty with
- Constrexpr.CProdN(_,bll,a) ->
+ match ty.CAst.v with
+ Constrexpr.CProdN(bll,a) ->
let nb =
List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
let bll = List.map (fun (x, _, y) -> x, y) bll in
@@ -353,7 +353,7 @@ type 'a extra_genarg_printer =
let pr_ltac_or_var pr = function
| ArgArg x -> pr x
- | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
+ | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id)
let pr_ltac_constant kn =
if !Flags.in_debugger then pr_kn kn
@@ -369,8 +369,8 @@ type 'a extra_genarg_printer =
let pr_esubst prc l =
let pr_qhyp = function
- (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
- | (_,NamedHyp id,c) ->
+ (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
+ | (_,(NamedHyp id,c)) ->
str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
in
prlist_with_sep spc pr_qhyp l
@@ -417,7 +417,7 @@ type 'a extra_genarg_printer =
let pr_as_name = function
| Anonymous -> mt ()
- | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.ghost,id)
+ | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id)
let pr_pose_as_style prc na c =
spc() ++ prc c ++ pr_as_name na
@@ -508,7 +508,7 @@ type 'a extra_genarg_printer =
let pr_core_destruction_arg prc prlc = function
| ElimOnConstr c -> pr_with_bindings prc prlc c
- | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
+ | ElimOnIdent (loc,id) -> pr_with_comments ?loc (pr_id id)
| ElimOnAnonHyp n -> int n
let pr_destruction_arg prc prlc (clear_flag,h) =
@@ -575,7 +575,7 @@ type 'a extra_genarg_printer =
let pr_let_clause k pr (id,(bl,t)) =
hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
- str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t)))
+ str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t)))
let pr_let_clauses recflag pr = function
| hd::tl ->
@@ -1038,7 +1038,7 @@ type 'a extra_genarg_printer =
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
| TacAtom (loc,t) ->
- pr_with_comments loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
+ pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
| TacArg(_,Tacexp e) ->
pr.pr_tactic (latom,E) e, latom
| TacArg(_,ConstrMayEval (ConstrTerm c)) ->
@@ -1049,19 +1049,19 @@ type 'a extra_genarg_printer =
primitive "fresh" ++ pr_fresh_ids l, latom
| TacArg(_,TacGeneric arg) ->
pr.pr_generic arg, latom
- | TacArg(_,TacCall(loc,f,[])) ->
+ | TacArg(_,TacCall(loc,(f,[]))) ->
pr.pr_reference f, latom
- | TacArg(_,TacCall(loc,f,l)) ->
- pr_with_comments loc (hov 1 (
+ | TacArg(_,TacCall(loc,(f,l))) ->
+ pr_with_comments ?loc (hov 1 (
pr.pr_reference f ++ spc ()
++ prlist_with_sep spc pr_tacarg l)),
lcall
| TacArg (_,a) ->
pr_tacarg a, latom
- | TacML (loc,s,l) ->
- pr_with_comments loc (pr.pr_extend 1 s l), lcall
- | TacAlias (loc,kn,l) ->
- pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
+ | TacML (loc,(s,l)) ->
+ pr_with_comments ?loc (pr.pr_extend 1 s l), lcall
+ | TacAlias (loc,(kn,l)) ->
+ pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom
)
in
if prec_less prec inherited then strm
@@ -1079,16 +1079,16 @@ type 'a extra_genarg_printer =
| TacNumgoals ->
keyword "numgoals"
| (TacCall _|Tacexp _ | TacGeneric _) as a ->
- hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))))
+ hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.tag a))))
in pr_tac
let strip_prod_binders_glob_constr n (ty,_) =
let rec strip_ty acc n ty =
if Int.equal n 0 then (List.rev acc, (ty,None)) else
- match ty with
- Glob_term.GProd(loc,na,Explicit,a,b) ->
- strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
+ match ty.CAst.v with
+ Glob_term.GProd(na,Explicit,a,b) ->
+ strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
| _ -> error "Cannot translate fix tactic: not enough products" in
strip_ty [] n ty
@@ -1159,7 +1159,7 @@ type 'a extra_genarg_printer =
if n=0 then (List.rev acc, EConstr.of_constr ty) else
match Term.kind_of_term ty with
Term.Prod(na,a,b) ->
- strip_ty (([Loc.ghost,na],EConstr.of_constr a)::acc) (n-1) b
+ strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
| _ -> error "Cannot translate fix tactic: not enough products" in
strip_ty [] n ty
@@ -1254,7 +1254,7 @@ let () =
wit_clause_dft_concl
(pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) pr_lident)
- (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
+ (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)))
;
Genprint.register_print0
wit_constr
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 433f342c4..19bdf2d49 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -21,7 +21,7 @@ open Ppextend
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t option
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index a853576f2..c5dbc8a14 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -129,7 +129,7 @@ let to_ltacprof_results xml =
let feedback_results results =
Feedback.(feedback
- (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results)))
+ (Custom (None, "ltacprof_results", of_ltacprof_results results)))
(* ************** pretty printing ************************************* *)
@@ -249,7 +249,7 @@ let string_of_call ck =
| Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
| Tacexpr.LtacAtomCall te ->
(Pptactic.pr_glob_tactic (Global.env ())
- (Tacexpr.TacAtom (Loc.ghost, te)))
+ (Tacexpr.TacAtom (Loc.tag 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 5630a2d7b..e8c9f4eba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1786,34 +1786,34 @@ let rec strategy_of_ast = function
(* By default the strategy for "rewrite_db" is top-down *)
-let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
let declare_an_instance n s args =
- (((Loc.ghost,Name n),None), Explicit,
- CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None),
+ (((Loc.tag @@ Name n),None), Explicit,
+ CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None),
args))
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
new_instance (Flags.is_universe_polymorphism ())
- binders instance (Some (true, CRecord (Loc.ghost,fields)))
+ binders instance (Some (true, CAst.make @@ CRecord (fields)))
~global ~generalize:false ~refine:false Hints.empty_hint_info
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.ghost,Id.of_string "reflexivity"),lemma)]
+ [(Ident (Loc.tag @@ 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.ghost,Id.of_string "symmetry"),lemma)]
+ [(Ident (Loc.tag @@ 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.ghost,Id.of_string "transitivity"),lemma)]
+ [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)]
let declare_relation ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
@@ -1837,16 +1837,16 @@ let declare_relation ?(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.ghost,Id.of_string "PreOrder_Reflexive"), lemma1);
- (Ident (Loc.ghost,Id.of_string "PreOrder_Transitive"),lemma3)])
+ [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1);
+ (Ident (Loc.tag @@ 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.ghost,Id.of_string "PER_Symmetric"), lemma2);
- (Ident (Loc.ghost,Id.of_string "PER_Transitive"),lemma3)])
+ [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2);
+ (Ident (Loc.tag @@ 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
@@ -1854,11 +1854,11 @@ let declare_relation ?(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.ghost,Id.of_string "Equivalence_Reflexive"), lemma1);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
+ [(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)])
-let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None)
+let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
let proper_projection sigma r ty =
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
@@ -1958,17 +1958,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.ghost,Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+ [(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])])
let make_tactic name =
let open Tacexpr in
- let loc = Loc.ghost in
let tacpath = Libnames.qualid_of_string name in
- let tacname = Qualid (loc, tacpath) in
- TacArg (loc, TacCall (loc, tacname, []))
+ let tacname = Qualid (Loc.tag tacpath) in
+ TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, [])))
let add_morphism_infer glob m n =
init_setoid ();
@@ -2011,14 +2010,14 @@ let add_morphism glob binders m s n =
let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
let instance =
- (((Loc.ghost,Name instance_id),None), Explicit,
- CAppExpl (Loc.ghost,
- (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
+ (((Loc.tag @@ Name instance_id),None), Explicit,
+ CAst.make @@ CAppExpl (
+ (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
ignore(new_instance ~global:glob poly binders instance
- (Some (true, CRecord (Loc.ghost,[])))
+ (Some (true, CAst.make @@ CRecord []))
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index b76009c99..e037bb4b2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -268,11 +268,11 @@ let coerce_to_constr_list env v =
List.map map l
| None -> raise (CannotCoerceTo "a term list")
-let coerce_to_intro_pattern_list loc env sigma v =
+let coerce_to_intro_pattern_list ?loc env sigma v =
match Value.to_list v with
| None -> raise (CannotCoerceTo "an intro pattern list")
| Some l ->
- let map v = (loc, coerce_to_intro_pattern env sigma v) in
+ let map v = Loc.tag ?loc @@ coerce_to_intro_pattern env sigma v in
List.map map l
let coerce_to_hyp env sigma v =
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 4a44f86d9..9883c03c4 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -75,7 +75,7 @@ val coerce_to_evaluable_ref :
val coerce_to_constr_list : Environ.env -> Value.t -> constr list
val coerce_to_intro_pattern_list :
- Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
+ ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 91262f6fd..4d7b0f929 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -21,7 +21,7 @@ open Nameops
type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t option
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
type raw_argument = string * string option
type argument = Genarg.ArgT.any Extend.user_symbol
@@ -166,7 +166,7 @@ let add_tactic_entry (kn, ml, tg) state =
TacGeneric arg
in
let l = List.map map l in
- (TacAlias (loc,kn,l):raw_tactic_expr)
+ (TacAlias (Loc.tag ~loc (kn,l)):raw_tactic_expr)
in
let () =
if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
@@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
in
let map = function
| TacTerm s -> GramTerminal s
- | TacNonTerm (loc, s, ido) ->
+ | TacNonTerm (loc, (s, ido)) ->
let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
- GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e)
+ GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e))
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
@@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry =
let interp_prod_item = function
| TacTerm s -> TacTerm s
- | TacNonTerm (loc, (nt, sep), ido) ->
+ | TacNonTerm (loc, ((nt, sep), ido)) ->
let symbol = parse_user_entry nt sep in
let interp s = function
| None ->
@@ -220,7 +220,7 @@ let interp_prod_item = function
end
in
let symbol = interp_entry_name interp symbol in
- TacNonTerm (loc, symbol, ido)
+ TacNonTerm (loc, (symbol, ido))
let make_fresh_key =
let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
let cons_production_parameter = function
| TacTerm _ -> None
-| TacNonTerm (_, _, ido) -> ido
+| TacNonTerm (_, (_, ido)) -> ido
let add_glob_tactic_notation local ~level prods forml ids tac =
let parule = {
@@ -334,10 +334,10 @@ let extend_atomic_tactic name entries =
in
let empty_value = function
| TacTerm s -> raise NonEmptyArgument
- | TacNonTerm (_, symb, _) ->
+ | TacNonTerm (_, (symb, _)) ->
let EntryName (typ, e) = prod_item_of_symbol 0 symb in
let Genarg.Rawwit wit = typ in
- let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in
+ let inj x = TacArg (Loc.tag @@ TacGeneric (Genarg.in_gen typ x)) in
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
@@ -351,7 +351,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.ghost, entry, args) in
+ let body = TacML (Loc.tag (entry, args)) in
Tacenv.register_ltac false false (Names.Id.of_string id) body
in
List.iteri add_atomic entries
@@ -362,12 +362,12 @@ let add_ml_tactic_notation name ~level prods =
let open Tacexpr in
let get_id = function
| TacTerm s -> None
- | TacNonTerm (_, _, ido) -> ido
+ | TacNonTerm (_, (_, ido)) -> ido
in
let ids = List.map_filter get_id prods in
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
- let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
- let tac = TacML (Loc.ghost, entry, List.map map ids) in
+ let map id = Reference (Misctypes.ArgVar (Loc.tag id)) in
+ let tac = TacML (Loc.tag (entry, List.map map ids)) in
add_glob_tactic_notation false ~level prods true ids tac
in
List.iteri iter (List.rev prods);
@@ -401,7 +401,7 @@ let create_ltac_quotation name cast (e, l) =
entry),
Atoken (CLexer.terminal ")"))
in
- let action _ v _ _ _ loc = cast (loc, v) in
+ let action _ v _ _ _ loc = cast (Some loc, v) in
let gram = (level, assoc, [Rule (rule, action)]) in
Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
@@ -427,7 +427,7 @@ let register_ltac local tacl =
let kn = Lib.make_kn id in
let id_pp = pr_id id in
let () = if is_defined_tac kn then
- CErrors.user_err ~loc
+ CErrors.user_err ?loc
(str "There is already an Ltac named " ++ id_pp ++ str".")
in
let is_shadowed =
@@ -444,7 +444,7 @@ let register_ltac local tacl =
let kn =
try Nametab.locate_tactic (snd (qualid_of_reference ident))
with Not_found ->
- CErrors.user_err ~loc
+ CErrors.user_err ?loc
(str "There is no Ltac named " ++ pr_reference ident ++ str ".")
in
UpdateTac kn, body
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index dac62dad3..07aa7ad82 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t option
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
type raw_argument = string * string option
(** An argument type as provided in Tactic notations, i.e. a string like
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8aefe7605..bf760e7bb 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -184,8 +184,7 @@ type 'a gen_tactic_arg =
| TacGeneric of 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
- | TacCall of Loc.t * 'ref *
- 'a gen_tactic_arg list
+ | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located
| TacFreshId of string or_var list
| Tacexp of 'tacexpr
| TacPretype of 'trm
@@ -207,7 +206,7 @@ constraint 'a = <
'r : ltac refs, 'n : idents, 'l : levels *)
and 'a gen_tactic_expr =
- | TacAtom of Loc.t * 'a gen_atomic_tactic_expr
+ | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
| TacThen of
'a gen_tactic_expr *
'a gen_tactic_expr
@@ -266,9 +265,9 @@ and 'a gen_tactic_expr =
| TacArg of 'a gen_tactic_arg located
| TacSelect of goal_selector * 'a gen_tactic_expr
(* For ML extensions *)
- | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
+ | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
- | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list
+ | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
constraint 'a = <
term:'t;
@@ -389,7 +388,7 @@ type ltac_call_kind =
| LtacVarCall of Id.t * glob_tactic_expr
| LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
-type ltac_trace = (Loc.t * ltac_call_kind) list
+type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
| TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 75227def0..da7f11472 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -31,8 +31,6 @@ open Locus
(** Globalization of tactic expressions :
Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
-let dloc = Loc.ghost
-
let error_tactic_expected ?loc =
user_err ?loc (str "Tactic expected.")
@@ -74,16 +72,16 @@ let intern_name l ist = function
let strict_check = ref false
-let adjust_loc loc = if !strict_check then dloc else loc
+let adjust_loc loc = if !strict_check then None else loc
(* Globalize a name which must be bound -- actually just check it is bound *)
let intern_hyp ist (loc,id as locid) =
if not !strict_check then
locid
else if find_ident id ist then
- (dloc,id)
+ Loc.tag id
else
- Pretype_errors.error_var_not_found ~loc id
+ Pretype_errors.error_var_not_found ?loc id
let intern_or_var f ist = function
| ArgVar locid -> ArgVar (intern_hyp ist locid)
@@ -110,19 +108,19 @@ let intern_ltac_variable ist = function
let intern_constr_reference strict ist = function
| Ident (_,id) as r when not strict && find_hyp id ist ->
- GVar (dloc,id), Some (CRef (r,None))
+ (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
| Ident (_,id) as r when find_var id ist ->
- GVar (dloc,id), if strict then None else Some (CRef (r,None))
+ (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
| r ->
let loc,_ as lqid = qualid_of_reference r in
- GRef (loc,locate_global_with_alias lqid,None),
- if strict then None else Some (CRef (r,None))
+ CAst.make @@ GRef (locate_global_with_alias lqid,None),
+ if strict then None else Some (CAst.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
- TacCall (loc,ArgArg (loc,locate_tactic qid),[])
+ TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[]))
let intern_isolated_tactic_reference strict ist r =
(* An ltac reference *)
@@ -208,8 +206,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 (loc,(b,c)) =
+ (loc,(intern_binding_name ist b,intern_constr ist c))
let intern_bindings ist = function
| NoBindings -> NoBindings
@@ -267,8 +265,8 @@ let intern_destruction_arg ist = function
| clear,ElimOnIdent (loc,id) ->
if !strict_check then
(* If in a defined tactic, no intros-until *)
- match intern_constr ist (CRef (Ident (dloc,id), None)) with
- | GVar (loc,id),_ -> clear,ElimOnIdent (loc,id)
+ match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with
+ | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id)
| c -> clear,ElimOnConstr (c,NoBindings)
else
clear,ElimOnIdent (loc,id)
@@ -287,9 +285,9 @@ let intern_evaluable_global_reference ist r =
let intern_evaluable_reference_or_by_notation ist = function
| AN r -> intern_evaluable_global_reference ist r
- | ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,(ntn,sc)) ->
evaluable_of_global_reference ist.genv
- (Notation.interp_notation_as_global_reference loc
+ (Notation.interp_notation_as_global_reference ?loc
(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
(* Globalize a reduction expression *)
@@ -346,10 +344,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
| _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in
let c = Constrintern.interp_reference sign r in
- match c with
- | GRef (_,r,None) ->
+ match c.CAst.v with
+ | GRef (r,None) ->
Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
- | GVar (_,id) ->
+ | GVar id ->
let r = evaluable_of_global_reference ist.genv (VarRef id) in
Inl (ArgArg (r,None))
| _ ->
@@ -357,7 +355,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
Inr (bound_names,(c,None),dummy_pat) in
(l, match p with
| Inl r -> interp_ref r
- | Inr (CAppExpl(_,(None,r,None),[])) ->
+ | Inr { CAst.v = CAppExpl((None,r,None),[]) } ->
(* We interpret similarly @ref and ref *)
interp_ref (AN r)
| Inr c ->
@@ -368,13 +366,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_of_or_by_notation Libnames.loc_of_reference r)
+ Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
(Smartlocate.smart_global r)
with e when CErrors.noncritical e -> ()) occs
| Cbv grf | Lazy grf ->
List.iter (fun r ->
try
- Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
+ Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
(Smartlocate.smart_global r)
with e when CErrors.noncritical e -> ()) grf.rConst
| _ -> ()
@@ -455,7 +453,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
(* Utilities *)
let extract_let_names lrc =
let fold accu ((loc, name), _) =
- if Id.Set.mem name accu then user_err ~loc
+ if Id.Set.mem name accu then user_err ?loc
~hdr:"glob_tactic" (str "This variable is bound several times.")
else Id.Set.add name accu
in
@@ -546,7 +544,7 @@ and intern_tactic_seq onlytac ist = function
| TacAtom (loc,t) ->
let lf = ref ist.ltacvars in
let t = intern_atomic lf ist t in
- !lf, TacAtom (adjust_loc loc, t)
+ !lf, TacAtom (Loc.tag ?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
@@ -620,12 +618,12 @@ and intern_tactic_seq onlytac ist = function
ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac)
(* For extensions *)
- | TacAlias (loc,s,l) ->
+ | TacAlias (loc,(s,l)) ->
let l = List.map (intern_tacarg !strict_check false ist) l in
- ist.ltacvars, TacAlias (loc,s,l)
- | TacML (loc,opn,l) ->
+ ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
+ | TacML (loc,(opn,l)) ->
let _ignore = Tacenv.interp_ml_tactic opn in
- ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l)
+ ist.ltacvars, TacML (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
@@ -633,7 +631,7 @@ and intern_tactic_as_arg loc onlytac ist a =
| TacGeneric _ as a -> TacArg (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 (loc,a)
and intern_tactic_or_tacarg ist = intern_tactic false ist
@@ -646,11 +644,11 @@ 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,
+ | TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f
+ | TacCall (loc,(f,l)) ->
+ TacCall (Loc.tag ?loc (
intern_applied_tactic_reference ist f,
- List.map (intern_tacarg !strict_check false ist) l)
+ List.map (intern_tacarg !strict_check false ist) l))
| TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x)
| TacPretype c -> TacPretype (intern_constr ist c)
| TacNumgoals -> TacNumgoals
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b8c021f18..f63c38d4f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -200,8 +200,6 @@ end
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
-let dloc = Loc.ghost
-
let catching_error call_trace fail (e, info) =
let inner_trace =
Option.default [] (Exninfo.get info ltac_trace_info)
@@ -314,7 +312,7 @@ let append_trace trace v =
(* Dynamically check that an argument is a tactic *)
let coerce_to_tactic loc id v =
let v = Value.normalize v in
- let fail () = user_err ~loc
+ let fail () = user_err ?loc
(str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
in
let v = Value.normalize v in
@@ -325,7 +323,7 @@ let coerce_to_tactic loc id v =
| _ -> fail ()
else fail ()
-let intro_pattern_of_ident id = (Loc.ghost, IntroNaming (IntroIdentifier id))
+let intro_pattern_of_ident id = (Loc.tag @@ IntroNaming (IntroIdentifier id))
let value_of_ident id =
in_gen (topwit wit_intro_pattern) (intro_pattern_of_ident id)
@@ -369,22 +367,22 @@ let debugging_exception_step ist signal_anomaly e pp =
debugging_step ist (fun () ->
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
-let error_ltac_variable loc id env v s =
- user_err ~loc (str "Ltac variable " ++ pr_id id ++
+let error_ltac_variable ?loc id env v s =
+ user_err ?loc (str "Ltac variable " ++ pr_id id ++
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
strbrk "which cannot be coerced to " ++ str s ++ str".")
(* Raise Not_found if not in interpretation sign *)
let try_interp_ltac_var coerce ist env (loc,id) =
let v = Id.Map.find id ist.lfun in
- try coerce v with CannotCoerceTo s -> error_ltac_variable loc id env v s
+ try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s
let interp_ltac_var coerce ist env locid =
try try_interp_ltac_var coerce ist env locid
with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
let interp_ident ist env sigma id =
- try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (dloc,id)
+ try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id)
with Not_found -> id
(* Interprets an optional identifier, bound or fresh *)
@@ -403,7 +401,7 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
let interp_int ist locid =
try try_interp_ltac_var coerce_to_int ist None locid
with Not_found ->
- user_err ~loc:(fst locid) ~hdr:"interp_int"
+ user_err ?loc:(fst locid) ~hdr:"interp_int"
(str "Unbound variable " ++ pr_id (snd locid) ++ str".")
let interp_int_or_var ist = function
@@ -426,7 +424,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
with Not_found ->
(* Then look if bound in the proof context at calling time *)
if is_variable env id then id
- else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id))
+ else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id))
let interp_hyp_list_as_list ist env sigma (loc,id as x) =
try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
@@ -442,7 +440,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 ?loc (qualid_of_ident id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -458,14 +456,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 ?loc (qualid_of_ident id)
end
| ArgArg (r,None) -> r
| ArgVar (loc, id) ->
try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (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 ?loc (qualid_of_ident id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -524,7 +522,7 @@ let extract_ids ids lfun =
if has_type v (topwit wit_intro_pattern) then
let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
if Id.List.mem id ids then accu
- else accu @ intropattern_ids (dloc, ipat)
+ else accu @ intropattern_ids (Loc.tag ipat)
else accu
in
Id.Map.fold fold lfun []
@@ -534,7 +532,7 @@ let default_fresh_id = Id.of_string "H"
let interp_fresh_id ist env sigma l =
let extract_ident ist env sigma id =
try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
- ist (Some (env,sigma)) (dloc,id)
+ ist (Some (env,sigma)) (Loc.tag id)
with Not_found -> id in
let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
let avoid = match TacStore.get ist.extra f_avoid_ids with
@@ -692,7 +690,7 @@ let interp_typed_pattern ist env sigma (_,c,_) =
let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
let try_expand_ltac_var sigma x =
try match dest_fun x with
- | GVar (_,id), _ ->
+ | { CAst.v = GVar id }, _ ->
let v = Id.Map.find id ist.lfun in
sigma, List.map inj_fun (coerce_to_constr_list env v)
| _ ->
@@ -734,7 +732,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)) (loc,id)
with Not_found ->
- error_global_not_found ~loc (qualid_of_ident id))
+ error_global_not_found ?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
@@ -792,7 +790,7 @@ let interp_may_eval f ist env sigma = function
!evdref , c
with
| Not_found ->
- user_err ~loc ~hdr:"interp_may_eval"
+ user_err ?loc ~hdr:"interp_may_eval"
(str "Unbound context identifier" ++ pr_id s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
@@ -934,7 +932,7 @@ and interp_or_and_intro_pattern ist env sigma = function
and interp_intro_pattern_list_as_list ist env sigma = function
| [loc,IntroNaming (IntroIdentifier id)] as l ->
- (try sigma, coerce_to_intro_pattern_list loc env sigma (Id.Map.find id ist.lfun)
+ (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
List.fold_map (interp_intro_pattern ist env) sigma l)
| l -> List.fold_map (interp_intro_pattern ist env) sigma l
@@ -949,7 +947,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function
(match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with
| IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
| _ ->
- user_err ~loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
+ user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
| Some (ArgArg (loc,l)) ->
let sigma,l = interp_or_and_intro_pattern ist env sigma l in
sigma, Some (loc,l)
@@ -970,19 +968,19 @@ let interp_binding_name ist sigma = function
(* If a name is bound, it has to be a quantified hypothesis *)
(* user has to use other names for variables if these ones clash with *)
(* a name intented to be used as a (non-variable) identifier *)
- try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(dloc,id)
+ try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id)
with Not_found -> NamedHyp id
let interp_declared_or_quantified_hypothesis ist env sigma = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
try try_interp_ltac_var
- (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,id)
+ (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (Loc.tag id)
with Not_found -> NamedHyp id
-let interp_binding ist env sigma (loc,b,c) =
+let interp_binding ist env sigma (loc,(b,c)) =
let sigma, c = interp_open_constr ist env sigma c in
- sigma, (loc,interp_binding_name ist sigma b,c)
+ sigma, (loc,(interp_binding_name ist sigma b,c))
let interp_bindings ist env sigma = function
| NoBindings ->
@@ -1005,14 +1003,14 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
sigma, (c, bl)
let loc_of_bindings = function
-| NoBindings -> Loc.ghost
+| NoBindings -> None
| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
-| ExplicitBindings l -> pi1 (List.last l)
+| ExplicitBindings l -> fst (List.last l)
let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
let loc1 = loc_of_glob_constr c in
let loc2 = loc_of_bindings bl in
- let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in
+ let loc = Loc.merge_opt loc1 loc2 in
let f = { delayed = fun env sigma ->
let sigma = Sigma.to_evar_map sigma in
let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in
@@ -1030,7 +1028,7 @@ let interp_destruction_arg ist gl arg =
}
| keep,ElimOnAnonHyp n as x -> x
| keep,ElimOnIdent (loc,id) ->
- let error () = user_err ~loc
+ let error () = user_err ?loc
(strbrk "Cannot coerce " ++ pr_id id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
@@ -1041,7 +1039,7 @@ let interp_destruction_arg ist gl arg =
(keep, ElimOnConstr { delayed = begin fun env sigma ->
try Sigma.here (constr_of_id env id', NoBindings) sigma
with Not_found ->
- user_err ~loc ~hdr:"interp_destruction_arg" (
+ user_err ?loc ~hdr:"interp_destruction_arg" (
pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
end })
in
@@ -1067,7 +1065,7 @@ let interp_destruction_arg ist gl arg =
if Tactics.is_quantified_hypothesis id gl then
keep,ElimOnIdent (loc,id)
else
- let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in
+ let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
let f = { delayed = fun env sigma ->
let sigma = Sigma.to_evar_map sigma in
let (sigma,c) = interp_open_constr ist env sigma c in
@@ -1250,7 +1248,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,(s,l)) ->
let (ids, body) = Tacenv.interp_alias s in
let (>>=) = Ftactic.bind in
let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
@@ -1281,8 +1279,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
in
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
- | TacML (loc,opn,l) ->
- push_trace (loc,LtacMLCall tac) ist >>= fun trace ->
+ | TacML (loc,(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
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
@@ -1301,7 +1299,7 @@ and force_vrec ist v : Val.t Ftactic.t =
| v -> Ftactic.return (of_tacvalue v)
else Ftactic.return v
-and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
+and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
match r with
| ArgVar (loc,id) ->
let v =
@@ -1315,7 +1313,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
end
| ArgArg (loc,r) ->
let ids = extract_ids [] ist.lfun in
- let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in
+ let loc_info = (Option.default loc loc',LtacNameCall r) in
let extra = TacStore.set ist.extra f_avoid_ids ids in
push_trace loc_info ist >>= fun trace ->
let extra = TacStore.set extra f_trace trace in
@@ -1326,7 +1324,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
| TacGeneric arg -> interp_genarg ist arg
- | Reference r -> interp_ltac_reference dloc false ist r
+ | Reference r -> interp_ltac_reference false ist r
| ConstrMayEval c ->
Ftactic.s_enter { s_enter = begin fun gl ->
let sigma = project gl in
@@ -1334,17 +1332,17 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma)
end }
- | TacCall (loc,r,[]) ->
- interp_ltac_reference loc true ist r
- | TacCall (loc,f,l) ->
+ | TacCall (loc,(r,[])) ->
+ interp_ltac_reference true ist r
+ | TacCall (loc,(f,l)) ->
let (>>=) = Ftactic.bind in
- interp_ltac_reference loc true ist f >>= fun fv ->
+ interp_ltac_reference true ist f >>= fun fv ->
Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs ->
interp_app loc ist fv largs
| TacFreshId l ->
Ftactic.enter { 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) (dloc, IntroNaming (IntroIdentifier id)))
+ Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id)))
end }
| TacPretype c ->
Ftactic.s_enter { s_enter = begin fun gl ->
@@ -1435,7 +1433,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 ((_, id), b) =
- let v = of_tacvalue (VRec (lref, TacArg (dloc, b))) in
+ let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
Id.Map.add id v accu
in
let lfun = List.fold_left fold ist.lfun llc in
@@ -1761,7 +1759,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* We try to fully-typecheck the term *)
let (sigma,c_interp) = interp_constr ist env sigma c in
let let_tac b na c cl eqpat =
- let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+ let id = Option.default (Loc.tag 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
@@ -1773,7 +1771,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.ghost,IntroAnonymous) eqpat in
+ let id = Option.default (Loc.tag IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
Tactics.letin_pat_tac with_eq na c cl
in
@@ -2125,7 +2123,7 @@ let lift_constr_tac_to_ml_tac vars tac =
let c = Id.Map.find id ist.lfun in
try Some (coerce_to_closed_constr env c)
with CannotCoerceTo ty ->
- error_ltac_variable Loc.ghost dummy_id (Some (env,sigma)) c ty
+ error_ltac_variable dummy_id (Some (env,sigma)) c ty
in
let args = List.map_filter map vars in
tac args ist
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 494f36a95..2ec45312e 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -110,7 +110,7 @@ val interp_int : interp_sign -> Id.t Loc.located -> int
val interp_int_or_var : interp_sign -> int or_var -> int
-val error_ltac_variable : Loc.t -> Id.t ->
+val error_ltac_variable : ?loc:Loc.t -> Id.t ->
(Environ.env * Evd.evar_map) option -> value -> string -> 'a
(** Transforms a constr-expecting tactic into a tactic finding its arguments in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index fe3a9f3b2..4390ff08b 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -32,8 +32,8 @@ 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 (loc,(b,c)) =
+ (loc,(subst_quantified_hypothesis subst b,subst_glob_constr subst c))
let subst_bindings subst = function
| NoBindings -> NoBindings
@@ -77,9 +77,7 @@ let subst_or_var f = function
| ArgVar _ as x -> x
| ArgArg x -> ArgArg (f x)
-let dloc = Loc.ghost
-
-let subst_located f (_loc,id) = (dloc,f id)
+let subst_located f = Loc.map f
let subst_reference subst =
subst_or_var (subst_located (subst_kn subst))
@@ -182,7 +180,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 (dloc, subst_atomic subst t)
+ | TacAtom (_loc,t) -> TacAtom (Loc.tag @@ 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
@@ -229,22 +227,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 (dloc,subst_tacarg subst a)
+ | TacArg (_,a) -> TacArg (Loc.tag @@ subst_tacarg subst a)
| TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac)
(* For extensions *)
- | TacAlias (_,s,l) ->
+ | TacAlias (_,(s,l)) ->
let s = subst_kn subst s in
- TacAlias (dloc,s,List.map (subst_tacarg subst) l)
- | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l)
+ TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l))
+ | TacML (loc,(opn,l)) -> TacML (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, subst_reference subst f, List.map (subst_tacarg subst) l)
+ | TacCall (loc,(f,l)) ->
+ TacCall (Loc.tag ?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 dac15ff79..20a2013a5 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -366,7 +366,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.ghost,te)))
+ (Tacexpr.TacAtom (Loc.tag te)))
| Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
quote (Printer.pr_glob_constr_env (Global.env()) c) ++
(if not (Id.Map.is_empty vars) then
@@ -401,16 +401,16 @@ let skip_extensions trace =
| [] -> [] in
List.rev (aux (List.rev trace))
-let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2
+let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2
-let extract_ltac_trace trace eloc =
+let extract_ltac_trace ?loc trace =
let trace = skip_extensions trace in
- let (loc,c),tail = List.sep_last trace in
+ let (tloc,c),tail = List.sep_last trace in
if is_defined_ltac trace then
(* We entered a user-defined tactic,
we display the trace with location of the call *)
- let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
- Some msg, if finer_loc eloc loc then eloc else loc
+ let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in
+ (if finer_loc loc tloc then loc else tloc), Some msg
else
(* We entered a primitive tactic, we don't display trace but
report on the finest location *)
@@ -418,21 +418,21 @@ let extract_ltac_trace trace eloc =
(* trace is with innermost call coming first *)
let rec aux best_loc = function
| (loc,_)::tail ->
- if Loc.is_ghost best_loc ||
- not (Loc.is_ghost loc) && finer_loc loc best_loc
+ if Option.is_empty best_loc ||
+ not (Option.is_empty loc) && finer_loc loc best_loc
then
aux loc tail
else
aux best_loc tail
| [] -> best_loc in
- aux eloc trace in
- None, best_loc
+ aux loc trace in
+ best_loc, None
let get_ltac_trace (_, info) =
let ltac_trace = Exninfo.get info ltac_trace_info in
- let loc = Option.default Loc.ghost (Loc.get_loc info) in
+ let loc = Loc.get_loc info in
match ltac_trace with
| None -> None
- | Some trace -> Some (extract_ltac_trace trace loc)
+ | Some trace -> Some (extract_ltac_trace ?loc trace)
let () = ExplainErr.register_additional_error_info get_ltac_trace
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 0b4d35a22..ac35464c4 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -77,4 +77,4 @@ val db_breakpoint : debug_info ->
Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
val extract_ltac_trace :
- Tacexpr.ltac_trace -> Loc.t -> Pp.std_ppcmds option * Loc.t
+ ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4de2081cf..1e46c253d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -88,7 +88,6 @@ let _ =
(** Base tactics *)
-let loc = Loc.ghost
let idtac = Proofview.tclUNIT ()
let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ()))
@@ -206,7 +205,7 @@ let u_iff = make_unfold "iff"
let u_not = make_unfold "not"
let reduction_not_iff _ ist =
- let make_reduce c = TacAtom (loc, TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
+ let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
let tac = match !negation_unfolding, unfold_iff () with
| true, true -> make_reduce [u_not; u_iff]
| true, false -> make_reduce [u_not]
@@ -259,11 +258,11 @@ let tauto_power_flags = {
}
let with_flags flags _ ist =
- let f = (loc, Id.of_string "f") in
- let x = (loc, Id.of_string "x") in
+ let f = (Loc.tag @@ Id.of_string "f") in
+ let x = (Loc.tag @@ Id.of_string "x") in
let arg = Val.Dyn (tag_tauto_flags, flags) in
let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in
- eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)])))
+ eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)]))))
let register_tauto_tactic tac name0 args =
let ids = List.map (fun id -> Id.of_string id) args in
@@ -271,7 +270,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, entry, [])) in
+ let tac = TacFun (ids, TacML (Loc.tag (entry, []))) in
let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in
Mltop.declare_cache_obj obj tauto_plugin
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-02 11:16:25 +0000