aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml46
-rw-r--r--plugins/ltac/g_ltac.ml414
-rw-r--r--plugins/ltac/g_tactic.ml4140
-rw-r--r--plugins/ltac/pptactic.ml12
-rw-r--r--plugins/ltac/taccoerce.ml4
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacentries.ml9
-rw-r--r--plugins/ltac/tacintern.ml20
-rw-r--r--plugins/ltac/tacinterp.ml36
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--plugins/ltac/tactic_debug.ml7
11 files changed, 126 insertions, 126 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 5123d6c40..dc43930e4 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -267,7 +267,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
@@ -679,8 +679,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 -> 0,0 | Some loc -> Loc.unloc loc in
- resolve_hole (subst_hole_with_term (fst 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
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 23643c5d3..e20beae96 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 ] ]
@@ -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:
@@ -470,7 +470,7 @@ 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), p)) ]
+ [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), p)) ]
END
VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index d1e5c810f..8aaad0566 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -166,20 +166,20 @@ let mkTacCase with_evar = function
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 ->
- Loc.tag ~loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
- | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
+ Loc.tag ?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)
@@ -301,7 +301,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:
@@ -316,8 +316,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;
@@ -325,15 +325,15 @@ 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.tag ~loc:!@loc (NamedHyp id, c)
@@ -468,7 +468,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:
@@ -476,13 +476,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:
@@ -521,145 +521,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 26ac3c53e..bdafbdc78 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -352,7 +352,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
@@ -507,7 +507,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) =
@@ -1037,7 +1037,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)) ->
@@ -1051,16 +1051,16 @@ type 'a extra_genarg_printer =
| TacArg(_,TacCall(loc,(f,[]))) ->
pr.pr_reference f, latom
| TacArg(_,TacCall(loc,(f,l))) ->
- pr_with_comments ~loc (hov 1 (
+ 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
+ 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
+ pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom
)
in
if prec_less prec inherited then strm
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 9c4ac5265..b09672a12 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -76,7 +76,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 f608515aa..a19dbd327 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -170,7 +170,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
@@ -180,6 +180,7 @@ let add_tactic_entry (kn, ml, tg) state =
| TacTerm s -> GramTerminal s
| TacNonTerm (loc, (s, _)) ->
let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
+ let loc = Option.default Loc.internal_ghost loc in
GramNonTerminal (loc, typ, e)
in
let prods = List.map map tg.tacgram_prods in
@@ -405,7 +406,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])
@@ -431,7 +432,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 =
@@ -448,7 +449,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/tacintern.ml b/plugins/ltac/tacintern.ml
index 787a5f50b..44ea3ff1d 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -72,7 +72,7 @@ let intern_name l ist = function
let strict_check = ref false
-let adjust_loc loc = if !strict_check then None else Some 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) =
@@ -81,7 +81,7 @@ let intern_hyp ist (loc,id as locid) =
else if find_ident id ist then
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)
@@ -126,7 +126,7 @@ let intern_move_location ist = function
let intern_isolated_global_tactic_reference r =
let (loc,qid) = qualid_of_reference r in
- TacCall (Loc.tag ~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 *)
@@ -293,7 +293,7 @@ let intern_evaluable_reference_or_by_notation ist = function
| AN r -> intern_evaluable_global_reference ist r
| 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 *)
@@ -372,13 +372,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
| _ -> ()
@@ -459,7 +459,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
@@ -626,7 +626,7 @@ and intern_tactic_seq onlytac ist = function
(* For extensions *)
| TacAlias (loc,(s,l)) ->
let l = List.map (intern_tacarg !strict_check false ist) l in
- ist.ltacvars, TacAlias (Loc.tag ~loc (s,l))
+ ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
| TacML (loc,(opn,l)) ->
let _ignore = Tacenv.interp_ml_tactic opn in
ist.ltacvars, TacML (loc, (opn,List.map (intern_tacarg !strict_check false ist) l))
@@ -637,7 +637,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
@@ -652,7 +652,7 @@ and intern_tacarg strict onlytac ist = function
| ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
| TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f
| TacCall (loc,(f,l)) ->
- TacCall (Loc.tag ~loc (
+ TacCall (Loc.tag ?loc (
intern_applied_tactic_reference ist f,
List.map (intern_tacarg !strict_check false ist) l))
| TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e969b86f6..4d5b84455 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -313,7 +313,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
@@ -376,7 +376,7 @@ let error_ltac_variable ?loc id env v s =
(* 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
@@ -402,7 +402,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
@@ -425,7 +425,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)
@@ -447,7 +447,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
@@ -463,14 +463,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 =
@@ -739,7 +739,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
@@ -797,7 +797,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
@@ -939,7 +939,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
@@ -954,7 +954,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)
@@ -1011,13 +1011,13 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
let loc_of_bindings = function
| NoBindings -> None
-| ImplicitBindings l -> Some (loc_of_glob_constr (fst (List.last l)))
-| ExplicitBindings l -> Some (fst (List.last l))
+| ImplicitBindings l -> loc_of_glob_constr (fst (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 = Loc.opt_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
@@ -1035,7 +1035,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
@@ -1046,7 +1046,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
@@ -1072,7 +1072,7 @@ let interp_destruction_arg ist gl arg =
if Tactics.is_quantified_hypothesis id gl then
keep,ElimOnIdent (loc,id)
else
- let c = (Loc.tag ~loc @@ GVar id,Some (Loc.tag @@ CRef (Ident (loc,id),None))) in
+ let c = (Loc.tag ?loc @@ GVar id,Some (Loc.tag @@ 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
@@ -1287,7 +1287,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
| TacML (loc,(opn,l)) ->
- push_trace (Loc.tag ~loc @@ LtacMLCall tac) ist >>= fun trace ->
+ 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
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 0ee6e8a85..4390ff08b 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -242,7 +242,7 @@ and subst_tacarg subst = function
| Reference r -> Reference (subst_reference subst r)
| ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
| TacCall (loc,(f,l)) ->
- TacCall (Loc.tag ~loc (subst_reference subst f, List.map (subst_tacarg subst) l))
+ TacCall (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 ac8534bdc..f04495c61 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -387,12 +387,11 @@ 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 ?loc trace =
let trace = skip_extensions trace in
let (tloc,c),tail = List.sep_last trace in
- let loc = Option.default tloc loc in
if is_defined_ltac trace then
(* We entered a user-defined tactic,
we display the trace with location of the call *)
@@ -405,8 +404,8 @@ let extract_ltac_trace ?loc trace =
(* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-27 16:27:17 +0000