Moving most of Ltac code to Hightactics.

This is a major step towards the pluginification of Ltac. The one important
file that is out of reach for now is Tacsubst, as it is used in an intricate way
to handle amongst other things auto hints.

7 files changed, 731 insertions, 8 deletions

diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4
new file mode 100644
index 0000000000..f46a670080
--- /dev/null
+++ b/tactics/g_ltac.ml4
@@ -0,0 +1,429 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+open Util
+open Pp
+open Compat
+open Constrexpr
+open Tacexpr
+open Misctypes
+open Genarg
+open Genredexpr
+open Tok (* necessary for camlp4 *)
+
+open Pcoq
+open Pcoq.Prim
+open Pcoq.Tactic
+
+let fail_default_value = ArgArg 0
+
+let arg_of_expr = function
+    TacArg (loc,a) -> a
+  | e -> Tacexp (e:raw_tactic_expr)
+
+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 Constrarg.wit_intro_pattern) pat
+let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
+
+let reference_to_id = function
+  | Libnames.Ident (loc, id) -> (loc, id)
+  | Libnames.Qualid (loc,_) ->
+      Errors.user_err_loc (loc, "",
+        str "This expression should be a simple identifier.")
+
+let tactic_mode = Gram.entry_create "vernac:tactic_command"
+
+let new_entry name =
+  let e = Gram.entry_create name in
+  let entry = Entry.create name in
+  let () = Pcoq.set_grammar entry e in
+  e
+
+let selector = new_entry "vernac:selector"
+let tacdef_body = new_entry "tactic:tacdef_body"
+
+(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
+    proof editing and changes nothing else). Then sets it as the default proof mode. *)
+let _ =
+  let mode = {
+    Proof_global.name = "Classic";
+    set = (fun () -> set_command_entry tactic_mode);
+    reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+  } in
+  Proof_global.register_proof_mode mode
+
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+  Gram.Entry.of_parser "test_bracket_ident"
+    (fun strm ->
+      match get_tok (stream_nth 0 strm) with
+        | KEYWORD "[" ->
+            (match get_tok (stream_nth 1 strm) with
+              | IDENT _ -> ()
+	      | _ -> raise Stream.Failure)
+	| _ -> raise Stream.Failure)
+
+(* Tactics grammar rules *)
+
+GEXTEND Gram
+  GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
+          tactic_mode constr_may_eval constr_eval selector;
+
+  tactic_then_last:
+    [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
+          Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta)
+      | -> [||]
+    ] ]
+  ;
+  tactic_then_gen:
+    [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last)
+      | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l))
+      | ".."; l = tactic_then_last -> ([], Some (TacId [], l))
+      | ta = tactic_expr -> ([ta], None)
+      | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last)
+      | -> ([TacId []], None)
+    ] ]
+  ;
+  tactic_then_locality: (* [true] for the local variant [TacThens] and [false]
+                           for [TacExtend] *)
+  [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ]
+  ;
+  tactic_expr:
+    [ "5" RIGHTA
+      [ te = binder_tactic -> te ]
+    | "4" LEFTA
+      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
+      | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1)
+      | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" ->
+	  match l , tail with
+          | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
+	  | true  , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
+          | false , None -> TacThen (ta0,TacDispatch first)
+	  | true  , None -> TacThens (ta0,first) ]
+    | "3" RIGHTA
+      [ IDENT "try"; ta = tactic_expr -> TacTry ta
+      | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
+      | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
+      | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta)
+      | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
+      | IDENT "progress"; ta = tactic_expr -> TacProgress ta
+      | IDENT "once"; ta = tactic_expr -> TacOnce ta
+      | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta
+      | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
+(*To do: put Abstract in Refiner*)
+      | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
+      | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
+          TacAbstract (tc,Some s) ]
+(*End of To do*)
+    | "2" RIGHTA
+      [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1)
+      | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) 
+      | IDENT "tryif" ; ta = tactic_expr ;
+              "then" ; tat = tactic_expr ;
+              "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae)
+      | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
+      | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
+    | "1" RIGHTA
+      [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
+          TacMatchGoal (b,false,mrl)
+      | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
+        mrl = match_context_list; "end" ->
+          TacMatchGoal (b,true,mrl)
+      |	b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
+          TacMatch (b,c,mrl)
+      | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+	  TacFirst l
+      | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+	  TacSolve l
+      | IDENT "idtac"; l = LIST0 message_token -> TacId l
+      | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ];
+	  l = LIST0 message_token -> TacFail (g,n,l)
+      | st = simple_tactic -> st
+      | a = tactic_arg -> TacArg(!@loc,a)
+      | r = reference; la = LIST0 tactic_arg_compat ->
+          TacArg(!@loc,TacCall (!@loc,r,la)) ]
+    | "0"
+      [ "("; a = tactic_expr; ")" -> a
+      | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
+          begin match tail with
+          | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
+          | None -> TacDispatch tf
+          end
+      | a = tactic_atom -> TacArg (!@loc,a) ] ]
+  ;
+  failkw:
+  [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ]
+  ;
+  (* binder_tactic: level 5 of tactic_expr *)
+  binder_tactic:
+    [ RIGHTA
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
+          TacFun (it,body)
+      | "let"; isrec = [IDENT "rec" -> true | -> false];
+          llc = LIST1 let_clause SEP "with"; "in";
+          body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body)
+      | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ]
+  ;
+  (* Tactic arguments to the right of an application *)
+  tactic_arg_compat:
+    [ [ a = tactic_arg -> a
+      | r = reference -> Reference r
+      | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
+      (* Unambigous entries: tolerated w/o "ltac:" modifier *)
+      | "()" -> TacGeneric (genarg_of_unit ()) ] ]
+  ;
+  (* Can be used as argument and at toplevel in tactic expressions. *)
+  tactic_arg:
+    [ [ c = constr_eval -> ConstrMayEval c
+      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
+      | IDENT "type_term"; c=uconstr -> TacPretype c
+      | IDENT "numgoals" -> TacNumgoals ] ]
+  ;
+  (* If a qualid is given, use its short name. TODO: have the shortest
+     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 (snd qid) in ArgVar (!@loc,id) ] ]
+  ;
+  constr_eval:
+    [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
+          ConstrEval (rtc,c)
+      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
+          ConstrContext (id,c)
+      | IDENT "type"; IDENT "of"; c = Constr.constr ->
+          ConstrTypeOf c ] ]
+  ;
+  constr_may_eval: (* For extensions *)
+    [ [ c = constr_eval -> c
+      | c = Constr.constr -> ConstrTerm c ] ]
+  ;
+  tactic_atom:
+    [ [ n = integer -> TacGeneric (genarg_of_int n)
+      | r = reference -> TacCall (!@loc,r,[])
+      | "()" -> TacGeneric (genarg_of_unit ()) ] ]
+  ;
+  match_key:
+    [ [ "match" -> Once
+      | "lazymatch" -> Select
+      | "multimatch" -> General ] ]
+  ;
+  input_fun:
+    [ [ "_" -> None
+      | l = ident -> Some l ] ]
+  ;
+  let_clause:
+    [ [ id = identref; ":="; te = tactic_expr ->
+         (id, arg_of_expr te)
+      | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+         (id, arg_of_expr (TacFun(args,te))) ] ]
+  ;
+  match_pattern:
+    [ [ IDENT "context";  oid = OPT Constr.ident;
+          "["; pc = Constr.lconstr_pattern; "]" ->
+        let mode = not (!Flags.tactic_context_compat) in
+        Subterm (mode, oid, pc)
+      | IDENT "appcontext";  oid = OPT Constr.ident;
+          "["; pc = Constr.lconstr_pattern; "]" ->
+        msg_warning (strbrk "appcontext is deprecated");
+        Subterm (true,oid, pc)
+      | pc = Constr.lconstr_pattern -> Term pc ] ]
+  ;
+  match_hyps:
+    [ [ na = name; ":"; mp =  match_pattern -> Hyp (na, mp)
+      | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt)
+      | na = name; ":="; mpv = match_pattern ->
+	  let t, ty =
+	    match mpv with
+	    | Term t -> (match t with
+	      | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
+	      | _ -> mpv, None)
+	    | _ -> mpv, None
+	  in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty)
+    ] ]
+  ;
+  match_context_rule:
+    [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
+        "=>"; te = tactic_expr -> Pat (largs, mp, te)
+      | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
+        "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te)
+      | "_"; "=>"; te = tactic_expr -> All te ] ]
+  ;
+  match_context_list:
+    [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
+      | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
+  ;
+  match_rule:
+    [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te)
+      | "_"; "=>"; te = tactic_expr -> All te ] ]
+  ;
+  match_list:
+    [ [ mrl = LIST1 match_rule SEP "|" -> mrl
+      | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
+  ;
+  message_token:
+    [ [ id = identref -> MsgIdent id
+      | s = STRING -> MsgString s
+      | n = integer -> MsgInt n ] ]
+  ;
+
+  ltac_def_kind:
+    [ [ ":=" -> false
+      | "::=" -> true ] ]
+  ;
+
+  (* Definitions for tactics *)
+  tacdef_body:
+    [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+          if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body))
+          else
+            let id = reference_to_id name in
+            Vernacexpr.TacticDefinition (id, TacFun (it, body))
+      | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
+          if redef then Vernacexpr.TacticRedefinition (name, body)
+          else
+            let id = reference_to_id name in
+            Vernacexpr.TacticDefinition (id, body)
+    ] ]
+  ;
+  tactic:
+    [ [ tac = tactic_expr -> tac ] ]
+  ;
+  selector:
+    [ [ n=natural; ":" -> Vernacexpr.SelectNth n
+      | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
+      | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ]
+  ;
+  tactic_mode:
+    [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ]
+  ;
+  END
+
+open Stdarg
+open Constrarg
+open Vernacexpr
+open Vernac_classifier
+open Goptions
+open Libnames
+
+let print_info_trace = ref None
+
+let _ = declare_int_option {
+  optsync = true;
+  optdepr = false;
+  optname = "print info trace";
+  optkey = ["Info" ; "Level"];
+  optread = (fun () -> !print_info_trace);
+  optwrite = fun n -> print_info_trace := n;
+}
+
+let vernac_solve n info tcom b =
+  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 -> true | _ -> false in
+    let info = Option.append info !print_info_trace in
+    let (p,status) =
+      Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+    in
+    (* in case a strict subtree was completed,
+       go back to the top of the prooftree *)
+    let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+    p,status) in
+    if not status then Pp.feedback Feedback.AddedAxiom
+
+let pr_ltac_selector = function
+| SelectNth i -> int i ++ str ":"
+| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+| SelectAll -> str "all" ++ str ":"
+
+VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
+| [ selector(s) ] -> [ s ]
+END
+
+let pr_ltac_info n = str "Info" ++ spc () ++ int n
+
+VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info
+| [ "Info" natural(n) ] -> [ n ]
+END
+
+let pr_ltac_use_default b = if b then str ".." else mt ()
+
+VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
+| [ "." ] -> [ false ]
+| [ "..." ] -> [ true ]
+END
+
+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_global.get_default_goal_selector ()) g in
+    vernac_solve g n t def
+  ]
+| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    [ VtProofStep true, VtLater ] -> [
+    vernac_solve SelectAll n t def
+  ]
+END
+
+let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")"
+
+VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY pr_ltac_tactic_level
+| [ "(" "at" "level" natural(n) ")" ] -> [ n ]
+END
+
+VERNAC ARGUMENT EXTEND ltac_production_sep
+| [ "," string(sep) ] -> [ sep ]
+END
+
+let pr_ltac_production_item = function
+| TacTerm s -> quote (str s)
+| TacNonTerm (_, arg, (id, sep)) ->
+  let sep = match sep with
+  | "" -> mt ()
+  | sep -> str "," ++ spc () ++ quote (str sep)
+  in
+  str arg ++ str "(" ++ Nameops.pr_id id ++ sep ++ str ")"
+
+VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
+| [ string(s) ] -> [ TacTerm s ]
+| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
+  [ TacNonTerm (loc, Names.Id.to_string nt, (p, Option.default "" sep)) ]
+END
+
+VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF
+| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] ->
+  [
+    let l = Locality.LocalityFixme.consume () in
+    let n = Option.default 0 n in
+    Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e)
+  ]
+END
+
+VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
+| [ "Print" "Ltac" reference(r) ] ->
+  [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
+END
+
+VERNAC ARGUMENT EXTEND ltac_tacdef_body
+| [ tacdef_body(t) ] -> [ t ]
+END
+
+VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
+| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
+    VtSideff (List.map (function
+      | TacticDefinition ((_,r),_) -> r
+      | TacticRedefinition (Ident (_,r),_) -> r
+      | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
+  ] -> [
+    let lc = Locality.LocalityFixme.consume () in
+    Tacentries.register_ltac (Locality.make_module_locality lc) l
+  ]
+END
diff --git a/tactics/g_obligations.ml4 b/tactics/g_obligations.ml4
index e67d701218..4cd8bf1feb 100644
--- a/tactics/g_obligations.ml4
+++ b/tactics/g_obligations.ml4
@@ -19,16 +19,22 @@ open Constrexpr_ops
 open Stdarg
 open Constrarg
 open Extraargs
-open Pcoq.Prim
-open Pcoq.Constr
-open Pcoq.Tactic
+
+let (set_default_tactic, get_default_tactic, print_default_tactic) = 
+  Tactic_option.declare_tactic_option "Program tactic"
+
+let () =
+  (** Delay to recover the tactic imperatively *)
+  let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
+    snd (get_default_tactic ())
+  end in
+  Obligations.default_tactic := tac
 
 (* We define new entries for programs, with the use of this module
  * Subtac. These entries are named Subtac.<foo>
  *)
 
 module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
 module Tactic = Pcoq.Tactic
 
 open Pcoq
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 5c59465429..468b938b6a 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,8 @@
+Tacintern
+Tacentries
+Tacinterp
+Evar_tactics
+Tactic_option
 Extraargs
 G_obligations
 Coretactics
@@ -12,3 +17,4 @@ G_rewrite
 Tauto
 Eqdecide
 G_eqdecide
+G_ltac
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
new file mode 100644
index 0000000000..711cd8d9d0
--- /dev/null
+++ b/tactics/tacentries.ml
@@ -0,0 +1,263 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Libobject
+open Pcoq
+open Egramml
+open Egramcoq
+open Vernacexpr
+open Libnames
+open Nameops
+
+(**********************************************************************)
+(* Tactic Notation                                                    *)
+
+let interp_prod_item lev = function
+  | TacTerm s -> GramTerminal s
+  | TacNonTerm (loc, nt, (_, sep)) ->
+      let EntryName (etyp, e) = interp_entry_name lev nt sep in
+      GramNonTerminal (loc, etyp, e)
+
+let make_terminal_status = function
+  | GramTerminal s -> Some s
+  | GramNonTerminal _ -> None
+
+let make_fresh_key =
+  let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
+  fun () ->
+    let cur = incr id; !id in
+    let lbl = Id.of_string ("_" ^ string_of_int cur) in
+    let kn = Lib.make_kn lbl in
+    let (mp, dir, _) = KerName.repr kn in
+    (** We embed the full path of the kernel name in the label so that the
+        identifier should be unique. This ensures that including two modules
+        together won't confuse the corresponding labels. *)
+    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
+      (ModPath.to_string mp) (DirPath.to_string dir) cur)
+    in
+    KerName.make mp dir (Label.of_id lbl)
+
+type tactic_grammar_obj = {
+  tacobj_key : KerName.t;
+  tacobj_local : locality_flag;
+  tacobj_tacgram : tactic_grammar;
+  tacobj_tacpp : Pptactic.pp_tactic;
+  tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+}
+
+let check_key key =
+  if Tacenv.check_alias key then
+    error "Conflicting tactic notations keys. This can happen when including \
+    twice the same module."
+
+let cache_tactic_notation (_, tobj) =
+  let key = tobj.tacobj_key in
+  let () = check_key key in
+  Tacenv.register_alias key tobj.tacobj_body;
+  Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
+  Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
+
+let open_tactic_notation i (_, tobj) =
+  let key = tobj.tacobj_key in
+  if Int.equal i 1 && not tobj.tacobj_local then
+    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+
+let load_tactic_notation i (_, tobj) =
+  let key = tobj.tacobj_key in
+  let () = check_key key in
+  (** Only add the printing and interpretation rules. *)
+  Tacenv.register_alias key tobj.tacobj_body;
+  Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
+  if Int.equal i 1 && not tobj.tacobj_local then
+    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+
+let subst_tactic_notation (subst, tobj) =
+  let (ids, body) = tobj.tacobj_body in
+  { tobj with
+    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
+    tacobj_body = (ids, Tacsubst.subst_tactic subst body);
+  }
+
+let classify_tactic_notation tacobj = Substitute tacobj
+
+let inTacticGrammar : tactic_grammar_obj -> obj =
+  declare_object {(default_object "TacticGrammar") with
+       open_function = open_tactic_notation;
+       load_function = load_tactic_notation;
+       cache_function = cache_tactic_notation;
+       subst_function = subst_tactic_notation;
+       classify_function = classify_tactic_notation}
+
+let cons_production_parameter = function
+| TacTerm _ -> None
+| TacNonTerm (_, _, (id, _)) -> Some id
+
+let add_tactic_notation (local,n,prods,e) =
+  let ids = List.map_filter cons_production_parameter prods in
+  let prods = List.map (interp_prod_item n) prods in
+  let pprule = {
+    Pptactic.pptac_level = n;
+    pptac_prods = prods;
+  } in
+  let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
+  let parule = {
+    tacgram_level = n;
+    tacgram_prods = prods;
+  } in
+  let tacobj = {
+    tacobj_key = make_fresh_key ();
+    tacobj_local = local;
+    tacobj_tacgram = parule;
+    tacobj_tacpp = pprule;
+    tacobj_body = (ids, tac);
+  } in
+  Lib.add_anonymous_leaf (inTacticGrammar tacobj)
+
+(**********************************************************************)
+(* ML Tactic entries                                                  *)
+
+type ml_tactic_grammar_obj = {
+  mltacobj_name : Tacexpr.ml_tactic_name;
+  (** ML-side unique name *)
+  mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list;
+  (** Grammar rules generating the ML tactic. *)
+}
+
+exception NonEmptyArgument
+
+(** ML tactic notations whose use can be restricted to an identifier are added
+    as true Ltac entries. *)
+let extend_atomic_tactic name entries =
+  let open Tacexpr in
+  let map_prod prods =
+    let (hd, rem) = match prods with
+    | GramTerminal s :: rem -> (s, rem)
+    | _ -> assert false (** Not handled by the ML extension syntax *)
+    in
+    let empty_value = function
+    | GramTerminal s -> raise NonEmptyArgument
+    | GramNonTerminal (_, typ, e) ->
+      let Genarg.Rawwit wit = typ in
+      let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in
+      let default = epsilon_value inj e in
+      match default with
+      | None -> raise NonEmptyArgument
+      | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
+    in
+    try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
+  in
+  let entries = List.map map_prod entries in
+  let add_atomic i args = match args with
+  | None -> ()
+  | Some (id, args) ->
+    let args = List.map (fun a -> Tacexp a) args in
+    let entry = { mltac_name = name; mltac_index = i } in
+    let body = TacML (Loc.ghost, entry, args) in
+    Tacenv.register_ltac false false (Names.Id.of_string id) body
+  in
+  List.iteri add_atomic entries
+
+let cache_ml_tactic_notation (_, obj) =
+  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
+
+let open_ml_tactic_notation i obj =
+  if Int.equal i 1 then cache_ml_tactic_notation obj
+
+let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
+  declare_object { (default_object "MLTacticGrammar") with
+    open_function = open_ml_tactic_notation;
+    cache_function = cache_ml_tactic_notation;
+    classify_function = (fun o -> Substitute o);
+    subst_function = (fun (_, o) -> o);
+  }
+
+let add_ml_tactic_notation name prods =
+  let obj = {
+    mltacobj_name = name;
+    mltacobj_prod = prods;
+  } in
+  Lib.add_anonymous_leaf (inMLTacticGrammar obj);
+  extend_atomic_tactic name prods
+
+(** Command *)
+
+
+type tacdef_kind =
+  | NewTac of Id.t
+  | UpdateTac of Nametab.ltac_constant
+
+let is_defined_tac kn =
+  try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
+
+let register_ltac local tacl =
+  let map tactic_body =
+    match tactic_body with
+    | TacticDefinition ((loc,id), body) ->
+        let kn = Lib.make_kn id in
+        let id_pp = pr_id id in
+        let () = if is_defined_tac kn then
+          Errors.user_err_loc (loc, "",
+            str "There is already an Ltac named " ++ id_pp ++ str".")
+        in
+        let is_primitive =
+          try
+            match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
+            | Tacexpr.TacArg _ -> false
+            | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
+          with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+        in
+        let () = if is_primitive then
+          msg_warning (str "The Ltac name " ++ id_pp ++
+            str " may be unusable because of a conflict with a notation.")
+        in
+        NewTac id, body
+    | TacticRedefinition (ident, body) ->
+        let loc = loc_of_reference ident in
+        let kn =
+          try Nametab.locate_tactic (snd (qualid_of_reference ident))
+          with Not_found ->
+            Errors.user_err_loc (loc, "",
+                        str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+        in
+        UpdateTac kn, body
+  in
+  let rfun = List.map map tacl in
+  let recvars =
+    let fold accu (op, _) = match op with
+    | UpdateTac _ -> accu
+    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
+    in
+    List.fold_left fold [] rfun
+  in
+  let ist = Tacintern.make_empty_glob_sign () in
+  let map (name, body) =
+    let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
+    (name, body)
+  in
+  let defs () =
+    (** Register locally the tactic to handle recursivity. This function affects
+        the whole environment, so that we transactify it afterwards. *)
+    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
+    let () = List.iter iter_rec recvars in
+    List.map map rfun
+  in
+  let defs = Future.transactify defs () in
+  let iter (def, tac) = match def with
+  | NewTac id ->
+    Tacenv.register_ltac false local id tac;
+    Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
+  | UpdateTac kn ->
+    Tacenv.redefine_ltac local kn tac;
+    let name = Nametab.shortest_qualid_of_tactic kn in
+    Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
+  in
+  List.iter iter defs
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
new file mode 100644
index 0000000000..3cf0bc5cc9
--- /dev/null
+++ b/tactics/tacentries.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Tacexpr
+
+(** Adding a tactic notation in the environment *)
+
+val add_tactic_notation :
+  locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr ->
+    unit
+
+val add_ml_tactic_notation : ml_tactic_name ->
+  Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
+
+val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 36faba1137..6bf0e2aa73 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2214,3 +2214,5 @@ let _ =
       optkey   = ["Ltac";"Debug"];
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
+
+let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index fd7fab0c58..b495a885f8 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -19,10 +19,6 @@ Taccoerce
 Tacenv
 Hints
 Auto
-Tacintern
 Tactic_matching
 Tactic_debug
-Tacinterp
-Evar_tactics
 Term_dnet
-Tactic_option