diff options
Diffstat (limited to 'plugins/ltac')
27 files changed, 549 insertions, 533 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 28ff6df83..0a13a20a9 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,39 @@ 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" + +(* First-class Ltac access to primitive blocks *) + +let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; } +let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; } + +let register_list_tactical name f = + let tac args ist = match args with + | [v] -> + begin match Tacinterp.Value.to_list v with + | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list") + | Some tacs -> + let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in + f tacs + end + | _ -> assert false + in + Tacenv.register_ml_tactic (initial_name name) [|tac|] + +let () = register_list_tactical "first" Tacticals.New.tclFIRST +let () = register_list_tactical "solve" Tacticals.New.tclSOLVE + +let initial_tacticals () = + let idn n = Id.of_string (Printf.sprintf "_%i" n) in + let varn n = Reference (ArgVar (None, idn n)) in + let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in + List.iter iter [ + "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0]))); + "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0]))); + ] + +let () = Mltop.declare_cache_obj initial_tacticals "coretactics" diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index bc9c300e2..bf84f61a5 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -56,17 +56,16 @@ let instantiate_tac n c ido = InHyp -> (match decl with | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ) - | _ -> error - "Please be more specific: in type or value?") + | _ -> user_err Pp.(str "Please be more specific: in type or value?")) | InHypTypeOnly -> evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl)) | InHypValueOnly -> (match decl with | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) - | _ -> error "Not a defined hypothesis.") in + | _ -> user_err Pp.(str "Not a defined hypothesis.")) in if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; + user_err Pp.(str "Not enough uninstantiated existential variables."); + if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in instantiate_evar evk c sigma gl end @@ -76,12 +75,12 @@ let instantiate_tac_by_name id c = let sigma = gl.sigma in let evk = try Evd.evar_key id sigma - with Not_found -> error "Unknown existential variable." in + with Not_found -> user_err Pp.(str "Unknown existential variable.") in instantiate_evar evk c sigma gl 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 @@ -109,8 +108,8 @@ let hget_evar n = let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; + user_err Pp.(str "Not enough uninstantiated existential variables."); + if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 53b726432..fdb8d3461 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -90,7 +90,7 @@ let occurrences_of = function | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) | nl -> if List.exists (fun n -> n < 0) nl then - CErrors.error "Illegal negative occurrence number."; + CErrors.user_err Pp.(str "Illegal negative occurrence number."); OnlyOccurrences nl let coerce_to_int v = match Value.to_int v with @@ -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 @@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause | [ in_clause'(cl) ] -> [ cl ] END +let local_test_lpar_id_colon = + let err () = raise Stream.Failure in + Pcoq.Gram.Entry.of_parser "lpar_id_colon" + (fun strm -> + match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> + (match Util.stream_nth 1 strm with + | Tok.IDENT _ -> + (match Util.stream_nth 2 strm with + | Tok.KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +let pr_lpar_id_colon _ _ _ _ = mt () + +ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon +| [ local_test_lpar_id_colon(x) ] -> [ () ] +END + (* spiwack: the print functions are incomplete, but I don't know what they are used for *) let pr_r_nat_field natf = diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 7d4bccfad..9b4167512 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -67,6 +67,10 @@ val pr_by_arg_tac : (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> raw_tactic_expr option -> Pp.std_ppcmds +val test_lpar_id_colon : unit Pcoq.Gram.entry + +val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type + (** Spiwack: Primitive for retroknowledge registration *) val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 3e6ccaf84..9726a5b40 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -73,7 +73,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id) + | NamedHyp id -> None,ElimOnIdent (Loc.tag id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a @@ -264,7 +264,7 @@ let add_rewrite_hint bases ort t lcsr = (Declare.declare_universe_context false ctx; Univ.ContextSet.empty) in - Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in + Loc.tag ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in let eqs = List.map f lcsr in let add_hints base = add_rew_rules base eqs in List.iter add_hints bases @@ -306,6 +306,7 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in + let sigma, p = Evd.fresh_global env sigma p in let p = EConstr.of_constr p in let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn @@ -463,7 +464,7 @@ open Evar_tactics (* TODO: add support for some test similar to g_constr.name_colon so that expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar - [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] + [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END @@ -628,15 +629,15 @@ let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function - | GVar (_,id) as x -> + | { CAst.v = GVar id } as x -> if Id.equal id tid then (decr occref; if Int.equal !occref 0 then x else (incr locref; - GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true), + CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in @@ -648,13 +649,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) -> + | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } -> decr occref; if Int.equal !occref 0 then tc else (incr locref; - GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) + CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t @@ -676,8 +677,8 @@ let hResolve id c occ t = with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> let (e, info) = CErrors.push e in - let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in - resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) + let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in + resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) in let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in let t_constr = EConstr.of_constr t_constr in @@ -735,7 +736,7 @@ let rewrite_except h = let refl_equal = let coq_base_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" + Coqlib.gen_reference_in_modules "RecursiveDefinition" (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in function () -> (coq_base_constant "eq_refl") @@ -746,8 +747,9 @@ let refl_equal = let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in - Tacticals.New.tclTHENLIST - [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))]; + Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> + Tacticals.New.tclTHENLIST + [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -781,7 +783,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 @@ -1084,7 +1086,7 @@ let decompose l c = let sigma = Tacmach.New.project gl in let to_ind c = if isInd sigma c then fst (destInd sigma c) - else error "not an inductive type" + else user_err Pp.(str "not an inductive type") in let l = List.map to_ind l in Elim.h_decompose l c diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ca5d198c2..36ac10bfe 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -41,7 +41,7 @@ let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) | Libnames.Qualid (loc,_) -> - CErrors.user_err ~loc + CErrors.user_err ?loc (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -159,9 +159,9 @@ GEXTEND Gram | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (g,n,l) | st = simple_tactic -> st - | a = tactic_arg -> TacArg(!@loc,a) + | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a) | r = reference; la = LIST0 tactic_arg_compat -> - TacArg(!@loc,TacCall (!@loc,r,la)) ] + TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ] | "0" [ "("; a = tactic_expr; ")" -> a | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> @@ -169,7 +169,7 @@ GEXTEND Gram | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) | None -> TacDispatch tf end - | a = tactic_atom -> TacArg (!@loc,a) ] ] + | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ] ; failkw: [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] @@ -187,7 +187,7 @@ GEXTEND Gram (* Tactic arguments to the right of an application *) tactic_arg_compat: [ [ a = tactic_arg -> a - | c = Constr.constr -> (match c with CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c)) + | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) (* Unambiguous entries: tolerated w/o "ltac:" modifier *) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; @@ -203,7 +203,7 @@ GEXTEND Gram verbose most of the time. *) fresh_id: [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ] + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -219,7 +219,7 @@ GEXTEND Gram ; tactic_atom: [ [ n = integer -> TacGeneric (genarg_of_int n) - | r = reference -> TacCall (!@loc,r,[]) + | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[])) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; match_key: @@ -255,10 +255,10 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) + | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty) + in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) ] ] ; match_context_rule: @@ -353,7 +353,7 @@ GEXTEND Gram operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in - CHole (!@loc, None, IntroAnonymous, Some arg) ] ] + CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] ; END @@ -367,7 +367,6 @@ open Libnames let print_info_trace = ref None let _ = declare_int_option { - optsync = true; optdepr = false; optname = "print info trace"; optkey = ["Info" ; "Level"]; @@ -460,7 +459,9 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, (arg, sep), id) -> +| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg +| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false +| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -470,7 +471,9 @@ let pr_ltac_production_item = function VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ] +| [ ident(nt) ] -> + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ] END VERNAC COMMAND EXTEND VernacTacticNotation diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 3e6e2db60..4dceb0331 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -31,7 +31,7 @@ let () = Obligations.default_tactic := tac let with_tac f tac = - let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in + let env = Genintern.empty_glob_sign (Global.env ()) in let tac = match tac with | None -> None | Some tac -> @@ -50,7 +50,7 @@ module Tactic = Pltac open Pcoq -let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref = mkRefC (Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Init.Specif.sig")) type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index ac979bcf8..5adf8475a 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -124,7 +124,7 @@ END let clsubstitute o c = Proofview.Goal.enter { enter = begin fun gl -> - let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in + let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun cl -> diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 4b3ca80af..83bfd0233 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq = | _ -> err ()) (* idem for (x:t) *) -let test_lpar_id_colon = - Gram.Entry.of_parser "lpar_id_colon" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) +open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = @@ -128,16 +117,16 @@ let mk_fix_tac (loc,id,bl,ann,ty) = | _, Some x -> let ids = List.map snd (List.flatten (List.map pi1 bl)) in (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)) + with Not_found -> user_err Pp.(str "No such fix variable.")) + | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in + (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = let _ = Option.map (fun (aloc,_) -> user_err ~loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in - (id,CProdN(loc,bl,ty)) + (id,CAst.make ~loc @@ CProdN(bl,ty)) (* Functions overloaded by quotifier *) let destruction_arg_of_constr (c,lbind as clbind) = match lbind with @@ -154,32 +143,32 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)), + (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)), NoBindings))) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> - TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then - error "Use of numbers as direct arguments of 'case' is not supported."; + user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported."); TacInductionDestruct (false,with_evar,ic) -let rec mkCLambdaN_simple_loc loc bll c = +let rec mkCLambdaN_simple_loc ?loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> - CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c) - | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c + CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) + | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c let mkCLambdaN_simple bl c = match bl with | [] -> c | h :: _ -> - let loc = Loc.merge (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in - mkCLambdaN_simple_loc loc bl c + let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in + mkCLambdaN_simple_loc ?loc bl c -let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (List.last l)) +let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) let map_int_or_var f = function | ArgArg x -> ArgArg (f x) @@ -301,7 +290,7 @@ GEXTEND Gram (* (A & B & C) is translated into (A,(B,C)) *) let rec pairify = function | ([]|[_]|[_;_]) as l -> l - | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] + | t::q -> [t; Loc.tag ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] in IntroAndPattern (pairify (si::tc)) ] ] ; equality_intropattern: @@ -316,8 +305,8 @@ GEXTEND Gram ; nonsimple_intropattern: [ [ l = simple_intropattern -> l - | "*" -> !@loc, IntroForthcoming true - | "**" -> !@loc, IntroForthcoming false ]] + | "*" -> Loc.tag ~loc:!@loc @@ IntroForthcoming true + | "**" -> Loc.tag ~loc:!@loc @@ IntroForthcoming false ]] ; simple_intropattern: [ [ pat = simple_intropattern_closed; @@ -325,19 +314,19 @@ GEXTEND Gram let loc0,pat = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in - let loc = Loc.merge loc0 loc1 in + let loc = Loc.merge_opt loc0 loc1 in IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in - !@loc, List.fold_right f l pat ] ] + Loc.tag ~loc:!@loc @@ List.fold_right f l pat ] ] ; simple_intropattern_closed: - [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat) - | pat = equality_intropattern -> !@loc, IntroAction pat - | "_" -> !@loc, IntroAction IntroWildcard - | pat = naming_intropattern -> !@loc, IntroNaming pat ] ] + [ [ pat = or_and_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat) + | pat = equality_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction pat + | "_" -> Loc.tag ~loc:!@loc @@ IntroAction IntroWildcard + | pat = naming_intropattern -> Loc.tag ~loc:!@loc @@ IntroNaming pat ] ] ; simple_binding: - [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c) - | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ] + [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c) + | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> @@ -440,7 +429,7 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit,CHole (!@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) + [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; @@ -468,7 +457,7 @@ GEXTEND Gram | -> None ] ] ; or_and_intropattern_loc: - [ [ ipat = or_and_intropattern -> ArgArg (!@loc,ipat) + [ [ ipat = or_and_intropattern -> ArgArg (Loc.tag ~loc:!@loc ipat) | locid = identref -> ArgVar locid ] ] ; as_or_and_ipat: @@ -476,13 +465,13 @@ GEXTEND Gram | -> None ] ] ; eqn_ipat: - [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat) + [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (Loc.tag ~loc:!@loc pat) | IDENT "_eqn"; ":"; pat = naming_intropattern -> let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat) + warn_deprecated_eqn_syntax ~loc "H"; Some (Loc.tag ~loc pat) | IDENT "_eqn" -> let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous) + warn_deprecated_eqn_syntax ~loc "?"; Some (Loc.tag ~loc IntroAnonymous) | -> None ] ] ; as_name: @@ -521,145 +510,171 @@ 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 (false,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 (false,na,b,Locusops.nowhere,true,None)) + | IDENT "epose"; (id,b) = bindings_with_parameters -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) + | IDENT "epose"; b = constr; na = as_name -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,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 (false,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 (false,na,c,p,true,None)) + | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) + | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,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 (false,na,c,p,false,e)) + | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat; + p = clause_dft_all -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,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 (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + c = lconstr; ")" -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,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 (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,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,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,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 (false,true,Some tac,ipat,c)) + | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,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 (false,true,None,ipat,c)) + | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,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,false,Some tac,ipat,c)) + | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,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 b73b66e56..902985827 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 option) Loc.located type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list @@ -149,7 +149,7 @@ type 'a extra_genarg_printer = let pr_or_by_notation f = function | AN v -> f v - | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_located pr (loc,x) = pr x @@ -161,28 +161,6 @@ type 'a extra_genarg_printer = | AnonHyp n -> int n | 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) - - let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc prc l) - | ExplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l) - | NoBindings -> mt () - - let pr_bindings_no_with prc prlc = function - | ImplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc prc l - | ExplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - let pr_clear_flag clear_flag pp x = match clear_flag with | Some false -> surround (pp x) @@ -190,7 +168,7 @@ type 'a extra_genarg_printer = | None -> pp x let pr_with_bindings prc prlc (c,bl) = - prc c ++ pr_bindings prc prlc bl + prc c ++ Miscprint.pr_bindings prc prlc bl let pr_with_bindings_arg prc prlc (clear_flag,c) = pr_clear_flag clear_flag (pr_with_bindings prc prlc) c @@ -212,7 +190,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 +230,7 @@ type 'a extra_genarg_printer = let prods = (KNmap.find key !prnotation_tab).pptac_prods in let pr = function | TacTerm s -> primitive s - | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) + | TacNonTerm (_, (symb, _)) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) in pr_sequence pr prods with Not_found -> @@ -264,8 +242,9 @@ type 'a extra_genarg_printer = let rec pack prods args = match prods, args with | [], [] -> [] | TacTerm s :: prods, args -> TacTerm s :: pack prods args - | TacNonTerm (loc, symb, id) :: prods, arg :: args -> - TacNonTerm (loc, (symb, arg), id) :: pack prods args + | TacNonTerm (_, (_, None)) :: prods, args -> pack prods args + | TacNonTerm (loc, (symb, (Some _ as ido))) :: prods, arg :: args -> + TacNonTerm (loc, ((symb, arg), ido)) :: pack prods args | _ -> raise Not_found in let prods = pack pp.pptac_prods l in @@ -275,7 +254,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,28 +310,28 @@ type 'a extra_genarg_printer = pr_extend_gen (pr_farg prtac) let pr_raw_alias prc prlc prtac prpat lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args let pr_glob_alias prc prlc prtac prpat lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args (**********************************************************************) (* The tactic printer *) let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = - match ty with - Constrexpr.CProdN(_,bll,a) -> + match ty.CAst.v with + Constrexpr.CProdN(bll,a) -> let nb = List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in let bll = List.map (fun (x, _, y) -> x, y) bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a - | _ -> error "Cannot translate fix tactic: not enough products" in + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty 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 @@ -366,30 +345,6 @@ type 'a extra_genarg_printer = | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) - let pr_esubst prc l = - let pr_qhyp = function - (_,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 - - let pr_bindings_gen for_ex prc prlc = function - | ImplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - prlist_with_sep spc prc l) - | ExplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - pr_esubst prlc l) - | NoBindings -> mt () - - let pr_bindings prc prlc = pr_bindings_gen false prc prlc - - let pr_with_bindings prc prlc (c,bl) = - hov 1 (prc c ++ pr_bindings prc prlc bl) - let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl @@ -416,7 +371,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 +462,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) = @@ -570,18 +525,18 @@ type 'a extra_genarg_printer = str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar n = spc () ++ pr_name n + let pr_funvar n = spc () ++ Name.print n 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 -> hv 0 (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) - | [] -> anomaly (Pp.str "LetIn must declare at least one binding") + | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = hv 0 (str "[ " ++ @@ -767,15 +722,15 @@ type 'a extra_genarg_printer = primitive "cofix" ++ spc () ++ pr_id id ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l ) - | TacAssert (b,Some tac,ipat,c) -> + | TacAssert (ev,b,Some tac,ipat,c) -> hov 1 ( - primitive (if b then "assert" else "enough") ++ + primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) - | TacAssert (_,None,ipat,c) -> + | TacAssert (ev,_,None,ipat,c) -> hov 1 ( - primitive "pose proof" + primitive (if ev then "epose proof" else "pose proof") ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ) | TacGeneralize l -> @@ -785,11 +740,11 @@ type 'a extra_genarg_printer = pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> - hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) - | TacLetTac (na,c,cl,b,e) -> + | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl -> + hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c) + | TacLetTac (ev,na,c,cl,b,e) -> hov 1 ( - (if b then primitive "set" else primitive "remember") ++ + primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c else pr_pose_as_style pr.pr_constr na c) ++ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ @@ -1037,7 +992,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)) -> @@ -1048,19 +1003,19 @@ type 'a extra_genarg_printer = primitive "fresh" ++ pr_fresh_ids l, latom | TacArg(_,TacGeneric arg) -> pr.pr_generic arg, latom - | TacArg(_,TacCall(loc,f,[])) -> + | TacArg(_,TacCall(loc,(f,[]))) -> pr.pr_reference f, latom - | TacArg(_,TacCall(loc,f,l)) -> - pr_with_comments loc (hov 1 ( + | TacArg(_,TacCall(loc,(f,l))) -> + pr_with_comments ?loc (hov 1 ( pr.pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg l)), lcall | TacArg (_,a) -> pr_tacarg a, latom - | TacML (loc,s,l) -> - pr_with_comments loc (pr.pr_extend 1 s l), lcall - | TacAlias (loc,kn,l) -> - pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom + | TacML (loc,(s,l)) -> + pr_with_comments ?loc (pr.pr_extend 1 s l), lcall + | TacAlias (loc,(kn,l)) -> + pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm @@ -1078,17 +1033,17 @@ type 'a extra_genarg_printer = | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a)))) + hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.tag a)))) in pr_tac let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match ty with - Glob_term.GProd(loc,na,Explicit,a,b) -> - strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in + match ty.CAst.v with + Glob_term.GProd(na,Explicit,a,b) -> + strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let raw_printers = @@ -1158,8 +1113,8 @@ 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 - | _ -> error "Cannot translate fix tactic: not enough products" in + strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_atomic_tactic_level env sigma n t = @@ -1209,7 +1164,7 @@ let declare_extra_genarg_pprule wit (h : 'c extra_genarg_printer) = begin match wit with | ExtraArg s -> () - | _ -> error "Can declare a pretty-printing rule only for extra argument types." + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in let g x = @@ -1253,7 +1208,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 @@ -1279,9 +1234,9 @@ let () = (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; Genprint.register_print0 wit_bindings - (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); + (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 729338fb9..4265c416b 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 option) Loc.located type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> @@ -106,10 +106,6 @@ val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds -val pr_bindings : - ('constr -> std_ppcmds) -> - ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds - val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index a853576f2..b237e917d 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -113,7 +113,7 @@ let rec to_ltacprof_tactic m xml = children = List.fold_left to_ltacprof_tactic M.empty xs; } in M.add name node m - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML.") let to_ltacprof_results xml = let open Xml_datatype in @@ -125,11 +125,11 @@ let to_ltacprof_results xml = max_total = 0.0; local = 0.0; children = List.fold_left to_ltacprof_tactic M.empty xs } - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML.") let feedback_results results = Feedback.(feedback - (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results))) + (Custom (None, "ltacprof_results", of_ltacprof_results results))) (* ************** pretty printing ************************************* *) @@ -249,7 +249,7 @@ let string_of_call ck = | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id | Tacexpr.LtacAtomCall te -> (Pptactic.pr_glob_tactic (Global.env ()) - (Tacexpr.TacAtom (Loc.ghost, te))) + (Tacexpr.TacAtom (Loc.tag te))) | Tacexpr.LtacConstrInterp (c, _) -> pr_glob_constr_env (Global.env ()) c | Tacexpr.LtacMLCall te -> @@ -411,8 +411,7 @@ let _ = Declaremods.append_end_library_hook do_print_results_at_close let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Ltac Profiling"; optkey = ["Ltac"; "Profiling"]; optread = get_profiling; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5630a2d7b..f028abde9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -55,22 +55,16 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] -let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let lazy_find_reference dir s = + let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in + fun () -> Lazy.force gr -let try_find_global_reference dir s = - let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting") - -let find_reference dir s = - let gr = lazy (try_find_global_reference dir s) in - fun () -> Lazy.force gr +let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = - let gr = lazy (try_find_global_reference dir s) in + let gr = lazy (find_reference dir s) in fun (evd,cstrs) -> let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in @@ -81,7 +75,7 @@ let find_global dir s = (** Global constants. *) -let coq_eq_ref = find_reference ["Init"; "Logic"] "eq" +let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq" let coq_eq = find_global ["Init"; "Logic"] "eq" let coq_f_equal = find_global ["Init"; "Logic"] "f_equal" let coq_all = find_global ["Init"; "Logic"] "all" @@ -158,11 +152,11 @@ end) = struct let forall_relation = find_global morphisms "forall_relation" let pointwise_relation = find_global morphisms "pointwise_relation" - let forall_relation_ref = find_reference morphisms "forall_relation" - let pointwise_relation_ref = find_reference morphisms "pointwise_relation" + let forall_relation_ref = lazy_find_reference morphisms "forall_relation" + let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation" let respectful = find_global morphisms "respectful" - let respectful_ref = find_reference morphisms "respectful" + let respectful_ref = lazy_find_reference morphisms "respectful" let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation" @@ -174,8 +168,8 @@ end) = struct let rewrite_relation_class = find_global relation_classes "RewriteRelation" - let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper")) - let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy")) + let proper_class = lazy (class_info (find_reference morphisms "Proper")) + let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy")) let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) @@ -241,8 +235,8 @@ end) = struct let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs - else error "build_signature: no constraint can apply on a dependent argument" - | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") + else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") + | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.") | _, [] -> (match finalcstr with | None | Some (_, None) -> @@ -478,7 +472,7 @@ type hypinfo = { let get_symmetric_proof b = if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof -let error_no_relation () = error "Cannot find a relation to rewrite." +let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.") let rec decompose_app_rel env evd t = (** Head normalize for compatibility with the old meta mechanism *) @@ -531,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) = let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c - | None -> error "Cannot find an homogeneous relation to rewrite." + | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.") let rewrite_db = "rewrite" @@ -757,17 +751,23 @@ let default_flags = { under_lambdas = true; on_morphisms = true; } let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None -let make_eq () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let make_eq_refl () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ())) +let new_global (evars, cstrs) gr = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr + in (Sigma.to_evar_map sigma, cstrs), c + +let make_eq sigma = + new_global sigma (Coqlib.build_coq_eq ()) +let make_eq_refl sigma = + new_global sigma (Coqlib.build_coq_eq_refl ()) -let get_rew_prf r = match r.rew_prf with - | RewPrf (rel, prf) -> rel, prf +let get_rew_prf evars r = match r.rew_prf with + | RewPrf (rel, prf) -> evars, (rel, prf) | RewCast c -> - let rel = mkApp (make_eq (), [| r.rew_car |]) in - rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]), - c, mkApp (rel, [| r.rew_from; r.rew_to |])) + let evars, eq = make_eq evars in + let evars, eq_refl = make_eq_refl evars in + let rel = mkApp (eq, [| r.rew_car |]) in + evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]), + c, mkApp (rel, [| r.rew_from; r.rew_to |]))) let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation @@ -833,11 +833,12 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev env evars carrier relation x in [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs' | Some r -> - [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, + let evars, proof = get_rew_prf evars r in + [ snd proof; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then - error "Cannot rewrite inside dependent arguments of a function"; + user_err Pp.(str "Cannot rewrite inside dependent arguments of a function"); x :: acc, x :: subst, evars, sigargs, x :: typeargs') ([], [], evars, sigargs, []) args args' in @@ -853,7 +854,8 @@ let apply_constraint env avoid car rel prf cstr res = | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res let coerce env avoid cstr res = - let rel, prf = get_rew_prf res in + let evars, (rel, prf) = get_rew_prf res.rew_evars res in + let res = { res with rew_evars = evars } in apply_constraint env avoid res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = @@ -874,8 +876,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let rel, prf = get_rew_prf res in - let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in + let res = Success (coerce env unfresh cstr res) in (occ, res) } @@ -1237,9 +1238,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> - let rel, prf = get_rew_prf r in - Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r) + | Success r -> Success (coerce env unfresh (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail @@ -1425,7 +1424,7 @@ module Strategies = let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> - error "fold: the term is not unfoldable !" + user_err Pp.(str "fold: the term is not unfoldable!") in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in @@ -1786,34 +1785,34 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l) let declare_an_instance n s args = - (((Loc.ghost,Name n),None), Explicit, - CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None), + (((Loc.tag @@ Name n),None), Explicit, + CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) - binders instance (Some (true, CRecord (Loc.ghost,fields))) + binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "reflexivity"),lemma)] + [(Ident (Loc.tag @@ Id.of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "symmetry"),lemma)] + [(Ident (Loc.tag @@ Id.of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "transitivity"),lemma)] + [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1837,16 +1836,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "PreOrder_Reflexive"), lemma1); - (Ident (Loc.ghost,Id.of_string "PreOrder_Transitive"),lemma3)]) + [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1); + (Ident (Loc.tag @@ Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "PER_Symmetric"), lemma2); - (Ident (Loc.ghost,Id.of_string "PER_Transitive"),lemma3)]) + [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2); + (Ident (Loc.tag @@ Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1854,11 +1853,11 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), lemma1); - (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2); - (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)]) + [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), lemma1); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) +let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) let proper_projection sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in @@ -1958,17 +1957,16 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let make_tactic name = let open Tacexpr in - let loc = Loc.ghost in let tacpath = Libnames.qualid_of_string name in - let tacname = Qualid (loc, tacpath) in - TacArg (loc, TacCall (loc, tacname, [])) + let tacname = Qualid (Loc.tag tacpath) in + TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, []))) let add_morphism_infer glob m n = init_setoid (); @@ -2011,14 +2009,14 @@ let add_morphism glob binders m s n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = - (((Loc.ghost,Name instance_id),None), Explicit, - CAppExpl (Loc.ghost, - (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (((Loc.tag @@ Name instance_id),None), Explicit, + CAst.make @@ CAppExpl ( + (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~global:glob poly binders instance - (Some (true, CRecord (Loc.ghost,[]))) + (Some (true, CAst.make @@ CRecord [])) ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) @@ -2205,7 +2203,7 @@ let setoid_symmetry_in id = let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "Cannot find an equivalence relation to rewrite." + | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.") in let others,(c1,c2) = split_last_two args in let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index b76009c99..e037bb4b2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -268,11 +268,11 @@ let coerce_to_constr_list env v = List.map map l | None -> raise (CannotCoerceTo "a term list") -let coerce_to_intro_pattern_list loc env sigma v = +let coerce_to_intro_pattern_list ?loc env sigma v = match Value.to_list v with | None -> raise (CannotCoerceTo "an intro pattern list") | Some l -> - let map v = (loc, coerce_to_intro_pattern env sigma v) in + let map v = Loc.tag ?loc @@ coerce_to_intro_pattern env sigma v in List.map map l let coerce_to_hyp env sigma v = diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 4a44f86d9..9883c03c4 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -75,7 +75,7 @@ val coerce_to_evaluable_ref : val coerce_to_constr_list : Environ.env -> Value.t -> constr list val coerce_to_intro_pattern_list : - Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns + ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 32750383b..f44ccbd3b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -21,7 +21,7 @@ open Nameops type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of ('a * Names.Id.t option) Loc.located type raw_argument = string * string option type argument = Genarg.ArgT.any Extend.user_symbol @@ -60,7 +60,7 @@ let get_tacentry n m = else EntryName (rawwit Tacarg.wit_tactic, atactic n) let get_separator = function -| None -> error "Missing separator." +| None -> user_err Pp.(str "Missing separator.") | Some sep -> sep let rec parse_user_entry s sep = @@ -110,7 +110,7 @@ let get_tactic_entry n = else if 1<=n && n<5 then Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) else - error ("Invalid Tactic Notation level: "^(string_of_int n)^".") + user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) (**********************************************************************) (** State of the grammar extensions *) @@ -166,17 +166,17 @@ 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 - error "Notation for simple tactic must start with an identifier." + user_err Pp.(str "Notation for simple tactic must start with an identifier.") in let map = function | TacTerm s -> GramTerminal s - | TacNonTerm (loc, s, _) -> + | TacNonTerm (loc, (s, ido)) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (loc, typ, e) + GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e)) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in @@ -202,13 +202,13 @@ 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), ido)) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names else begin match ArgT.name s with - | None -> error ("Unknown entry "^s^".") + | None -> user_err Pp.(str ("Unknown entry "^s^".")) | Some arg -> arg end | Some n -> @@ -220,7 +220,7 @@ let interp_prod_item = function end in let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, symbol, id) + TacNonTerm (loc, (symbol, ido)) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -253,8 +253,8 @@ let pprule pa = { let check_key key = if Tacenv.check_alias key then - error "Conflicting tactic notations keys. This can happen when including \ - twice the same module." + user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \ + twice the same module.") let cache_tactic_notation (_, tobj) = let key = tobj.tacobj_key in @@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj = let cons_production_parameter = function | TacTerm _ -> None -| TacNonTerm (_, _, id) -> Some id +| TacNonTerm (_, (_, ido)) -> ido let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { @@ -334,10 +334,10 @@ let extend_atomic_tactic name entries = in let empty_value = function | TacTerm s -> raise NonEmptyArgument - | TacNonTerm (_, symb, _) -> + | TacNonTerm (_, (symb, _)) -> let EntryName (typ, e) = prod_item_of_symbol 0 symb in let Genarg.Rawwit wit = typ in - let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in + let inj x = TacArg (Loc.tag @@ TacGeneric (Genarg.in_gen typ x)) in let default = epsilon_value inj e in match default with | None -> raise NonEmptyArgument @@ -351,7 +351,7 @@ let extend_atomic_tactic name entries = | Some (id, args) -> let args = List.map (fun a -> Tacexp a) args in let entry = { mltac_name = name; mltac_index = i } in - let body = TacML (Loc.ghost, entry, args) in + let body = TacML (Loc.tag (entry, args)) in Tacenv.register_ltac false false (Names.Id.of_string id) body in List.iteri add_atomic entries @@ -362,12 +362,12 @@ let add_ml_tactic_notation name ~level prods = let open Tacexpr in let get_id = function | TacTerm s -> None - | TacNonTerm (_, _, id) -> Some id + | TacNonTerm (_, (_, ido)) -> ido in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in - let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in - let tac = TacML (Loc.ghost, entry, List.map map ids) in + let map id = Reference (Misctypes.ArgVar (Loc.tag id)) in + let tac = TacML (Loc.tag (entry, List.map map ids)) in add_glob_tactic_notation false ~level prods true ids tac in List.iteri iter (List.rev prods); @@ -401,7 +401,7 @@ let create_ltac_quotation name cast (e, l) = entry), Atoken (CLexer.terminal ")")) in - let action _ v _ _ _ loc = cast (loc, v) in + let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram]) @@ -427,7 +427,7 @@ let register_ltac local tacl = let kn = Lib.make_kn id in let id_pp = pr_id id in let () = if is_defined_tac kn then - CErrors.user_err ~loc + CErrors.user_err ?loc (str "There is already an Ltac named " ++ id_pp ++ str".") in let is_shadowed = @@ -444,7 +444,7 @@ let register_ltac local tacl = let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> - CErrors.user_err ~loc + CErrors.user_err ?loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") in UpdateTac kn, body @@ -502,7 +502,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg n = spc () ++ pr_name n in + let pr_ltac_fun_arg n = spc () ++ Name.print n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 069504473..07aa7ad82 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of ('a * Names.Id.t option) Loc.located type raw_argument = string * string option (** An argument type as provided in Tactic notations, i.e. a string like diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index e3c2b4ad5..efb7e780d 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -24,7 +24,7 @@ let register_alias key tac = let interp_alias key = try KNmap.find key !alias_map - with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) + with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key ++ str ".") let check_alias key = KNmap.mem key !alias_map diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 8aefe7605..b78dc3742 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -141,10 +141,10 @@ type 'a gen_atomic_tactic_expr = | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of - bool * 'tacexpr option option * + evars_flag * bool * 'tacexpr option option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list - | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * + | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * intro_pattern_naming_expr located option (* Derived basic tactics *) @@ -184,8 +184,7 @@ type 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref - | TacCall of Loc.t * 'ref * - 'a gen_tactic_arg list + | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located | TacFreshId of string or_var list | Tacexp of 'tacexpr | TacPretype of 'trm @@ -207,7 +206,7 @@ constraint 'a = < 'r : ltac refs, 'n : idents, 'l : levels *) and 'a gen_tactic_expr = - | TacAtom of Loc.t * 'a gen_atomic_tactic_expr + | TacAtom of ('a gen_atomic_tactic_expr) Loc.located | TacThen of 'a gen_tactic_expr * 'a gen_tactic_expr @@ -266,9 +265,9 @@ and 'a gen_tactic_expr = | TacArg of 'a gen_tactic_arg located | TacSelect of goal_selector * 'a gen_tactic_expr (* For ML extensions *) - | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list + | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list + | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located constraint 'a = < term:'t; @@ -389,7 +388,7 @@ type ltac_call_kind = | LtacVarCall of Id.t * glob_tactic_expr | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map -type ltac_trace = (Loc.t * ltac_call_kind) list +type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 75227def0..d201cf949 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.") @@ -41,13 +39,12 @@ let error_tactic_expected ?loc = type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; (* ltac variables and the subset of vars introduced by Intro/Let/... *) - genv : Environ.env } - -let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; genv = Environ.empty_env } + genv : Environ.env; + extra : Genintern.Store.t; +} -let make_empty_glob_sign () = - { fully_empty_glob_sign with genv = Global.env () } +let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env +let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) (* We have identifier <| global_reference <| constr *) @@ -74,16 +71,16 @@ let intern_name l ist = function let strict_check = ref false -let adjust_loc loc = if !strict_check then dloc else loc +let adjust_loc loc = if !strict_check then None else loc (* Globalize a name which must be bound -- actually just check it is bound *) let intern_hyp ist (loc,id as locid) = if not !strict_check then locid else if find_ident id ist then - (dloc,id) + Loc.tag id else - Pretype_errors.error_var_not_found ~loc id + Pretype_errors.error_var_not_found ?loc id let intern_or_var f ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) @@ -110,19 +107,19 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - GVar (dloc,id), Some (CRef (r,None)) + (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - GVar (dloc,id), if strict then None else Some (CRef (r,None)) + (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in - GRef (loc,locate_global_with_alias lqid,None), - if strict then None else Some (CRef (r,None)) + CAst.make @@ GRef (locate_global_with_alias lqid,None), + if strict then None else Some (CAst.make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - TacCall (loc,ArgArg (loc,locate_tactic qid),[]) + TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) @@ -192,15 +189,16 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { Constrintern.ltac_vars = lfun; ltac_bound = Id.Set.empty; + ltac_extra = extra; } in let c' = - warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c + warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c in (c',if !strict_check then None else Some c) @@ -208,8 +206,8 @@ let intern_constr = intern_constr_gen false false let intern_type = intern_constr_gen false true (* Globalize bindings *) -let intern_binding ist (loc,b,c) = - (loc,intern_binding_name ist b,intern_constr ist c) +let intern_binding ist (loc,(b,c)) = + (loc,(intern_binding_name ist b,intern_constr ist c)) let intern_bindings ist = function | NoBindings -> NoBindings @@ -254,7 +252,7 @@ and intern_or_and_intro_pattern lf ist = function let intern_or_and_intro_pattern_loc lf ist = function | ArgVar (_,id) as x -> if find_var id ist then x - else error "Disjunctive/conjunctive introduction pattern expected." + else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) let intern_intro_pattern_naming_loc lf ist (loc,pat) = @@ -267,8 +265,8 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - match intern_constr ist (CRef (Ident (dloc,id), None)) with - | GVar (loc,id),_ -> clear,ElimOnIdent (loc,id) + match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with + | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else clear,ElimOnIdent (loc,id) @@ -287,9 +285,9 @@ let intern_evaluable_global_reference ist r = let intern_evaluable_reference_or_by_notation ist = function | AN r -> intern_evaluable_global_reference ist r - | ByNotation (loc,ntn,sc) -> + | ByNotation (loc,(ntn,sc)) -> evaluable_of_global_reference ist.genv - (Notation.interp_notation_as_global_reference loc + (Notation.interp_notation_as_global_reference ?loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) @@ -313,6 +311,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let ltacvars = { Constrintern.ltac_vars = ltacvars; ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; } in let metas,pat = Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars pc @@ -344,12 +343,16 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let r = match r with | AN r -> r | _ -> 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 sign = { + Constrintern.ltac_vars = ist.ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in let c = Constrintern.interp_reference sign r in - match c with - | GRef (_,r,None) -> + match c.CAst.v with + | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) - | GVar (_,id) -> + | GVar id -> let r = evaluable_of_global_reference ist.genv (VarRef id) in Inl (ArgArg (r,None)) | _ -> @@ -357,7 +360,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = Inr (bound_names,(c,None),dummy_pat) in (l, match p with | Inl r -> interp_ref r - | Inr (CAppExpl(_,(None,r,None),[])) -> + | Inr { CAst.v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> @@ -368,13 +371,13 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let dump_glob_red_expr = function | Unfold occs -> List.iter (fun (_, r) -> try - Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) occs | Cbv grf | Lazy grf -> List.iter (fun r -> try - Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) grf.rConst | _ -> () @@ -455,7 +458,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 @@ -486,17 +489,17 @@ let rec intern_atomic lf ist x = | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) - | TacAssert (b,otac,ipat,c) -> - TacAssert (b,Option.map (Option.map (intern_pure_tactic ist)) otac, + | TacAssert (ev,b,otac,ipat,c) -> + TacAssert (ev,b,Option.map (Option.map (intern_pure_tactic ist)) otac, Option.map (intern_intro_pattern lf ist) ipat, intern_constr_gen false (not (Option.is_empty otac)) ist c) | TacGeneralize cl -> TacGeneralize (List.map (fun (c,na) -> intern_constr_with_occurrences ist c, intern_name lf ist na) cl) - | TacLetTac (na,c,cls,b,eqpat) -> + | TacLetTac (ev,na,c,cls,b,eqpat) -> let na = intern_name lf ist na in - TacLetTac (na,intern_constr ist c, + TacLetTac (ev,na,intern_constr ist c, (clause_app (intern_hyp_location ist) cls),b, (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat)) @@ -546,7 +549,7 @@ and intern_tactic_seq onlytac ist = function | TacAtom (loc,t) -> let lf = ref ist.ltacvars in let t = intern_atomic lf ist t in - !lf, TacAtom (adjust_loc loc, t) + !lf, TacAtom (Loc.tag ?loc:(adjust_loc loc) t) | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun) | TacLetIn (isrec,l,u) -> let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in @@ -620,12 +623,12 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac) (* For extensions *) - | TacAlias (loc,s,l) -> + | TacAlias (loc,(s,l)) -> let l = List.map (intern_tacarg !strict_check false ist) l in - ist.ltacvars, TacAlias (loc,s,l) - | TacML (loc,opn,l) -> + ist.ltacvars, TacAlias (Loc.tag ?loc (s,l)) + | TacML (loc,(opn,l)) -> let _ignore = Tacenv.interp_ml_tactic opn in - ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l) + ist.ltacvars, TacML (loc, (opn,List.map (intern_tacarg !strict_check false ist) l)) and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with @@ -633,7 +636,7 @@ and intern_tactic_as_arg loc onlytac ist a = | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> - if onlytac then error_tactic_expected ~loc else TacArg (loc,a) + if onlytac then error_tactic_expected ?loc else TacArg (loc,a) and intern_tactic_or_tacarg ist = intern_tactic false ist @@ -646,11 +649,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 @@ -708,15 +711,14 @@ let glob_tactic_env l env x = let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check - (intern_pure_tactic - { ltacvars; genv = env }) + (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars }) x let split_ltac_fun = function | TacFun (l,t) -> (l,t) | t -> ([],t) -let pr_ltac_fun_arg n = spc () ++ pr_name n +let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 71ca354fa..8ad52ca02 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -18,7 +18,9 @@ open Misctypes type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; - genv : Environ.env } + genv : Environ.env; + extra : Genintern.Store.t; +} val fully_empty_glob_sign : glob_sign diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b8c021f18..2014f2aff 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -200,8 +200,6 @@ end let print_top_val env v = Pptactic.pr_value Pptactic.ltop v -let dloc = Loc.ghost - let catching_error call_trace fail (e, info) = let inner_trace = Option.default [] (Exninfo.get info ltac_trace_info) @@ -314,7 +312,7 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = let v = Value.normalize v in - let fail () = user_err ~loc + let fail () = user_err ?loc (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") in let v = Value.normalize v in @@ -325,7 +323,7 @@ let coerce_to_tactic loc id v = | _ -> fail () else fail () -let intro_pattern_of_ident id = (Loc.ghost, IntroNaming (IntroIdentifier id)) +let intro_pattern_of_ident id = (Loc.tag @@ IntroNaming (IntroIdentifier id)) let value_of_ident id = in_gen (topwit wit_intro_pattern) (intro_pattern_of_ident id) @@ -369,22 +367,22 @@ let debugging_exception_step ist signal_anomaly e pp = debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) -let error_ltac_variable loc id env v s = - user_err ~loc (str "Ltac variable " ++ pr_id id ++ +let error_ltac_variable ?loc id env v s = + user_err ?loc (str "Ltac variable " ++ pr_id id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") (* Raise Not_found if not in interpretation sign *) let try_interp_ltac_var coerce ist env (loc,id) = let v = Id.Map.find id ist.lfun in - try coerce v with CannotCoerceTo s -> error_ltac_variable loc id env v s + try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid - with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") + with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.") let interp_ident ist env sigma id = - try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (dloc,id) + try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> id (* Interprets an optional identifier, bound or fresh *) @@ -403,7 +401,7 @@ let interp_intro_pattern_naming_var loc ist env sigma id = let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> - user_err ~loc:(fst locid) ~hdr:"interp_int" + user_err ?loc:(fst locid) ~hdr:"interp_int" (str "Unbound variable " ++ pr_id (snd locid) ++ str".") let interp_int_or_var ist = function @@ -426,7 +424,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) @@ -442,7 +440,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found ~loc (qualid_of_ident id) + with Not_found -> error_global_not_found ?loc (qualid_of_ident id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -458,14 +456,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found ~loc (qualid_of_ident id) + | _ -> error_global_not_found ?loc (qualid_of_ident id) end | ArgArg (r,None) -> r | ArgVar (loc, id) -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found ~loc (qualid_of_ident id) + with Not_found -> error_global_not_found ?loc (qualid_of_ident id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -524,7 +522,7 @@ let extract_ids ids lfun = if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu - else accu @ intropattern_ids (dloc, ipat) + else accu @ intropattern_ids (Loc.tag ipat) else accu in Id.Map.fold fold lfun [] @@ -534,7 +532,7 @@ let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = let extract_ident ist env sigma id = try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma) - ist (Some (env,sigma)) (dloc,id) + ist (Some (env,sigma)) (Loc.tag id) with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with @@ -587,10 +585,11 @@ let interp_uconstr ist env sigma = function let ltacvars = { Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); ltac_bound = Id.Map.domain ist.lfun; + ltac_extra = Genintern.Store.empty; } in { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } -let interp_gen kind ist allow_patvar flags env sigma (c,ce) = +let interp_gen kind ist pattern_mode flags env sigma (c,ce) = let constrvars = extract_ltac_constr_context ist env sigma in let vars = { Pretyping.ltac_constrs = constrvars.typed; @@ -614,10 +613,11 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let ltacvars = { ltac_vars = constr_context; ltac_bound = Id.Map.domain ist.lfun; + ltac_extra = Genintern.Store.empty; } in let kind_for_intern = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in - intern_gen kind_for_intern ~allow_patvar ~ltacvars env c + intern_gen kind_for_intern ~pattern_mode ~ltacvars env c in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do @@ -672,10 +672,7 @@ let pure_open_constr_flags = { expand_evars = false } (* Interprets an open constr *) -let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c = - let flags = - if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags () - else open_constr_use_classes_flags () in +let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c = interp_gen expected_type ist false flags env sigma c let interp_pure_open_constr ist = @@ -692,7 +689,7 @@ let interp_typed_pattern ist env sigma (_,c,_) = let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with - | GVar (_,id), _ -> + | { CAst.v = GVar id }, _ -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -734,7 +731,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) with Not_found -> - error_global_not_found ~loc (qualid_of_ident id)) + error_global_not_found ?loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -792,7 +789,7 @@ let interp_may_eval f ist env sigma = function !evdref , c with | Not_found -> - user_err ~loc ~hdr:"interp_may_eval" + user_err ?loc ~hdr:"interp_may_eval" (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in @@ -934,7 +931,7 @@ and interp_or_and_intro_pattern ist env sigma = function and interp_intro_pattern_list_as_list ist env sigma = function | [loc,IntroNaming (IntroIdentifier id)] as l -> - (try sigma, coerce_to_intro_pattern_list loc env sigma (Id.Map.find id ist.lfun) + (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> List.fold_map (interp_intro_pattern ist env) sigma l) | l -> List.fold_map (interp_intro_pattern ist env) sigma l @@ -949,7 +946,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> - user_err ~loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) + user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) | Some (ArgArg (loc,l)) -> let sigma,l = interp_or_and_intro_pattern ist env sigma l in sigma, Some (loc,l) @@ -970,19 +967,19 @@ let interp_binding_name ist sigma = function (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(dloc,id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,id) + (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> NamedHyp id -let interp_binding ist env sigma (loc,b,c) = +let interp_binding ist env sigma (loc,(b,c)) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,interp_binding_name ist sigma b,c) + sigma, (loc,(interp_binding_name ist sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -996,7 +993,7 @@ let interp_bindings ist env sigma = function let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in - let sigma, c = interp_open_constr ist env sigma c in + let sigma, c = interp_constr ist env sigma c in sigma, (c,bl) let interp_open_constr_with_bindings ist env sigma (c,bl) = @@ -1005,14 +1002,14 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = sigma, (c, bl) let loc_of_bindings = function -| NoBindings -> Loc.ghost +| NoBindings -> None | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) -| ExplicitBindings l -> pi1 (List.last l) +| ExplicitBindings l -> fst (List.last l) let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in - let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in + let loc = Loc.merge_opt loc1 loc2 in let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in @@ -1025,12 +1022,12 @@ let interp_destruction_arg ist gl arg = | keep,ElimOnConstr c -> keep,ElimOnConstr { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_constr_with_bindings ist env sigma c in + let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in Sigma.Unsafe.of_pair (c, sigma) } | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> - let error () = user_err ~loc + let error () = user_err ?loc (strbrk "Cannot coerce " ++ pr_id id ++ strbrk " neither to a quantified hypothesis nor to a term.") in @@ -1041,7 +1038,7 @@ let interp_destruction_arg ist gl arg = (keep, ElimOnConstr { delayed = begin fun env sigma -> try Sigma.here (constr_of_id env id', NoBindings) sigma with Not_found -> - user_err ~loc ~hdr:"interp_destruction_arg" ( + user_err ?loc ~hdr:"interp_destruction_arg" ( pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") end }) in @@ -1067,7 +1064,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else - let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in + let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in @@ -1116,11 +1113,11 @@ let cons_and_check_name id l = let rec read_match_goal_hyps lfun ist env sigma lidh = function | (Hyp ((loc,na) as locna,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Hyp (locna,read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | (Def ((loc,na) as locna,mv,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | [] -> [] @@ -1250,7 +1247,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with eval_tactic ist tac | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) - | TacAlias (loc,s,l) -> + | TacAlias (loc,(s,l)) -> let (ids, body) = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in @@ -1281,8 +1278,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with in Ftactic.run tac (fun () -> Proofview.tclUNIT ()) - | TacML (loc,opn,l) -> - push_trace (loc,LtacMLCall tac) ist >>= fun trace -> + | TacML (loc,(opn,l)) -> + push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist >>= fun trace -> let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in @@ -1301,7 +1298,7 @@ and force_vrec ist v : Val.t Ftactic.t = | v -> Ftactic.return (of_tacvalue v) else Ftactic.return v -and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = +and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = match r with | ArgVar (loc,id) -> let v = @@ -1315,7 +1312,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = end | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in - let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in + let loc_info = (Option.default loc loc',LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in push_trace loc_info ist >>= fun trace -> let extra = TacStore.set extra f_trace trace in @@ -1326,7 +1323,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = and interp_tacarg ist arg : Val.t Ftactic.t = match arg with | TacGeneric arg -> interp_genarg ist arg - | Reference r -> interp_ltac_reference dloc false ist r + | Reference r -> interp_ltac_reference false ist r | ConstrMayEval c -> Ftactic.s_enter { s_enter = begin fun gl -> let sigma = project gl in @@ -1334,17 +1331,17 @@ and interp_tacarg ist arg : Val.t Ftactic.t = let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) end } - | TacCall (loc,r,[]) -> - interp_ltac_reference loc true ist r - | TacCall (loc,f,l) -> + | TacCall (loc,(r,[])) -> + interp_ltac_reference true ist r + | TacCall (loc,(f,l)) -> let (>>=) = Ftactic.bind in - interp_ltac_reference loc true ist f >>= fun fv -> + interp_ltac_reference true ist f >>= fun fv -> Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> interp_app loc ist fv largs | TacFreshId l -> Ftactic.enter { enter = begin fun gl -> let id = interp_fresh_id ist (pf_env gl) (project gl) l in - Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) + Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id))) end } | TacPretype c -> Ftactic.s_enter { s_enter = begin fun gl -> @@ -1423,7 +1420,7 @@ and tactic_of_value ist vle = (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum pr_name vars ++ Pp.str ".") + pr_enum Name.print vars ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in @@ -1435,7 +1432,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 @@ -1678,8 +1675,8 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let sigma, cb = interp_constr_with_bindings ist env sigma cb in - let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in let named_tac = let tac = Tactics.elim ev keep cb cbo in name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac @@ -1690,7 +1687,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let sigma, cb = interp_constr_with_bindings ist env sigma cb in + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in let named_tac = let tac = Tactics.general_case_analysis ev keep cb in name_atomic ~env (TacCase(ev,(keep,cb))) tac @@ -1727,18 +1724,21 @@ and interp_atomic ist tac : unit Proofview.tactic = Sigma.Unsafe.of_pair (tac, sigma) end } end - | TacAssert (b,t,ipat,c) -> + | TacAssert (ev,b,t,ipat,c) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let (sigma,c) = - (if Option.is_empty t then interp_constr else interp_type) ist env sigma c + let (sigma,c) = + let expected_type = + if Option.is_empty t then WithoutTypeConstraint else IsType in + let flags = open_constr_use_classes_flags () in + interp_open_constr ~expected_type ~flags ist env sigma c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (Option.map (interp_tactic ist)) t in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES ev (name_atomic ~env - (TacAssert(b,Option.map (Option.map ignore) t,ipat,c)) + (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma end } | TacGeneralize cl -> @@ -1751,36 +1751,37 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacGeneralize cl) (Tactics.generalize_gen cl)) sigma end } - | TacLetTac (na,c,clp,b,eqpat) -> + | TacLetTac (ev,na,c,clp,b,eqpat) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let clp = interp_clause ist env sigma clp in let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in - if Locusops.is_nowhere clp then + if Locusops.is_nowhere clp (* typically "pose" *) then (* We try to fully-typecheck the term *) - let (sigma,c_interp) = interp_constr ist env sigma c in + let flags = open_constr_use_classes_flags () in + let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in let let_tac b na c cl eqpat = - let id = Option.default (Loc.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 let na = interp_name ist env sigma na in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES ev (name_atomic ~env - (TacLetTac(na,c_interp,clp,b,eqpat)) + (TacLetTac(ev,na,c_interp,clp,b,eqpat)) (let_tac b na c_interp clp eqpat)) sigma 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 + Tactics.letin_pat_tac ev with_eq na c cl in let (sigma',c) = interp_pure_open_constr ist env sigma c in name_atomic ~env - (TacLetTac(na,c,clp,b,eqpat)) - (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) + (TacLetTac(ev,na,c,clp,b,eqpat)) + (Tacticals.New.tclWITHHOLES ev (let_pat_tac b (interp_name ist env sigma na) (sigma,c) clp eqpat) sigma') end } @@ -1807,7 +1808,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let l,lp = List.split l in let sigma,el = - Option.fold_map (interp_constr_with_bindings ist env) sigma el in + Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in let tac = name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) (Tactics.induction_destruct isrec ev (l,el)) @@ -1966,8 +1967,7 @@ let interp_tac_gen lfun avoid_ids debug t = let ist = { lfun = lfun; extra = extra } in let ltacvars = Id.Map.domain lfun in interp_tactic ist - (intern_pure_tactic { - ltacvars; genv = env } t) + (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -1976,7 +1976,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = let hide_interp env = - let ist = { ltacvars = Id.Set.empty; genv = env } in + let ist = Genintern.empty_glob_sign env in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with @@ -2045,6 +2045,11 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm Sigma.Unsafe.of_pair (c, sigma) } +let interp_open_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> + let (sigma, c) = interp_open_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in + Sigma.Unsafe.of_pair (c, sigma) + } + let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) end } @@ -2067,6 +2072,7 @@ let () = register_interp0 wit_open_constr (lifts interp_open_constr); register_interp0 wit_bindings interp_bindings'; register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; + register_interp0 wit_open_constr_with_bindings interp_open_constr_with_bindings'; register_interp0 wit_destruction_arg interp_destruction_arg'; () @@ -2099,17 +2105,13 @@ let interp_redexp env sigma r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let eval ty env sigma lfun arg = + let eval lfun env sigma ty tac = let ist = { lfun = lfun; extra = TacStore.empty; } in - if Genarg.has_type arg (glbwit wit_tactic) then - let tac = Genarg.out_gen (glbwit wit_tactic) arg in - let tac = interp_tactic ist tac in - let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in - (EConstr.of_constr c, sigma) - else - failwith "not a tactic" + let tac = interp_tactic ist tac in + let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in + (EConstr.of_constr c, sigma) in - Hook.set Pretyping.genarg_interp_hook eval + Pretyping.register_constr_interp0 wit_tactic eval (** Used in tactic extension **) @@ -2125,7 +2127,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 @@ -2138,8 +2140,7 @@ let vernac_debug b = let _ = let open Goptions in declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Ltac debug"; optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); @@ -2148,8 +2149,7 @@ let _ = let _ = let open Goptions in declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Ltac debug"; optkey = ["Debug";"Ltac"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 494f36a95..2ec45312e 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -110,7 +110,7 @@ val interp_int : interp_sign -> Id.t Loc.located -> int val interp_int_or_var : interp_sign -> int or_var -> int -val error_ltac_variable : Loc.t -> Id.t -> +val error_ltac_variable : ?loc:Loc.t -> Id.t -> (Environ.env * Evd.evar_map) option -> value -> string -> 'a (** Transforms a constr-expecting tactic into a tactic finding its arguments in diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fe3a9f3b2..2858df313 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -14,7 +14,6 @@ open Stdarg open Tacarg open Misctypes open Globnames -open Term open Genredexpr open Patternops @@ -32,8 +31,8 @@ let subst_glob_constr_and_expr subst (c, e) = let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) -let subst_binding subst (loc,b,c) = - (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c) +let subst_binding subst (loc,(b,c)) = + (loc,(subst_quantified_hypothesis subst b,subst_glob_constr subst c)) let subst_bindings subst = function | NoBindings -> NoBindings @@ -77,9 +76,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)) @@ -93,7 +90,7 @@ open Printer let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in - if not (eq_constr (Universes.constr_of_global ref') t') then + if not (is_global ref' t') then Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; @@ -148,13 +145,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) - | TacAssert (b,otac,na,c) -> - TacAssert (b,Option.map (Option.map (subst_tactic subst)) otac,na, + | TacAssert (ev,b,otac,na,c) -> + TacAssert (ev,b,Option.map (Option.map (subst_tactic subst)) otac,na, subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacLetTac (id,c,clp,b,eqpat) -> - TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) + | TacLetTac (ev,id,c,clp,b,eqpat) -> + TacLetTac (ev,id,subst_glob_constr subst c,clp,b,eqpat) (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> @@ -182,7 +179,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 +226,22 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) | TacComplete tac -> TacComplete (subst_tactic subst tac) - | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a) + | TacArg (_,a) -> TacArg (Loc.tag @@ subst_tacarg subst a) | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac) (* For extensions *) - | TacAlias (_,s,l) -> + | TacAlias (_,(s,l)) -> let s = subst_kn subst s in - TacAlias (dloc,s,List.map (subst_tacarg subst) l) - | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l) + TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l)) + | TacML (loc,(opn,l)) -> TacML (loc, (opn,List.map (subst_tacarg subst) l)) and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) - | TacCall (_loc,f,l) -> - TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) + | TacCall (loc,(f,l)) -> + TacCall (Loc.tag ?loc (subst_reference subst f, List.map (subst_tacarg subst) l)) | TacFreshId _ as x -> x | TacPretype c -> TacPretype (subst_glob_constr subst c) | TacNumgoals -> TacNumgoals diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index dac15ff79..294cba4d7 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -91,8 +91,7 @@ open Goptions let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Ltac batch debug"; optkey = ["Ltac";"Batch";"Debug"]; optread = (fun () -> !batch); @@ -366,7 +365,7 @@ let explain_ltac_call_trace last trace loc = Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.ghost,te))) + (Tacexpr.TacAtom (Loc.tag te))) | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then @@ -401,16 +400,16 @@ let skip_extensions trace = | [] -> [] in List.rev (aux (List.rev trace)) -let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 +let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2 -let extract_ltac_trace trace eloc = +let extract_ltac_trace ?loc trace = let trace = skip_extensions trace in - let (loc,c),tail = List.sep_last trace in + let (tloc,c),tail = List.sep_last trace in if is_defined_ltac trace then (* We entered a user-defined tactic, we display the trace with location of the call *) - let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in - Some msg, if finer_loc eloc loc then eloc else loc + let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in + (if finer_loc loc tloc then loc else tloc), Some msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -418,21 +417,21 @@ let extract_ltac_trace trace eloc = (* trace is with innermost call coming first *) let rec aux best_loc = function | (loc,_)::tail -> - if Loc.is_ghost best_loc || - not (Loc.is_ghost loc) && finer_loc loc best_loc + if Option.is_empty best_loc || + not (Option.is_empty loc) && finer_loc loc best_loc then aux loc tail else aux best_loc tail | [] -> best_loc in - aux eloc trace in - None, best_loc + aux loc trace in + best_loc, None let get_ltac_trace (_, info) = let ltac_trace = Exninfo.get info ltac_trace_info in - let loc = Option.default Loc.ghost (Loc.get_loc info) in + let loc = Loc.get_loc info in match ltac_trace with | None -> None - | Some trace -> Some (extract_ltac_trace trace loc) + | Some trace -> Some (extract_ltac_trace ?loc trace) let () = ExplainErr.register_additional_error_info get_ltac_trace diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 0b4d35a22..ac35464c4 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -77,4 +77,4 @@ val db_breakpoint : debug_info -> Id.t Loc.located message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : - Tacexpr.ltac_trace -> Loc.t -> Pp.std_ppcmds option * Loc.t + ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4de2081cf..d8e21d81d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -70,8 +70,7 @@ let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2 open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "unfolding of not in intuition"; optkey = ["Intuition";"Negation";"Unfolding"]; optread = (fun () -> !negation_unfolding); @@ -79,8 +78,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "unfolding of iff in intuition"; optkey = ["Intuition";"Iff";"Unfolding"]; optread = (fun () -> !iff_unfolding); @@ -88,7 +86,6 @@ let _ = (** Base tactics *) -let loc = Loc.ghost let idtac = Proofview.tclUNIT () let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ())) @@ -206,7 +203,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] @@ -223,9 +220,7 @@ let apply_nnpp _ ist = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> try - let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in - let nnpp = EConstr.of_constr nnpp in - apply nnpp + Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply with Not_found -> tclFAIL 0 (Pp.mt ()) end @@ -259,11 +254,11 @@ let tauto_power_flags = { } let with_flags flags _ ist = - let f = (loc, Id.of_string "f") in - let x = (loc, Id.of_string "x") in + let f = (Loc.tag @@ Id.of_string "f") in + let x = (Loc.tag @@ Id.of_string "x") in let arg = Val.Dyn (tag_tauto_flags, flags) in let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in - eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)]))) + eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in @@ -271,7 +266,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 |