diff options
Diffstat (limited to 'plugins/ltac/g_ltac.ml4')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 0c42a8bb2..d7d642e50 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,7 +35,7 @@ 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 @@ -58,8 +59,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 +198,9 @@ 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)*) + [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - ArgVar (CAst.make ~loc:!@loc id) ] ] + Locus.ArgVar (CAst.make ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -325,6 +326,7 @@ GEXTEND Gram ; toplevel_selector: [ [ sel = selector_body; ":" -> sel + | "!"; ":" -> SelectAlreadyFocused | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: @@ -415,7 +417,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) ] => |