diff options
Diffstat (limited to 'plugins/ltac')
45 files changed, 704 insertions, 462 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 7d2c4d0825..931633e1a8 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -239,12 +241,20 @@ END (** Simple induction / destruct *) +let simple_induct h = + Tacticals.New.tclTHEN (Tactics.intros_until h) + (Tacticals.New.onLastHyp Tactics.simplest_elim) + TACTIC EXTEND simple_induction - [ "simple" "induction" quantified_hypothesis(h) ] -> [ Tactics.simple_induct h ] + [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ] END +let simple_destruct h = + Tacticals.New.tclTHEN (Tactics.intros_until h) + (Tacticals.New.onLastHyp Tactics.simplest_case) + TACTIC EXTEND simple_destruct - [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ] + [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ] END (** Double induction *) @@ -346,7 +356,7 @@ 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 varn n = Reference (ArgVar (CAst.make (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]))); diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 1f628803a3..9382f567b4 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli index 122aecd75b..b6cfc38260 100644 --- a/plugins/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 4c6d3c2d36..702b830342 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -81,7 +83,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x - | ArgVar (loc, id) -> Id.print id + | ArgVar { CAst.loc = loc; v=id } -> Id.print id let occurrences_of = function | [] -> NoOccurrences @@ -102,7 +104,7 @@ let int_list_of_VList v = match Value.to_list v with let interp_occs ist gl l = match l with | ArgArg x -> x - | ArgVar (_,id as locid) -> + | ArgVar ({ CAst.v = id } as locid) -> (try int_list_of_VList (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) let interp_occs ist gl l = @@ -188,7 +190,7 @@ END type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = Id.t Loc.located gen_place +type loc_place = lident gen_place type place = Id.t gen_place let pr_gen_place pr_id = function @@ -199,7 +201,7 @@ let pr_gen_place pr_id = function | HypLocation (id,InHypValueOnly) -> str "in (Value of " ++ pr_id id ++ str ")" -let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id) +let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print let pr_hloc = pr_loc_place () () () @@ -228,11 +230,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Loc.tag id),InHyp) ] + [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypTypeOnly) ] + [ HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypValueOnly) ] + [ HypLocation ((CAst.make id),InHypValueOnly) ] END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 00668ddc7d..e5a4f090ed 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Tacexpr @@ -50,7 +52,7 @@ val lglob : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location -type loc_place = Id.t Loc.located gen_place +type loc_place = lident gen_place type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type @@ -77,6 +79,6 @@ val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type val wit_in_clause : - (Id.t Loc.located Locus.clause_expr, - Id.t Loc.located Locus.clause_expr, - Id.t Locus.clause_expr) Genarg.genarg_type + (lident Locus.clause_expr, + lident Locus.clause_expr, + Id.t Locus.clause_expr) Genarg.genarg_type diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 286f9d95d5..7d43f1986f 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -71,7 +73,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (Loc.tag id) + | NamedHyp id -> None,ElimOnIdent (CAst.make 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 @@ -253,6 +255,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = let sigma = Evd.from_env env in let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in + let c = EConstr.to_constr sigma c in let ctx = let ctx = UState.context_set ctx in if poly then ctx @@ -554,6 +557,7 @@ let add_transitivity_lemma left lem = let env = Global.env () in let sigma = Evd.from_env env in let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in + let lem' = EConstr.to_constr sigma lem' in add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) @@ -611,8 +615,10 @@ END VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> - [ let tc,ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in - let tb,ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in + [ let tc,_ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in + let tb,_ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in + let tc = EConstr.to_constr Evd.empty tc in + let tb = EConstr.to_constr Evd.empty tb in Global.register f tc tb ] END @@ -705,7 +711,6 @@ let hResolve id c occ t = 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 let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -973,6 +978,7 @@ TACTIC EXTEND unshelve | [ "unshelve" tactic1(t) ] -> [ Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) -> + let gls = List.map Proofview.with_empty_state gls in Proofview.Unsafe.tclGETGOALS >>= fun ogls -> Proofview.Unsafe.tclSETGOALS (gls @ ogls) ] diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index c423585e5e..7fb9a19a0c 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index f74d24db07..643f7e99f7 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 014433ac47..1c2f90b670 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Class_tactics diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index f705778fc0..2251a66204 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (************************************************************************) @@ -13,6 +15,7 @@ (************************************************************************) open Eqdecide +open Stdarg DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 9ef8195695..66268f9f9b 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) DECLARE PLUGIN "ltac_plugin" @@ -37,10 +39,10 @@ let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac let reference_to_id = function - | Libnames.Ident (loc, id) -> (loc, id) + | Libnames.Ident (loc, id) -> CAst.make ?loc id | Libnames.Qualid (loc,_) -> - CErrors.user_err ?loc - (str "This expression should be a simple identifier.") + CErrors.user_err ?loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -196,7 +198,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.tag ~loc:!@loc id) ] ] + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (CAst.make ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -225,12 +227,12 @@ GEXTEND Gram | l = ident -> Name.Name l ] ] ; let_clause: - [ [ (l,id) = identref; ":="; te = tactic_expr -> - ((l,Name id), arg_of_expr te) - | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr -> + [ [ idr = identref; ":="; te = tactic_expr -> + (CAst.map (fun id -> Name id) idr, arg_of_expr te) + | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr -> (na, arg_of_expr te) - | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - ((l,Name id), arg_of_expr (TacFun(args,te))) ] ] + | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; @@ -483,7 +485,7 @@ let pr_ltac_ref = Libnames.pr_reference let pr_tacdef_body tacdef_body = let id, redef, body = match tacdef_body with - | TacticDefinition ((_,id), body) -> Id.print id, false, body + | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body in let idl, body = @@ -504,7 +506,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function - | TacticDefinition ((_,r),_) -> r + | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (Ident (_,r),_) -> r | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index e251b10495..54e2ba960d 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 2459a09bc6..fbaa2e58f7 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Syntax for rewriting with strategies *) diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e68140828a..1b8a852d96 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -115,16 +117,16 @@ let mk_fix_tac (loc,id,bl,ann,ty) = match bl,ann with [([_],_,_)], None -> 1 | _, Some x -> - let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in - (try List.index Names.Name.equal (snd x) ids + let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in + (try List.index Names.Name.equal x.CAst.v ids with Not_found -> user_err Pp.(str "No such fix variable.")) | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl 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 + let _ = Option.map (fun { CAst.loc = aloc } -> + user_err ?loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in @@ -134,7 +136,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | NoBindings -> begin - try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c)) + try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v) with e when CErrors.noncritical e -> ElimOnConstr clbind end | _ -> ElimOnConstr clbind @@ -152,6 +154,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> + let id = CAst.(id.loc, id.v) in TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) @@ -161,7 +164,7 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc ?loc bll c = match bll with - | ((loc1,_)::_ as idl,bk,t) :: bll -> + | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll -> CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c @@ -169,7 +172,7 @@ let rec mkCLambdaN_simple_loc ?loc bll c = let mkCLambdaN_simple bl c = match bl with | [] -> c | h :: _ -> - let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in + let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in mkCLambdaN_simple_loc ?loc bl c let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) @@ -381,15 +384,20 @@ GEXTEND Gram ; hypident: [ [ id = id_or_meta -> - id,InHyp + let id : Misctypes.lident = id in + id,InHyp | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> - id,InHypTypeOnly + let id : Misctypes.lident = id in + id,InHypTypeOnly | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> - id,InHypValueOnly + let id : Misctypes.lident = id in + id,InHypValueOnly ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ] + [ [ (id,l)=hypident; occs=occs -> + let id : Misctypes.lident = id in + ((occs,id),l) ] ] ; in_clause: [ [ "*"; occs=occs -> @@ -433,7 +441,8 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) + [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ + CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; @@ -565,28 +574,34 @@ GEXTEND Gram 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; ":="; + | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - 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; ":="; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "assert c as id by tac" *) - | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - 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; ":"; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_colon; "("; lid = 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)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "enough c as id by tac" *) - | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - 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; ":"; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eenough"; test_lpar_id_colon; "("; lid = 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)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 2c1b1067ea..e9711268c2 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pcoq diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 048dcc8e92..699e231106 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -1,15 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Ltac parsing entries *) open Loc -open Names open Pcoq open Libnames open Constrexpr @@ -20,7 +21,7 @@ open Misctypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry -val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry +val hypident : (lident * Locus.hyp_location_flag) Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry @@ -29,8 +30,8 @@ val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry val int_or_var : int or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry -val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry -val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry +val in_clause : lident Locus.clause_expr Gram.entry +val clause_dft_concl : lident Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4f430b79e4..fbb70cca68 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -161,7 +163,7 @@ let string_of_genarg_arg (ArgumentType arg) = (keyword "eval" ++ brk (1,1) ++ pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++ keyword "in" ++ spc() ++ prc c) - | ConstrContext ((_,id),c) -> + | ConstrContext ({CAst.v=id},c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ str "[ " ++ prlc c ++ str " ]") @@ -364,7 +366,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_ltac_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id) + | ArgVar {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn @@ -404,7 +406,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_as_name = function | Anonymous -> mt () - | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id) + | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (CAst.make id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na @@ -496,12 +498,12 @@ let string_of_genarg_arg (ArgumentType arg) = 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 {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) | ElimOnAnonHyp n -> int n let pr_destruction_arg prc prlc (clear_flag,h) = pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h - + let pr_inversion_kind = function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" @@ -684,7 +686,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = @@ -692,10 +694,10 @@ let pr_goal_selector ~toplevel s = (nal,ty)::bll -> if n <= List.length nal then match List.chop (n-1) nal with - _, (_,Name id) :: _ -> id, (nal,ty)::bll - | bef, (loc,Anonymous) :: aft -> + _, {CAst.v=Name id} :: _ -> id, (nal,ty)::bll + | bef, {CAst.loc;v=Anonymous} :: aft -> let id = next_ident_away (Id.of_string"y") avoid in - id, ((bef@(loc,Name id)::aft, ty)::bll) + id, ((bef@(CAst.make ?loc @@ Name id)::aft, ty)::bll) | _ -> assert false else let (id,bll') = set_nth_name avoid (n-List.length nal) bll in @@ -705,7 +707,7 @@ let pr_goal_selector ~toplevel s = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln) + (fun ln na -> match na with { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln) ln nal) Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in @@ -1087,7 +1089,7 @@ let pr_goal_selector ~toplevel s = if Int.equal n 0 then (List.rev acc, (ty,None)) else match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> - strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b + strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty @@ -1158,7 +1160,7 @@ let pr_goal_selector ~toplevel s = if n=0 then (List.rev acc, EConstr.of_constr ty) else match Constr.kind ty with | Constr.Prod(na,a,b) -> - strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b + strip_ty (([CAst.make 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 @@ -1318,7 +1320,7 @@ let () = register_basic_print0 wit_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 wit_intro_pattern (lift (Miscprint.pr_intro_pattern pr_constr_expr)) @@ -1328,7 +1330,7 @@ let () = wit_clause_dft_concl (lift (pr_clauses (Some true) pr_lident)) (lift (pr_clauses (Some true) pr_lident)) - (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (CAst.make id)) c)) ; Genprint.register_print0 wit_constr diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index bda5774abf..7e6c6b20ee 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module implements pretty-printers for tactic_expr syntactic diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 1615465281..d22bd4967a 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Unicode diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index adedf7ee91..6a67aab5dc 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 7a75662be0..983e1578be 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Ltac profiling entrypoints *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index acd7a30c43..e0368153e5 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -1568,7 +1570,8 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in let gls = List.rev (Evd.fold_undefined fold undef []) in - match clause, prf with + let gls = List.map Proofview.with_empty_state gls in + match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ Refine.refine ~typecheck:true (fun h -> (h,p)); @@ -1773,7 +1776,7 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l) let declare_an_instance n s args = - (((Loc.tag @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), Explicit, CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), args)) @@ -1896,7 +1899,6 @@ let declare_projection n instance_id r = let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in - let m = EConstr.of_constr m in let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in let cstrs = @@ -1920,7 +1922,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m @@ -2006,7 +2008,7 @@ 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.tag @@ Name instance_id),None), Explicit, + (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 17e7244b39..1e3d4733b5 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 1bf9ea4c1d..6eb482b1c3 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Generic arguments based on Ltac. *) diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 6c4f3dd873..5347eda7d7 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Genarg diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index e5933de2a6..2c7ebb7458 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -14,6 +16,7 @@ open Misctypes open Genarg open Stdarg open Geninterp +open Pp exception CannotCoerceTo of string @@ -92,6 +95,38 @@ let to_option v = prj Val.typ_opt v let to_pair v = prj Val.typ_pair v +let cast_error wit v = + let pr_v = Pptactic.pr_value Pptactic.ltop v in + let Val.Dyn (tag, _) = v in + let tag = Val.pr tag in + CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag + ++ str " while type " ++ Val.pr wit ++ str " was expected.") + +let unbox wit v ans = match ans with +| None -> cast_error wit v +| Some x -> x + +let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with +| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v)) +| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v)) +| Val.Pair (tag1, tag2) -> + let (x, y) = unbox Val.typ_pair v (to_pair v) in + (prj tag1 x, prj tag2 y) +| Val.Base t -> + let Val.Dyn (t', x) = v in + match Val.eq t t' with + | None -> cast_error t v + | Some Refl -> x +let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with +| ExtraArg _ -> Geninterp.val_tag (topwit wit) +| ListArg t -> Val.List (tag_of_arg t) +| OptArg t -> Val.Opt (tag_of_arg t) +| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) + +let val_cast arg v = prj (tag_of_arg arg) v + +let cast (Topwit wit) v = val_cast wit v + end let is_variable env id = @@ -332,3 +367,46 @@ let coerce_to_int_or_var_list v = | Some l -> let map n = ArgArg (coerce_to_int n) in List.map map l + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +(* Values for interpretation *) +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = + let wit = Genarg.create_arg "tacvalue" in + let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in + wit + +let pr_argument_type arg = + let Val.Dyn (tag, _) = arg in + Val.pr tag + +(** TODO: unify printing of generic Ltac values in case of coercion failure. *) + +(* Displays a value *) +let pr_value env v = + let pr_with_env pr = + match env with + | Some (env,sigma) -> pr env sigma + | None -> str "a value of type" ++ spc () ++ pr_argument_type v in + let open Genprint in + match generic_val_print v with + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) + +let error_ltac_variable ?loc id env v s = + CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++ + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + strbrk "which cannot be coerced to " ++ str s ++ str".") diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index dce16b7333..1fa5e3c076 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -40,6 +42,7 @@ sig val to_list : t -> t list option val to_option : t -> t option option val to_pair : t -> (t * t) option + val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a end (** {5 Coercion functions} *) @@ -90,3 +93,21 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type + +val error_ltac_variable : ?loc:Loc.t -> Id.t -> + (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +val wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type + +val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 8112cc4008..566fc28733 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -374,7 +376,7 @@ let add_ml_tactic_notation name ~level prods = 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.tag id)) in + let map id = Reference (Misctypes.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in add_glob_tactic_notation false ~level prods true ids tac in @@ -431,11 +433,11 @@ let warn_unusable_identifier = let register_ltac local tacl = let map tactic_body = match tactic_body with - | Tacexpr.TacticDefinition ((loc,id), body) -> + | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) -> let kn = Lib.make_kn id in let id_pp = Id.print 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 = @@ -552,3 +554,138 @@ let () = AnyEntry Pltac.tactic_arg; ] in register_grammars_by_name "tactic" entries + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu -> + match tu with + | TUlist1 l -> Ulist1(untype_user_symbol l) + | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s) + | TUlist0 l -> Ulist0(untype_user_symbol l) + | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s) + | TUopt(o) -> Uopt(untype_user_symbol o) + | TUentry a -> Uentry (Genarg.ArgT.Any a) + | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i) + +let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list = + fun sign -> match sign with + | TyNil -> [] + | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' + | TyArg ((loc,(a,id)),sig') -> + TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg ((loc,a),sig') -> + TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + +let clause_of_ty_ml = function + | TyML (t,_) -> clause_of_sign t + +let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function + | TUentry a -> ExtraArg a + | TUentryl (a,l) -> ExtraArg a + | TUopt(o) -> OptArg (prj o) + | TUlist1 l -> ListArg (prj l) + | TUlist1sep (l,_) -> ListArg (prj l) + | TUlist0 l -> ListArg (prj l) + | TUlist0sep (l,_) -> ListArg (prj l) + +let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = + fun sign tac -> + match sign with + | TyNil -> + begin fun vals ist -> match vals with + | [] -> tac ist + | _ :: _ -> assert false + end + | TyIdent (s, sig') -> eval_sign sig' tac + | TyArg ((_loc,(a,id)), sig') -> + let f = eval_sign sig' in + begin fun tac vals ist -> match vals with + | [] -> assert false + | v :: vals -> + let v' = Taccoerce.Value.cast (topwit (prj a)) v in + f (tac v') vals ist + end tac + | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + +let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function + | TyML (t,tac) -> eval_sign t tac + +let is_constr_entry = function +| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr +| _ -> false + +let rec only_constr : type a. a ty_sig -> bool = function +| TyNil -> true +| TyIdent(_,_) -> false +| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false + +let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function +| TyNil -> [] +| TyIdent (_,s) -> mk_sign_vars s +| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s +| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s + +let dummy_id = Id.of_string "_" + +let lift_constr_tac_to_ml_tac vars tac = + let tac _ ist = Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let map = function + | Anonymous -> None + | Name id -> + let c = Id.Map.find id ist.Geninterp.lfun in + try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c) + with Taccoerce.CannotCoerceTo ty -> + Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty + in + let args = List.map_filter map vars in + tac args ist + end in + tac + +let tactic_extend plugin_name tacname ~level sign = + let open Tacexpr in + let ml_tactic_name = + { mltac_tactic = tacname; + mltac_plugin = plugin_name } + in + match sign with + | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s -> + (** The extension is only made of a name followed by constr entries: we do not + add any grammar nor printing rule and add it as a true Ltac definition. *) + (* + let patt = make_patt rem in + let vars = List.map make_var rem in + let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in + *) + let vars = mk_sign_vars s in + let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in + let tac = match s with + | TyNil -> eval ml_tac + (** Special handling of tactics without arguments: such tactics do not do + a Proofview.Goal.nf_enter to compute their arguments. It matters for some + whole-prof tactics like [shelve_unifiable]. *) + | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac) + in + (** Arguments are not passed directly to the ML tactic in the TacML node, + the ML tactic retrieves its arguments in the [ist] environment instead. + This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true false id body in + let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in + Mltop.declare_cache_obj obj plugin_name + | _ -> + let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in + Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); + Mltop.declare_cache_obj obj plugin_name diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index ab2c6b3073..3f804ee8d1 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Ltac toplevel command entries. *) @@ -65,3 +67,15 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.reference -> unit (** Display the absolute name of a tactic. *) + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 8c59a36fa6..d5ab2d690d 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 4ecc978fea..3af2f2a460 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index ccd555b615..6db808dd66 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Loc @@ -41,7 +43,7 @@ type goal_selector = Vernacexpr.goal_selector = type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = | ElimOnConstr of 'a - | ElimOnIdent of Id.t located + | ElimOnIdent of lident | ElimOnAnonHyp of int type 'a destruction_arg = @@ -85,8 +87,8 @@ type 'a match_pattern = (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = - | Hyp of Name.t located * 'a match_pattern - | Def of Name.t located * 'a match_pattern * 'a match_pattern + | Hyp of lname * 'a match_pattern + | Def of lname * 'a match_pattern * 'a match_pattern (* Type of a Match rule for Match Context and Match *) type ('a,'t) match_rule = @@ -254,7 +256,7 @@ and 'a gen_tactic_expr = | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Name.t located * 'a gen_tactic_arg) list * + (lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr | TacMatch of lazy_flag * 'a gen_tactic_expr * @@ -300,7 +302,7 @@ type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr type g_cst = evaluable_global_reference and_short_name or_var type g_ref = ltac_constant located or_var -type g_nam = Id.t located +type g_nam = lident type g_dispatch = < term:g_trm; @@ -328,7 +330,7 @@ type r_trm = constr_expr type r_pat = constr_pattern_expr type r_cst = reference or_by_notation type r_ref = reference -type r_nam = Id.t located +type r_nam = lident type r_lev = rlevel type r_dispatch = < @@ -357,7 +359,7 @@ type t_trm = EConstr.constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located -type t_nam = Id.t +type t_nam = Id.t type t_dispatch = < term:t_trm; @@ -391,5 +393,5 @@ type ltac_call_kind = 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 *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index ebffde441d..121075f728 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -1,17 +1,20 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pattern open Pp +open CErrors +open CAst +open Pattern open Genredexpr open Glob_term open Tacred -open CErrors open Util open Names open Libnames @@ -73,11 +76,11 @@ let strict_check = ref false 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) = +let intern_hyp ist ({loc;v=id} as locid) = if not !strict_check then locid else if find_ident id ist then - Loc.tag id + make id else Pretype_errors.error_var_not_found ?loc id @@ -89,7 +92,8 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n) let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist = function - | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) + | Ident (loc,id) when find_var id ist -> + ArgVar CAst.(make ?loc id) | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) @@ -99,7 +103,7 @@ let intern_ltac_variable ist = function | Ident (loc,id) -> if find_var id ist then (* A local variable of any type *) - ArgVar (loc,id) + ArgVar CAst.(make ?loc id) else raise Not_found | _ -> raise Not_found @@ -197,7 +201,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = ltac_extra = extra; } in let c' = - warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c + warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c in (c',if !strict_check then None else Some c) @@ -249,7 +253,7 @@ and intern_or_and_intro_pattern lf ist = function IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll) let intern_or_and_intro_pattern_loc lf ist = function - | ArgVar (_,id) as x -> + | ArgVar {v=id} as x -> if find_var id ist then x else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) @@ -261,18 +265,18 @@ let intern_intro_pattern_naming_loc lf ist (loc,pat) = let intern_destruction_arg ist = function | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c) | clear,ElimOnAnonHyp n as x -> x - | clear,ElimOnIdent (loc,id) -> + | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in match DAst.get c with - | GVar id -> clear,ElimOnIdent (c.CAst.loc,id) + | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) else - clear,ElimOnIdent (loc,id) + clear,ElimOnIdent CAst.(make ?loc id) let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id) + | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id) | _ -> None let intern_evaluable_global_reference ist r = @@ -292,9 +296,9 @@ let intern_evaluable_reference_or_by_notation ist = function (* Globalize a reduction expression *) let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id) + | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id) | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some (loc,id)) + ArgArg (EvalVarRef id, Some CAst.(make ?loc id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -314,7 +318,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = ltac_extra = ist.extra; } in let metas,pat = Constrintern.intern_constr_pattern - ist.genv ~as_type ~ltacvars pc + ist.genv Evd.(from_env ist.genv) ~as_type ~ltacvars pc in let (glob,_ as c) = intern_constr_gen true false ist pc in let bound_names = Glob_ops.bound_glob_vars glob in @@ -333,7 +337,7 @@ let intern_typed_pattern ist ~as_type ~ltacvars p = ltac_bound = Id.Set.empty; ltac_extra = ist.extra; } in - Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p + Constrintern.intern_constr_pattern ist.genv Evd.(from_env ist.genv) ~as_type ~ltacvars p else [], dummy_pat in let (glob,_ as c) = intern_constr_gen true false ist p in @@ -370,7 +374,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 { CAst.v = CAppExpl((None,r,None),[]) } -> + | Inr { v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> @@ -400,8 +404,8 @@ let intern_red_expr ist = function | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) | Simpl (f,o) -> - Simpl (intern_flag ist f, - Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) + Simpl (intern_flag ist f, + Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r @@ -438,7 +442,7 @@ let intern_pattern ist ?(as_type=false) ltacvars = function let intern_constr_may_eval ist = function | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c) | ConstrContext (locid,c) -> - ConstrContext (intern_hyp ist locid,intern_constr ist c) + ConstrContext (intern_hyp ist locid,intern_constr ist c) | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c) | ConstrTerm c -> ConstrTerm (intern_constr ist c) @@ -452,12 +456,12 @@ let opt_cons accu = function (* Reads the hypotheses of a "match goal" rule *) let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function - | (Hyp ((_,na) as locna,mp))::tl -> + | (Hyp ({v=na} as locna,mp))::tl -> let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in let lfun' = name_cons (opt_cons lfun ido) na in lfun', metas1@metas2, Hyp (locna,pat)::hyps - | (Def ((_,na) as locna,mv,mp))::tl -> + | (Def ({v=na} as locna,mv,mp))::tl -> let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in @@ -467,7 +471,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = - let fold accu ((loc, name), _) = + let fold accu ({loc;v=name}, _) = Nameops.Name.fold_right (fun id accu -> if Id.Set.mem id accu then user_err ?loc ~hdr:"glob_tactic" (str "This variable is bound several times.") @@ -813,7 +817,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - ((loc, Name id), c) :: accu + (CAst.make ?loc @@ Name id, c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index e3a4d5c798..fb32508cc9 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -47,7 +49,7 @@ val intern_constr_with_bindings : glob_sign -> constr_expr * constr_expr bindings -> glob_constr_and_expr * glob_constr_and_expr bindings -val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located +val intern_hyp : glob_sign -> lident -> lident (** Adds a globalization function for extra generic arguments *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f2720954d0..991afe9c60 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1,14 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constrintern open Patternops open Pp +open CAst open Genredexpr open Glob_term open Glob_ops @@ -76,9 +79,6 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) -let base_val_typ wit = - match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") - let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -90,11 +90,6 @@ let safe_msgnl s = type value = Val.t -(** Abstract application, to print ltac functions *) -type appl = - | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.KerName.t * Val.t list) list - (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with | UnnamedAppl -> UnnamedAppl @@ -118,19 +113,6 @@ let combine_appl appl1 appl2 = | UnnamedAppl,a | a,UnnamedAppl -> a | GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1) -(* Values for interpretation *) -type tacvalue = - | VFun of appl*ltac_trace * value Id.Map.t * - Name.t list * glob_tactic_expr - | VRec of value Id.Map.t ref * glob_tactic_expr - -let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - let wit = Genarg.create_arg "tacvalue" in - let () = register_val0 wit None in - let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in - wit - let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v @@ -166,39 +148,6 @@ module Value = struct let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in of_tacvalue closure - let cast_error wit v = - let pr_v = Pptactic.pr_value Pptactic.ltop v in - let Val.Dyn (tag, _) = v in - let tag = Val.pr tag in - user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag - ++ str " while type " ++ Val.pr wit ++ str " was expected.") - - let unbox wit v ans = match ans with - | None -> cast_error wit v - | Some x -> x - - let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with - | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v)) - | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v)) - | Val.Pair (tag1, tag2) -> - let (x, y) = unbox Val.typ_pair v (to_pair v) in - (prj tag1 x, prj tag2 y) - | Val.Base t -> - let Val.Dyn (t', x) = v in - match Val.eq t t' with - | None -> cast_error t v - | Some Refl -> x - - let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with - | ExtraArg _ -> val_tag wit - | ListArg t -> Val.List (tag_of_arg t) - | OptArg t -> Val.Opt (tag_of_arg t) - | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) - - let val_cast arg v = prj (tag_of_arg arg) v - - let cast (Topwit wit) v = val_cast wit v - end let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -230,21 +179,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with | None -> DebugOff | Some level -> level -(** TODO: unify printing of generic Ltac values in case of coercion failure. *) - -(* Displays a value *) -let pr_value env v = - let pr_with_env pr = - match env with - | Some (env,sigma) -> pr env sigma - | None -> str "a value of type" ++ spc () ++ pr_argument_type v in - let open Genprint in - match generic_val_print v with - | TopPrinterBasic pr -> pr () - | TopPrinterNeedsContext pr -> pr_with_env pr - | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> - pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) - let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in let pr_sep () = fnl () in @@ -357,22 +291,18 @@ 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 " ++ Id.print 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 try_interp_ltac_var coerce ist env {loc;v=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 -> + Taccoerce.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 locid.v ++ 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)) (Loc.tag id) + try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (make id) with Not_found -> id (* Interprets an optional identifier, bound or fresh *) @@ -381,25 +311,25 @@ let interp_name ist env sigma = function | Name id -> Name (interp_ident ist env sigma id) let interp_intro_pattern_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroNaming (IntroIdentifier id) let interp_intro_pattern_naming_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroIdentifier id -let interp_int ist locid = +let interp_int ist ({loc;v=id} as locid) = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> - user_err ?loc:(fst locid) ~hdr:"interp_int" - (str "Unbound variable " ++ Id.print (snd locid) ++ str".") + user_err ?loc ~hdr:"interp_int" + (str "Unbound variable " ++ Id.print id ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid | ArgArg n -> n let interp_int_or_var_as_list ist = function - | ArgVar (_,id as locid) -> + | ArgVar ({v=id} as locid) -> (try coerce_to_int_or_var_list (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)]) | ArgArg n as x -> [x] @@ -408,7 +338,7 @@ let interp_int_or_var_list ist l = List.flatten (List.map (interp_int_or_var_as_list ist) l) (* Interprets a bound variable (especially an existing hypothesis) *) -let interp_hyp ist env sigma (loc,id as locid) = +let interp_hyp ist env sigma ({loc;v=id} as locid) = (* Look first in lfun for a value coercible to a variable *) try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid with Not_found -> @@ -416,7 +346,7 @@ let interp_hyp ist env sigma (loc,id as locid) = if is_variable env id then id else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) -let interp_hyp_list_as_list ist env sigma (loc,id as x) = +let interp_hyp_list_as_list ist env sigma ({loc;v=id} as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x] @@ -425,8 +355,8 @@ let interp_hyp_list ist env sigma l = let interp_reference ist env sigma = function | ArgArg (_,r) -> r - | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id) + | ArgVar {loc;v=id} -> + try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) @@ -439,7 +369,7 @@ let try_interp_evaluable env (loc, id) = | _ -> error_not_evaluable (VarRef id) let interp_evaluable ist env sigma = function - | ArgArg (r,Some (loc,id)) -> + | ArgArg (r,Some {loc;v=id}) -> (* Maybe [id] has been introduced by Intro-like tactics *) begin try try_interp_evaluable env (loc, id) @@ -449,8 +379,8 @@ let interp_evaluable ist env sigma = function | _ -> 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) + | ArgVar {loc;v=id} -> + try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) with Not_found -> error_global_not_found ?loc (qualid_of_ident id) @@ -521,9 +451,9 @@ 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)) (Loc.tag id) + ist (Some (env,sigma)) (make id) with Not_found -> id in - let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in + let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with | None -> Id.Set.empty | Some l -> l @@ -535,7 +465,7 @@ let interp_fresh_id ist env sigma l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in + | ArgVar {v=id} -> Id.to_string (extract_ident ist env sigma id)) l) in let s = if CLexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env @@ -583,7 +513,7 @@ let interp_glob_closure ist env sigma ?(kind=WithoutTypeConstraint) ?(pattern_mo ltac_bound = Id.Map.domain ist.lfun; ltac_extra = Genintern.Store.empty; } in - { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env term_expr } + { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env sigma term_expr } let interp_uconstr ist env sigma c = interp_glob_closure ist env sigma c @@ -701,7 +631,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) = let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let p = match a with - | Inl (ArgVar (loc,id)) -> + | Inl (ArgVar {loc;v=id}) -> (* This is the encoding of an ltac var supposed to be bound prioritary to an evaluable reference and otherwise to a constr (it is an encoding to satisfy the "union" type given to Simpl) *) @@ -710,7 +640,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in 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) + (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> error_global_not_found ?loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) @@ -756,7 +686,7 @@ let interp_may_eval f ist env sigma = function let (sigma,c_interp) = f ist env sigma c in let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in redfun env sigma c_interp - | ConstrContext ((loc,s),c) -> + | ConstrContext ({loc;v=s},c) -> (try let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in @@ -821,7 +751,7 @@ let message_of_value v = let interp_message_token ist = function | MsgString s -> Ftactic.return (str s) | MsgInt n -> Ftactic.return (int n) - | MsgIdent (loc,id) -> + | MsgIdent {loc;v=id} -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found.")) @@ -881,7 +811,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None - | Some (ArgVar (loc,id)) -> + | Some (ArgVar {loc;v=id}) -> (match interp_intro_pattern_var loc ist env sigma id with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> @@ -906,14 +836,14 @@ let interp_binding_name ist env 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 (Some (env,sigma)) (Loc.tag id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make 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)) (Loc.tag id) + (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,(b,c)) = @@ -924,7 +854,7 @@ let interp_bindings ist env sigma = function | NoBindings -> sigma, NoBindings | ImplicitBindings l -> - let sigma, l = interp_open_constr_list ist env sigma l in + let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in @@ -959,14 +889,14 @@ let interp_destruction_arg ist gl arg = interp_open_constr_with_bindings ist env sigma c end | keep,ElimOnAnonHyp n as x -> x - | keep,ElimOnIdent (loc,id) -> + | keep,ElimOnIdent {loc;v=id} -> let error () = user_err ?loc (strbrk "Cannot coerce " ++ Id.print id ++ strbrk " neither to a quantified hypothesis nor to a term.") in let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl - then keep,ElimOnIdent (loc,id') + then keep,ElimOnIdent CAst.(make ?loc id') else (keep, ElimOnConstr begin fun env sigma -> try (sigma, (constr_of_id env id', NoBindings)) @@ -994,7 +924,7 @@ let interp_destruction_arg ist gl arg = with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then - keep,ElimOnIdent (loc,id) + keep,ElimOnIdent CAst.(make ?loc id) else let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f env sigma = @@ -1043,11 +973,11 @@ let cons_and_check_name id l = else id::l let rec read_match_goal_hyps lfun ist env sigma lidh = function - | (Hyp ((loc,na) as locna,mp))::tl -> + | (Hyp ({loc;v=na} as locna,mp))::tl -> 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 -> + | (Def ({loc;v=na} as locna,mv,mp))::tl -> 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) @@ -1112,7 +1042,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti in Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) - + and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> @@ -1248,7 +1178,7 @@ and force_vrec ist v : Val.t Ftactic.t = and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = match r with - | ArgVar (loc,id) -> + | ArgVar {loc;v=id} -> let v = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id @@ -1416,7 +1346,7 @@ and tactic_of_value ist vle = 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 ((_, na), b) = + let fold accu ({v=na}, b) = let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in Name.fold_right (fun id -> Id.Map.add id v) na accu in @@ -1431,7 +1361,7 @@ and interp_letin ist llc u = | [] -> let ist = { ist with lfun } in val_interp ist u - | ((_, na), body) :: defs -> + | ({v=na}, body) :: defs -> Ftactic.bind (interp_tacarg ist body) (fun v -> fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs) in @@ -2087,27 +2017,6 @@ let _ = in Pretyping.register_constr_interp0 wit_tactic eval -(** Used in tactic extension **) - -let dummy_id = Id.of_string "_" - -let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let map = function - | Anonymous -> None - | Name id -> - let c = Id.Map.find id ist.lfun in - try Some (coerce_to_closed_constr env c) - with CannotCoerceTo ty -> - error_ltac_variable dummy_id (Some (env,sigma)) c ty - in - let args = List.map_filter map vars in - tac args ist - end in - tac - let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 5f2723a1e3..bd44bdbea4 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -75,7 +77,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map (** Interprets tactic expressions *) val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> - Id.t Loc.located -> Id.t + lident -> Id.t val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> @@ -125,19 +127,11 @@ val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> uni (** Internals that can be useful for syntax extensions. *) val interp_ltac_var : (value -> 'a) -> interp_sign -> - (Environ.env * Evd.evar_map) option -> Id.t Loc.located -> 'a + (Environ.env * Evd.evar_map) option -> lident -> 'a -val interp_int : interp_sign -> Id.t Loc.located -> int +val interp_int : interp_sign -> lident -> int val interp_int_or_var : interp_sign -> int or_var -> int -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 - the Ltac environment according to the given names. *) -val lift_constr_tac_to_ml_tac : Name.t list -> - (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic - val default_ist : unit -> Geninterp.interp_sign (** Empty ist with debug set on the current value. *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 79bf3685e2..927139c1af 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index 5ac3775676..0a894791b0 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Tacexpr diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 2dd7c9a747..e55b49fb4e 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 2475e41f9d..734e76b563 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Environ @@ -74,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - Id.t Loc.located message_token list -> unit Proofview.NonLogical.t + Misctypes.lident message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index e87951dd7f..b6462c8106 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file extends Matching with the main logic for Ltac's @@ -306,9 +308,9 @@ module PatternMatching (E:StaticEnvironment) = struct [pat] is [Hyp _] or [Def _]. *) let hyp_match pat hyps = match pat with - | Hyp ((_,hypname),typepat) -> + | Hyp ({CAst.v=hypname},typepat) -> hyp_match_type hypname typepat hyps - | Def ((_,hypname),bodypat,typepat) -> + | Def ({CAst.v=hypname},bodypat,typepat) -> hyp_match_body_and_type hypname bodypat typepat hyps (** [hyp_pattern_list_match pats hyps lhs], matches the list of diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 955f8105fb..0722c68783 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -1,9 +1,11 @@ - (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index fdeab8dc4b..f6b2e5b362 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Libobject diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index 95cd243ec8..d2f2947c94 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Tacexpr diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 01d3f79c74..a51c09ca4f 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Term @@ -63,11 +65,6 @@ let assoc_flags ist : tauto_flags = (* Whether inner not are unfolded *) let negation_unfolding = ref true -(* Whether inner iff are unfolded *) -let iff_unfolding = ref false - -let unfold_iff () = !iff_unfolding - open Goptions let _ = declare_bool_option @@ -77,14 +74,6 @@ let _ = optread = (fun () -> !negation_unfolding); optwrite = (:=) negation_unfolding } -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "unfolding of iff in intuition"; - optkey = ["Intuition";"Iff";"Unfolding"]; - optread = (fun () -> !iff_unfolding); - optwrite = (:=) iff_unfolding } - (** Base tactics *) let idtac = Proofview.tclUNIT () @@ -200,16 +189,13 @@ let make_unfold name = let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) -let u_iff = make_unfold "iff" let u_not = make_unfold "not" let reduction_not_iff _ ist = 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] - | false, true -> make_reduce [u_iff] - | false, false -> TacId [] + let tac = match !negation_unfolding with + | true -> make_reduce [u_not] + | false -> TacId [] in eval_tactic_ist ist tac @@ -255,10 +241,10 @@ let tauto_power_flags = { } let with_flags flags _ ist = - let f = (Loc.tag @@ Id.of_string "f") in - let x = (Loc.tag @@ Id.of_string "x") in + let f = CAst.make @@ Id.of_string "f" in + let x = CAst.make @@ 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 + let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) let register_tauto_tactic tac name0 args = |