1 files changed, 38 insertions, 31 deletions

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