From 6d9e008ffd81bbe927e3442fb0c37269ed25b21f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Jan 2017 01:27:40 +0100 Subject: [location] Use Loc.located for constr_expr. This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location. --- plugins/ltac/g_ltac.ml4 | 8 ++++---- plugins/ltac/g_tactic.ml4 | 12 ++++++------ plugins/ltac/pptactic.ml | 4 ++-- plugins/ltac/rewrite.ml | 12 ++++++------ plugins/ltac/tacintern.ml | 10 +++++----- plugins/ltac/tacinterp.ml | 2 +- 6 files changed, 24 insertions(+), 24 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ca5d198c23..dffd90be35 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -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 _loc, CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c)) (* Unambiguous entries: tolerated w/o "ltac:" modifier *) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; @@ -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) + | _loc, 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 (Loc.tag @@ 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) ] ] + Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] ; END diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 4b3ca80af5..1674bb4ca2 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -130,14 +130,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, Loc.tag ~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,Loc.tag ~loc @@ CProdN(bl,ty)) (* Functions overloaded by quotifier *) let destruction_arg_of_constr (c,lbind as clbind) = match lbind with @@ -154,12 +154,12 @@ 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,(Loc.tag @@ 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,(Loc.tag @@ CRef (Ident id,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then @@ -169,7 +169,7 @@ let mkTacCase with_evar = function 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) + Loc.tag ~loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c | [] -> c @@ -440,7 +440,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, Loc.tag ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 39ae1f41d2..ad76ef9c65 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -340,8 +340,8 @@ type 'a extra_genarg_printer = let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = - match ty with - Constrexpr.CProdN(_,bll,a) -> + match snd ty 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 diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b84be4600c..1f75f88d42 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1787,18 +1787,18 @@ 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 = Loc.tag @@ CAppExpl ((None,(Libnames.Ident (Loc.ghost,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 @@ CAppExpl ((None, Qualid (Loc.ghost, 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, Loc.tag @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info let declare_instance_refl global binders a aeq n lemma = @@ -1859,7 +1859,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2); (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) +let cHole = Loc.tag @@ 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 @@ -2013,13 +2013,13 @@ let add_morphism glob binders m s n = let instance_id = add_suffix n "_Proper" in let instance = (((Loc.ghost,Name instance_id),None), Explicit, - CAppExpl (Loc.ghost, + Loc.tag @@ CAppExpl ( (None, Qualid (Loc.ghost, 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, Loc.tag @@ CRecord [])) ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 3f83f104e9..75f890c960 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -110,13 +110,13 @@ 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)) + GVar (dloc,id), Some (Loc.tag @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - GVar (dloc,id), if strict then None else Some (CRef (r,None)) + GVar (dloc,id), if strict then None else Some (Loc.tag @@ 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)) + if strict then None else Some (Loc.tag @@ CRef (r,None)) let intern_move_location ist = function | MoveAfter id -> MoveAfter (intern_hyp ist id) @@ -273,7 +273,7 @@ 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 + match intern_constr ist (Loc.tag @@ CRef (Ident (dloc,id), None)) with | GVar (loc,id),_ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else @@ -363,7 +363,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 (_, CAppExpl((None,r,None),[])) -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 50f43931e9..de6c44b2b9 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1074,7 +1074,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 = (GVar (loc,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 -- cgit v1.2.3 From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 14:23:53 +0100 Subject: [location] Switch glob_constr to Loc.located --- plugins/ltac/extratactics.ml4 | 12 ++++++------ plugins/ltac/g_rewrite.ml4 | 2 +- plugins/ltac/pptactic.ml | 4 ++-- plugins/ltac/tacintern.ml | 22 ++++++++++------------ plugins/ltac/tacinterp.ml | 4 ++-- 5 files changed, 21 insertions(+), 23 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 38fdfb7599..232bd851ff 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -631,15 +631,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 -> + | (_, 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), + Loc.tag ~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 @@ -651,13 +651,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) -> + | _, 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)) + Loc.tag ~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 diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c50100bf55..1f40c67b5d 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - 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 (_, GVar id') when Id.equal id' id -> true | _ -> false in Tacticals.onAllHypsAndConcl (fun cl -> match cl with diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index ad76ef9c65..aec2e37fde 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1085,8 +1085,8 @@ type 'a extra_genarg_printer = 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) -> + match Loc.obj ty with + Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 75f890c960..e7d4c1be9f 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,14 +72,14 @@ 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 Loc.ghost 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 @@ -110,12 +108,12 @@ 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 (Loc.tag @@ CRef (r,None)) + (Loc.tag @@ GVar id), Some (Loc.tag @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - GVar (dloc,id), if strict then None else Some (Loc.tag @@ CRef (r,None)) + (Loc.tag @@ GVar id), if strict then None else Some (Loc.tag @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in - GRef (loc,locate_global_with_alias lqid,None), + Loc.tag @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (Loc.tag @@ CRef (r,None)) let intern_move_location ist = function @@ -273,8 +271,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 (Loc.tag @@ CRef (Ident (dloc,id), None)) with - | GVar (loc,id),_ -> clear,ElimOnIdent (loc,id) + match intern_constr ist (Loc.tag @@ CRef (Ident (Loc.tag id), None)) with + | (loc, GVar id), _ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else clear,ElimOnIdent (loc,id) @@ -352,10 +350,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 Loc.obj c 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)) | _ -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index de6c44b2b9..a8d8eda1dd 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -699,7 +699,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), _ -> + | (_, GVar id), _ -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -1074,7 +1074,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 (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 -- cgit v1.2.3 From bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 15:06:26 +0100 Subject: [location] Use located in misctypes. --- plugins/ltac/g_tactic.ml4 | 4 ++-- plugins/ltac/pptactic.ml | 10 +++++----- plugins/ltac/tacintern.ml | 6 +++--- plugins/ltac/tacinterp.ml | 6 +++--- plugins/ltac/tacsubst.ml | 4 ++-- 5 files changed, 15 insertions(+), 15 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 1674bb4ca2..d1e5c810f4 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -336,8 +336,8 @@ GEXTEND Gram | pat = naming_intropattern -> !@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 -> diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index aec2e37fde..0dd6819fdf 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -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 -> @@ -368,8 +368,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 diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index e7d4c1be9f..ad9814b84b 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -212,8 +212,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 @@ -291,7 +291,7 @@ 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 (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a8d8eda1dd..aac63fcb2b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -987,9 +987,9 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,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 -> @@ -1014,7 +1014,7 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = let loc_of_bindings = function | NoBindings -> Loc.ghost | 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 diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fe3a9f3b2a..9582ebd899 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 -- cgit v1.2.3 From 84eb5cd72a015c45337a5a6070c5651f56be6e74 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 15:45:43 +0100 Subject: [location] Use located in tactics. One case missing due the TACTIC EXTEND macro. --- plugins/ltac/g_ltac.ml4 | 4 ++-- plugins/ltac/pptactic.ml | 6 +++--- plugins/ltac/rewrite.ml | 2 +- plugins/ltac/tacentries.ml | 2 +- plugins/ltac/tacexpr.mli | 9 ++++----- plugins/ltac/tacintern.ml | 16 ++++++++-------- plugins/ltac/tacinterp.ml | 6 +++--- plugins/ltac/tacsubst.ml | 18 ++++++++---------- plugins/ltac/tauto.ml | 2 +- 9 files changed, 31 insertions(+), 34 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index dffd90be35..d6cbd8db14 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -161,7 +161,7 @@ GEXTEND Gram | st = simple_tactic -> st | a = tactic_arg -> TacArg(!@loc,a) | r = reference; la = LIST0 tactic_arg_compat -> - TacArg(!@loc,TacCall (!@loc,r,la)) ] + TacArg(!@loc, TacCall (!@loc,(r,la))) ] | "0" [ "("; a = tactic_expr; ")" -> a | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> @@ -219,7 +219,7 @@ GEXTEND Gram ; tactic_atom: [ [ n = integer -> TacGeneric (genarg_of_int n) - | r = reference -> TacCall (!@loc,r,[]) + | r = reference -> TacCall (!@loc,(r,[])) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; match_key: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 0dd6819fdf..ae596c411d 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1048,9 +1048,9 @@ 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)) -> + | TacArg(_,TacCall(loc,(f,l))) -> pr_with_comments loc (hov 1 ( pr.pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg l)), @@ -1059,7 +1059,7 @@ type 'a extra_genarg_printer = pr_tacarg a, latom | TacML (loc,s,l) -> pr_with_comments loc (pr.pr_extend 1 s l), lcall - | TacAlias (loc,kn,l) -> + | TacAlias (loc,(kn,l)) -> pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom ) in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 1f75f88d42..40484bfeab 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1969,7 +1969,7 @@ let make_tactic name = let loc = Loc.ghost in let tacpath = Libnames.qualid_of_string name in let tacname = Qualid (loc, tacpath) in - TacArg (loc, TacCall (loc, tacname, [])) + TacArg (loc, TacCall (Loc.tag ~loc (tacname, []))) let add_morphism_infer glob m n = init_setoid (); diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index cd8c9e471e..39121ac94e 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,(kn,l)):raw_tactic_expr) in let () = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 8aefe76059..e8e99fcfed 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 @@ -268,7 +267,7 @@ and 'a gen_tactic_expr = (* For ML extensions *) | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list (* 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 ad9814b84b..df845b1a40 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -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,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 *) @@ -624,12 +624,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) + 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 (adjust_loc 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 @@ -650,11 +650,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 aac63fcb2b..64eda28ed7 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1257,7 +1257,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 @@ -1341,9 +1341,9 @@ 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,[]) -> + | TacCall (loc,(r,[])) -> interp_ltac_reference loc true ist r - | TacCall (loc,f,l) -> + | TacCall (loc,(f,l)) -> let (>>=) = Ftactic.bind in interp_ltac_reference loc true ist f >>= fun fv -> Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 9582ebd899..c92dd23a09 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -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/tauto.ml b/plugins/ltac/tauto.ml index dc7ee6a234..30eed08d7a 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -264,7 +264,7 @@ let with_flags flags _ ist = let x = (loc, 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, TacCall (loc, (ArgVar f, [Reference (ArgVar x)])))) let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in -- cgit v1.2.3 From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 23:40:35 +0100 Subject: [location] Remove Loc.ghost. Now it is a private field, locations are optional. --- plugins/ltac/coretactics.ml4 | 5 ++-- plugins/ltac/evar_tactics.ml | 2 +- plugins/ltac/extraargs.ml4 | 6 ++--- plugins/ltac/extratactics.ml4 | 8 +++---- plugins/ltac/g_ltac.ml4 | 4 ++-- plugins/ltac/g_obligations.ml4 | 2 +- plugins/ltac/pptactic.ml | 42 +++++++++++++++++----------------- plugins/ltac/pptactic.mli | 2 +- plugins/ltac/profile_ltac.ml | 4 ++-- plugins/ltac/rewrite.ml | 41 ++++++++++++++++----------------- plugins/ltac/tacentries.ml | 22 +++++++++--------- plugins/ltac/tacentries.mli | 2 +- plugins/ltac/tacexpr.mli | 2 +- plugins/ltac/tacintern.ml | 10 ++++---- plugins/ltac/tacinterp.ml | 52 ++++++++++++++++++++---------------------- plugins/ltac/tacinterp.mli | 2 +- plugins/ltac/tacsubst.ml | 2 +- plugins/ltac/tactic_debug.ml | 19 +++++++-------- plugins/ltac/tactic_debug.mli | 2 +- plugins/ltac/tauto.ml | 11 ++++----- 20 files changed, 118 insertions(+), 122 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 28ff6df838..6890b31981 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 5d3f6df03d..a5d9697ae7 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -82,7 +82,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 53b726432c..aa81f148e2 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 232bd851ff..5123d6c403 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -76,7 +76,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 @@ -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 -> Loc.ghost | Some loc -> loc in - resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) + 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) 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 @@ -784,7 +784,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 d6cbd8db14..23643c5d34 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -460,7 +460,7 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, (arg, sep), id) -> +| Tacentries.TacNonTerm (_, ((arg, sep), id)) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -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, ((Names.Id.to_string nt, sep), p)) ] END VERNAC COMMAND EXTEND VernacTacticNotation diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 3e6e2db605..7d40758360 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/pptactic.ml b/plugins/ltac/pptactic.ml index ae596c411d..26ac3c53e3 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 +| TacNonTerm of ('a * Names.Id.t) Loc.located type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list @@ -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 rec 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,8 +264,8 @@ type 'a extra_genarg_printer = let rec pack prods args = match prods, args with | [], [] -> [] | TacTerm s :: prods, args -> TacTerm s :: pack prods args - | TacNonTerm (loc, symb, id) :: prods, arg :: args -> - TacNonTerm (loc, (symb, arg), id) :: pack prods args + | TacNonTerm (loc, (symb, id)) :: prods, arg :: args -> + TacNonTerm (loc, ((symb, arg), id)) :: pack prods args | _ -> raise Not_found in let prods = pack pp.pptac_prods l in @@ -275,7 +275,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 @@ -331,9 +331,9 @@ 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 *) @@ -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 @@ -416,7 +416,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 @@ -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) = @@ -574,7 +574,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 -> @@ -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 + | 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 + pr_with_comments ~loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm @@ -1078,7 +1078,7 @@ 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 @@ -1087,7 +1087,7 @@ type 'a extra_genarg_printer = if Int.equal n 0 then (List.rev acc, (ty,None)) else match Loc.obj ty with Glob_term.GProd(na,Explicit,a,b) -> - strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) 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 @@ -1158,7 +1158,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 @@ -1253,7 +1253,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 729338fb9a..23570392d8 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 +| TacNonTerm of ('a * Names.Id.t) 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 bcb28f77ce..eb97a0e70e 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 ************************************* *) @@ -250,7 +250,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 40484bfeab..19c2eaf0a7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1787,11 +1787,11 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = Loc.tag @@ CAppExpl ((None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l) +let mkappc s l = Loc.tag @@ 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, - Loc.tag @@ CAppExpl ((None, Qualid (Loc.ghost, qualid_of_string s),None), + (((Loc.tag @@ Name n),None), Explicit, + Loc.tag @@ 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] @@ -1804,17 +1804,17 @@ let anew_instance global binders instance fields = let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(Ident (Loc.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 (); @@ -1838,16 +1838,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 @@ -1855,9 +1855,9 @@ 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 = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None) @@ -1959,17 +1959,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.tag ~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 (); @@ -2012,9 +2011,9 @@ 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, + (((Loc.tag @@ Name instance_id),None), Explicit, Loc.tag @@ CAppExpl ( - (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (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 diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 39121ac94e..f608515aa7 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -22,7 +22,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 +| TacNonTerm of ('a * Names.Id.t) Loc.located type raw_argument = string * string option type argument = Genarg.ArgT.any Extend.user_symbol @@ -178,7 +178,7 @@ let add_tactic_entry (kn, ml, tg) state = in let map = function | TacTerm s -> GramTerminal s - | TacNonTerm (loc, s, _) -> + | TacNonTerm (loc, (s, _)) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in GramNonTerminal (loc, typ, e) in @@ -206,7 +206,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s - | TacNonTerm (loc, (nt, sep), id) -> + | TacNonTerm (loc, ((nt, sep), id)) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> @@ -224,7 +224,7 @@ let interp_prod_item = function end in let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, symbol, id) + TacNonTerm (loc, (symbol, id)) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -300,7 +300,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj = let cons_production_parameter = function | TacTerm _ -> None -| TacNonTerm (_, _, id) -> Some id +| TacNonTerm (_, (_, id)) -> Some id let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { @@ -338,10 +338,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 @@ -355,7 +355,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 @@ -366,12 +366,12 @@ let add_ml_tactic_notation name ~level prods = let open Tacexpr in let get_id = function | TacTerm s -> None - | TacNonTerm (_, _, id) -> Some id + | TacNonTerm (_, (_, id)) -> Some id 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); diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 0695044736..48598f7f48 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 +| TacNonTerm of ('a * Names.Id.t) 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 e8e99fcfed..bf760e7bba 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -265,7 +265,7 @@ 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 (KerName.t * 'a gen_tactic_arg list) Loc.located diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index df845b1a40..787a5f50bd 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 Loc.ghost else loc +let adjust_loc loc = if !strict_check then None else Some loc (* Globalize a name which must be bound -- actually just check it is bound *) let intern_hyp ist (loc,id as locid) = @@ -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 *) @@ -550,7 +550,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 @@ -627,9 +627,9 @@ and intern_tactic_seq onlytac ist = function | TacAlias (loc,(s,l)) -> let l = List.map (intern_tacarg !strict_check false ist) l in ist.ltacvars, TacAlias (Loc.tag ~loc (s,l)) - | TacML (loc,opn,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 diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 64eda28ed7..e969b86f6f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -201,8 +201,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) @@ -326,7 +324,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) @@ -370,22 +368,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 *) @@ -531,7 +529,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 [] @@ -541,7 +539,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 @@ -977,14 +975,14 @@ 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)) = @@ -1012,14 +1010,14 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = sigma, (c, bl) let loc_of_bindings = function -| NoBindings -> Loc.ghost -| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) -| ExplicitBindings l -> fst (List.last l) +| NoBindings -> None +| ImplicitBindings l -> Some (loc_of_glob_constr (fst (List.last l))) +| ExplicitBindings l -> Some (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.opt_merge 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 @@ -1288,8 +1286,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 @@ -1308,7 +1306,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 = @@ -1322,7 +1320,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 @@ -1333,7 +1331,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 @@ -1342,16 +1340,16 @@ and interp_tacarg ist arg : Val.t Ftactic.t = Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) end } | TacCall (loc,(r,[])) -> - interp_ltac_reference loc true ist 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 -> @@ -1442,7 +1440,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 @@ -1768,7 +1766,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 @@ -1780,7 +1778,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 @@ -2132,7 +2130,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 1e5f6bd42b..6cd5a63b32 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -111,7 +111,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 c92dd23a09..0ee6e8a859 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -234,7 +234,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacAlias (_,(s,l)) -> let s = subst_kn subst s in TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l)) - | TacML (_loc,opn,l) -> TacML (_loc, opn,List.map (subst_tacarg subst) l) + | 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) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index dffeade298..ac8534bdc4 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -352,7 +352,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 @@ -389,14 +389,15 @@ let skip_extensions trace = let finer_loc loc1 loc2 = Loc.merge 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 + 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 *) - 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 *) @@ -411,14 +412,14 @@ let extract_ltac_trace trace eloc = 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 7745d9b7b6..38d8caca63 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -78,4 +78,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 30eed08d7a..df186cc46b 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -89,7 +89,6 @@ let _ = (** Base tactics *) -let loc = Loc.ghost let idtac = Proofview.tclUNIT () let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ())) @@ -207,7 +206,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] @@ -260,11 +259,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 @@ -272,7 +271,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 -- cgit v1.2.3 From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- plugins/ltac/extratactics.ml4 | 6 +- plugins/ltac/g_ltac.ml4 | 14 ++--- plugins/ltac/g_tactic.ml4 | 140 +++++++++++++++++++++--------------------- plugins/ltac/pptactic.ml | 12 ++-- plugins/ltac/taccoerce.ml | 4 +- plugins/ltac/taccoerce.mli | 2 +- plugins/ltac/tacentries.ml | 9 +-- plugins/ltac/tacintern.ml | 20 +++--- plugins/ltac/tacinterp.ml | 36 +++++------ plugins/ltac/tacsubst.ml | 2 +- plugins/ltac/tactic_debug.ml | 7 +-- 11 files changed, 126 insertions(+), 126 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 5123d6c403..dc43930e4d 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 23643c5d34..e20beae963 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 d1e5c810f4..8aaad05666 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 26ac3c53e3..bdafbdc78c 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 b76009c997..e037bb4b26 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 9c4ac52657..b09672a12b 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 f608515aa7..a19dbd3276 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 787a5f50bd..44ea3ff1d6 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 e969b86f6f..4d5b844550 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 0ee6e8a859..4390ff08b4 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 ac8534bdc4..f04495c61d 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 -- cgit v1.2.3 From 9122623f2377bfe6aad0d4ea662481992e768201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 19:40:57 +0200 Subject: [location] Remove `Loc.internal_ghost` `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it. --- plugins/ltac/tacentries.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a19dbd3276..1de4024fd1 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -180,8 +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) + GramNonTerminal (Loc.tag ?loc (typ, e)) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in -- cgit v1.2.3 From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 23:19:35 +0200 Subject: [location] [ast] Switch Constrexpr AST to an extensible node type. Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. --- plugins/ltac/g_ltac.ml4 | 8 ++++---- plugins/ltac/g_tactic.ml4 | 12 ++++++------ plugins/ltac/pptactic.ml | 2 +- plugins/ltac/rewrite.ml | 12 ++++++------ plugins/ltac/tacintern.ml | 10 +++++----- plugins/ltac/tacinterp.ml | 2 +- 6 files changed, 23 insertions(+), 23 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index e20beae963..5fc22cb4ad 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -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 _loc, 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 ()) ] ] ; @@ -255,10 +255,10 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | _loc, CCast (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 (Loc.tag @@ CHole (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 - Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] + CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] ; END diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 8aaad05666..60deb443a9 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -130,14 +130,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, Loc.tag ~loc @@ CProdN(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,Loc.tag ~loc @@ CProdN(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 @@ -154,12 +154,12 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(Loc.tag @@ CPrim (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,(Loc.tag @@ 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 @@ -169,7 +169,7 @@ let mkTacCase with_evar = function 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:(Loc.merge_opt loc1 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 @@ -440,7 +440,7 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (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) ] ] ; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index bdafbdc78c..58473d7ddf 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -340,7 +340,7 @@ type 'a extra_genarg_printer = let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = - match snd ty with + match ty.CAst.v with Constrexpr.CProdN(bll,a) -> let nb = List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 19c2eaf0a7..2ef435b6ba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1787,18 +1787,18 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = Loc.tag @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ 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.tag @@ Name n),None), Explicit, - Loc.tag @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), + 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, Loc.tag @@ CRecord (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 = @@ -1859,7 +1859,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2); (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = Loc.tag @@ CHole (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 @@ -2012,13 +2012,13 @@ let add_morphism glob binders m s n = let instance_id = add_suffix n "_Proper" in let instance = (((Loc.tag @@ Name instance_id),None), Explicit, - Loc.tag @@ CAppExpl ( + 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, Loc.tag @@ CRecord [])) + (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/tacintern.ml b/plugins/ltac/tacintern.ml index 44ea3ff1d6..566dd8ed7b 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -108,13 +108,13 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (Loc.tag @@ GVar id), Some (Loc.tag @@ CRef (r,None)) + (Loc.tag @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (Loc.tag @@ GVar id), if strict then None else Some (Loc.tag @@ CRef (r,None)) + (Loc.tag @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in Loc.tag @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (Loc.tag @@ CRef (r,None)) + if strict then None else Some (CAst.make @@ CRef (r,None)) let intern_move_location ist = function | MoveAfter id -> MoveAfter (intern_hyp ist id) @@ -271,7 +271,7 @@ 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 (Loc.tag @@ CRef (Ident (Loc.tag id), None)) with + match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with | (loc, GVar id), _ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else @@ -361,7 +361,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 -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 4d5b844550..449027b52e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -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 (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 -- cgit v1.2.3 From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Apr 2017 03:35:20 +0200 Subject: [location] [ast] Port module AST to CAst --- plugins/ltac/extratactics.ml4 | 8 ++++---- plugins/ltac/g_rewrite.ml4 | 2 +- plugins/ltac/pptactic.ml | 2 +- plugins/ltac/tacintern.ml | 10 +++++----- plugins/ltac/tacinterp.ml | 4 ++-- 5 files changed, 13 insertions(+), 13 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index dc43930e4d..9d50b6e6f9 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -631,14 +631,14 @@ 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; - Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@ + CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true), Misctypes.IntroAnonymous, None))) else x @@ -651,12 +651,12 @@ 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; - Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@ + 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 diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 1f40c67b5d..b4a0e46ae7 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - 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 Tacticals.onAllHypsAndConcl (fun cl -> match cl with diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 58473d7ddf..87b79374e7 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1085,7 +1085,7 @@ type 'a extra_genarg_printer = 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 Loc.obj ty with + 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 diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 566dd8ed7b..8751a14c71 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -108,12 +108,12 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (Loc.tag @@ GVar id), Some (CAst.make @@ CRef (r,None)) + (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (Loc.tag @@ GVar id), if strict then None else Some (CAst.make @@ 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 - Loc.tag @@ GRef (locate_global_with_alias lqid,None), + CAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (CAst.make @@ CRef (r,None)) let intern_move_location ist = function @@ -272,7 +272,7 @@ let intern_destruction_arg ist = function if !strict_check then (* If in a defined tactic, no intros-until *) match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with - | (loc, GVar id), _ -> clear,ElimOnIdent (loc,id) + | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else clear,ElimOnIdent (loc,id) @@ -350,7 +350,7 @@ 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 Loc.obj c with + match c.CAst.v with | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) | GVar id -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 449027b52e..91bc46fe72 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -697,7 +697,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) | _ -> @@ -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 (CAst.make @@ 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 -- cgit v1.2.3