From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/ltac/g_ltac.ml4 | 69 +++++++++++++++++++++++++++---------------------- 1 file changed, 38 insertions(+), 31 deletions(-) (limited to 'plugins/ltac/g_ltac.ml4') diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 0c42a8bb..929390b1 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,21 +12,22 @@ DECLARE PLUGIN "ltac_plugin" open Util open Pp +open Glob_term open Constrexpr open Tacexpr -open Misctypes +open Namegen open Genarg open Genredexpr open Tok (* necessary for camlp5 *) open Names open Pcoq -open Pcoq.Constr -open Pcoq.Vernac_ open Pcoq.Prim +open Pcoq.Constr +open Pvernac.Vernac_ open Pltac -let fail_default_value = ArgArg 0 +let fail_default_value = Locus.ArgArg 0 let arg_of_expr = function TacArg (loc,a) -> a @@ -34,20 +35,21 @@ let arg_of_expr = function let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat +let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat 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 = CAst.map_with_loc (fun ?loc -> function - | Libnames.Ident id -> id - | Libnames.Qualid _ -> - CErrors.user_err ?loc - (str "This expression should be a simple identifier.")) +let reference_to_id qid = + if Libnames.qualid_is_ident qid then + CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc + (str "This expression should be a simple identifier.") -let tactic_mode = Gram.entry_create "vernac:tactic_command" +let tactic_mode = Entry.create "vernac:tactic_command" let new_entry name = - let e = Gram.entry_create name in + let e = Entry.create name in e let toplevel_selector = new_entry "vernac:toplevel_selector" @@ -58,8 +60,8 @@ let tacdef_body = new_entry "tactic:tacdef_body" let _ = let mode = { Proof_global.name = "Classic"; - set = (fun () -> set_command_entry tactic_mode); - reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + set = (fun () -> Pvernac.set_command_entry tactic_mode); + reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); } in Proof_global.register_proof_mode mode @@ -197,9 +199,8 @@ GEXTEND Gram non ambiguous name where dots are replaced by "_"? Probably too verbose most of the time. *) fresh_id: - [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - ArgVar (CAst.make ~loc:!@loc id) ] ] + [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) + | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -286,12 +287,14 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> + [ [ name = Constr.global; it=LIST1 input_fun; + redef = ltac_def_kind; body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> + | name = Constr.global; redef = ltac_def_kind; + body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -311,21 +314,23 @@ GEXTEND Gram range_selector_or_nth: [ [ n = natural ; "-" ; m = natural; l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - SelectList ((n, m) :: Option.default [] l) + Goal_select.SelectList ((n, m) :: Option.default [] l) | n = natural; l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> + let open Goal_select in Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] ; selector_body: [ [ l = range_selector_or_nth -> l - | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ] + | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ] ; selector: [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] ; toplevel_selector: [ [ sel = selector_body; ":" -> sel - | IDENT "all"; ":" -> SelectAll ] ] + | "!"; ":" -> Goal_select.SelectAlreadyFocused + | IDENT "all"; ":" -> Goal_select.SelectAll ] ] ; tactic_mode: [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g @@ -342,7 +347,7 @@ GEXTEND Gram hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - Vernacexpr.HintsExtern (n,c, in_tac tac) ] ] + Hints.HintsExtern (n,c, in_tac tac) ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> @@ -369,6 +374,7 @@ let _ = declare_int_option { } let vernac_solve n info tcom b = + let open Goal_select in let status = Proof_global.with_current_proof (fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in @@ -415,7 +421,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false VERNAC tactic_mode EXTEND VernacSolve | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => [ classify_as_proofstep ] -> [ - let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in + let g = Option.default (Goal_select.get_default_goal_selector ()) g in vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => @@ -428,7 +434,7 @@ VERNAC tactic_mode EXTEND VernacSolve VtLater ] -> [ let t = rm_abstract t in - vernac_solve SelectAll n t def + vernac_solve Goal_select.SelectAll n t def ] END @@ -466,14 +472,15 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + let deprecation = atts.deprecated in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; st ] END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ] + [ Feedback.msg_notice (Tacintern.print_ltac r) ] END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY @@ -481,7 +488,7 @@ VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY [ Tacentries.print_located_tactic r ] END -let pr_ltac_ref = Libnames.pr_reference +let pr_ltac_ref = Libnames.pr_qualid let pr_tacdef_body tacdef_body = let id, redef, body = @@ -508,10 +515,10 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition ({CAst.v=Ident r},_) -> r - | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater + | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in - Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + let deprecation = atts.deprecated in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; st ] END -- cgit v1.2.3