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.

22 files changed, 376 insertions, 362 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index bbd3d8a62f..2ef30f299b 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -120,7 +120,7 @@ let declare_tactic loc s c cl = match cl with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
-  let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ >> in
+  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
       try do {
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 36b855ec3b..bd5890e296 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -60,7 +60,6 @@ type printable =
   | PrintClasses
   | PrintTypeClasses
   | PrintInstances of reference or_by_notation
-  | PrintLtac of reference
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
   | PrintCanonicalConversions
@@ -291,8 +290,6 @@ type vernac_expr =
   | VernacError of exn (* always fails *)
 
   (* Syntax *)
-  | VernacTacticNotation of
-      int * grammar_tactic_prod_item_expr list * raw_tactic_expr
   | VernacSyntaxExtension of
       obsolete_locality * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
@@ -382,7 +379,6 @@ type vernac_expr =
   | VernacBackTo of int
 
   (* Commands *)
-  | VernacDeclareTacticDefinition of tacdef_body list
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * reference list
   | VernacHints of obsolete_locality * string list * hints_expr
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c89238d296..8d7b6a2b48 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -751,11 +751,7 @@ GEXTEND Gram
   GLOBAL: command query_command class_rawexpr;
 
   command:
-    [ [ IDENT "Ltac";
-        l = LIST1 tacdef_body SEP "with" ->
-          VernacDeclareTacticDefinition l
-
-      | IDENT "Comments"; l = LIST0 comment -> VernacComments l
+    [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
 
       (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
       | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
@@ -890,7 +886,6 @@ GEXTEND Gram
       | IDENT "Classes" ->  PrintClasses
       | IDENT "TypeClasses" -> PrintTypeClasses
       | IDENT "Instances"; qid = smart_global -> PrintInstances qid
-      | IDENT "Ltac"; qid = global -> PrintLtac qid
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
@@ -1048,10 +1043,6 @@ GEXTEND Gram
      | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
            VernacNotationAddFormat (n,s,fmt)
 
-     | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
-	 pil = LIST1 production_item; ":="; t = Tactic.tactic
-         -> VernacTacticNotation (n,pil,t)
-
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   Metasyntax.check_infix_modifiers l;
@@ -1077,9 +1068,6 @@ GEXTEND Gram
   obsolete_locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
-  tactic_level:
-    [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
-  ;
   level:
     [ [ IDENT "level"; n = natural -> NumLevel n
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
@@ -1111,10 +1099,4 @@ GEXTEND Gram
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
-  production_item:
-    [ [ s = ne_string -> TacTerm s
-      | nt = IDENT;
-        po = [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
-                   ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ]
-  ;
 END
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index eed6caea30..8df519b567 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -3,4 +3,3 @@ G_vernac
 G_prim
 G_proofs
 G_tactic
-G_ltac
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9c2f09db84..c7cb62d592 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -364,9 +364,6 @@ module Tactic =
     (* Main entry for quotations *)
     let tactic_eoi = eoi_entry tactic
 
-    (* For Ltac definition *)
-    let tacdef_body = Gram.entry_create "tactic:tacdef_body"
-
   end
 
 module Vernac_ =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7410d4e44c..35973a4d72 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -229,7 +229,6 @@ module Tactic :
     val binder_tactic : raw_tactic_expr Gram.entry
     val tactic : raw_tactic_expr Gram.entry
     val tactic_eoi : raw_tactic_expr Gram.entry
-    val tacdef_body : Vernacexpr.tacdef_body Gram.entry
   end
 
 module Vernac_ :
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 887a14d2bf..c1f5e122bd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -378,17 +378,6 @@ module Make
     | l -> spc() ++
       hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-  let print_level n =
-    if not (Int.equal n 0) then
-      spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")")
-    else
-      mt ()
-
-  let pr_grammar_tactic_rule n (_,pil,t) =
-    hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++
-             hov 0 (prlist_with_sep sep pr_production_item pil ++
-                      spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
-
   let pr_univs pl =
     match pl with
     | None -> mt ()
@@ -466,8 +455,6 @@ module Make
         keyword "Print TypeClasses"
       | PrintInstances qid ->
         keyword "Print Instances" ++ spc () ++ pr_smart_global qid
-      | PrintLtac qid ->
-        keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid
       | PrintCoercions ->
         keyword "Print Coercions"
       | PrintCoercionPaths (s,t) ->
@@ -644,8 +631,6 @@ module Make
           return (keyword "No-parsing-rule for VernacError")
 
       (* Syntax *)
-        | VernacTacticNotation (n,r,e) ->
-          return (pr_grammar_tactic_rule n ("",r,e))
         | VernacOpenCloseScope (_,(opening,sc)) ->
           return (
             keyword (if opening then "Open " else "Close ") ++
@@ -1010,29 +995,6 @@ module Make
           return (keyword "Cd" ++ pr_opt qs s)
 
         (* Commands *)
-        | VernacDeclareTacticDefinition l ->
-          let pr_tac_body tacdef_body =
-            let id, redef, body =
-              match tacdef_body with
-              | TacticDefinition ((_,id), body) -> pr_id id, false, body
-              | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
-            in
-            let idl, body =
-              match body with
-                | Tacexpr.TacFun (idl,b) -> idl,b
-                | _ -> [], body in
-            id ++
-              prlist (function None -> str " _"
-                | Some id -> spc () ++ pr_id id) idl
-            ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
-              pr_raw_tactic body
-          in
-          return (
-            hov 1
-              (keyword "Ltac" ++ spc () ++
-                 prlist_with_sep (fun () ->
-                   fnl() ++ keyword "with" ++ spc ()) pr_tac_body l)
-          )
         | VernacCreateHintDb (dbname,b) ->
           return (
             hov 1 (keyword "Create HintDb" ++ spc () ++
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index a459cd65f8..2d2ea1f8b0 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -503,9 +503,6 @@ let rec tmpp v loc =
   | VernacError _ -> xmlWithLoc loc "error" [] []
 
   (* Syntax *)
-  | VernacTacticNotation _ as x ->
-      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
   | VernacSyntaxExtension (_, ((_, name), sml)) ->
       let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
       xmlReservedNotation attrs name loc
@@ -697,7 +694,6 @@ let rec tmpp v loc =
   | VernacBackTo _ -> PCData "VernacBackTo"
 
   (* Commands *)
-  | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
   | VernacCreateHintDb _ as x -> xmlTODO loc x
   | VernacRemoveHints _ as x -> xmlTODO loc x
   | VernacHints _ as x -> xmlTODO loc x
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 97d6e1fb71..ecaf0fb7c5 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -173,13 +173,6 @@ let rec classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _ -> VtSideff [], VtLater
-    | VernacDeclareTacticDefinition l ->
-        let open Libnames in
-        let open Vernacexpr in
-        VtSideff (List.map (function
-          | TacticDefinition ((_,r),_) -> r
-          | TacticRedefinition (Ident (_,r),_) -> r
-          | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
@@ -195,7 +188,6 @@ let rec classify_vernac e =
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
     | VernacSyntaxExtension _ 
     | VernacSyntacticDefinition _
-    | VernacTacticNotation _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
diff --git a/parsing/g_ltac.ml4 b/tactics/g_ltac.ml4
index d1992c57bb..f46a670080 100644
--- a/parsing/g_ltac.ml4
+++ b/tactics/g_ltac.ml4
@@ -48,6 +48,7 @@ let new_entry name =
   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. *)
@@ -311,6 +312,7 @@ open Constrarg
 open Vernacexpr
 open Vernac_classifier
 open Goptions
+open Libnames
 
 let print_info_trace = ref None
 
@@ -370,3 +372,58 @@ VERNAC tactic_mode EXTEND VernacSolve
     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
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e5edc74222..6277a8146a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -43,176 +43,6 @@ let inToken : string -> obj =
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 (**********************************************************************)
-(* 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
-
-(**********************************************************************)
 (* Printing grammar entries                                           *)
 
 let entry_buf = Buffer.create 64
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 5d01405b27..085cc87c8b 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -15,15 +15,6 @@ open Notation_term
 
 val add_token_obj : string -> unit
 
-(** 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
-
 (** Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 44c83be46c..b2fc456d07 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -323,8 +323,7 @@ let get_info x =
 
 let assumption_message = Declare.assumption_message
 
-let (set_default_tactic, get_default_tactic, print_default_tactic) = 
-  Tactic_option.declare_tactic_option "Program tactic"
+let default_tactic = ref (Proofview.tclUNIT ())
 
 (* true = All transparent, false = Opaque if possible *)
 let proofs_transparency = ref true
@@ -895,7 +894,7 @@ let rec solve_obligation prg num tac =
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
   let () = trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
             Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
-  let _ = Pfedit.by (snd (get_default_tactic ())) in
+  let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
 
 and obligation (user_num, name, typ) tac =
@@ -924,7 +923,7 @@ and solve_obligation_by_tac prg obls i tac =
 	      | None ->
 		  match obl.obl_tac with
 		  | Some t -> t
-		  | None -> snd (get_default_tactic ())
+		  | None -> !default_tactic
 	    in
 	    let evd = Evd.from_ctx !prg.prg_ctx in
 	    let evd = Evd.update_sigma_env evd (Global.env ()) in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index e257da0161..3e99f5760b 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -54,10 +54,8 @@ type progress = (* Resolution status of a program *)
   | Remain of int  (* n obligations remaining *)
   | Dependent (* Dependent on other definitions *)
   | Defined of global_reference (* Defined as id *)
-      
-val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val get_default_tactic : unit -> locality_flag * unit Proofview.tactic
-val print_default_tactic : unit -> Pp.std_ppcmds
+
+val default_tactic : unit Proofview.tactic ref
 
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8ba5eb3f7d..bdd52d5be0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -20,7 +20,6 @@ open Tacmach
 open Constrintern
 open Prettyp
 open Printer
-open Tacinterp
 open Command
 open Goptions
 open Libnames
@@ -34,6 +33,9 @@ open Misctypes
 open Locality
 open Sigma.Notations
 
+(** TODO: make this function independent of Ltac *)
+let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
+
 let debug = false
 let prerr_endline =
   if debug then prerr_endline else fun _ -> ()
@@ -471,7 +473,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
           | None -> None
           | Some r ->
 	      let (evc,env)= get_current_context () in
- 		Some (snd (interp_redexp env evc r)) in
+ 		Some (snd (Hook.get f_interp_redexp env evc r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof locality p kind l lettop =
@@ -912,81 +914,6 @@ let vernac_restore_state file =
 (************)
 (* Commands *)
 
-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
-
-let vernac_declare_tactic_definition locality def =
-  let local = make_module_locality locality in
-  register_ltac local def
-
 let vernac_create_hintdb locality id b =
   let local = make_module_locality locality in
   Hints.create_hint_db local id full_transparent_state b
@@ -1500,8 +1427,7 @@ let vernac_check_may_eval redexp glopt rc =
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
                     Printer.pr_universe_ctx sigma uctx)
     | Some r ->
-        Tacintern.dump_glob_red_expr r;
-        let (sigma',r_interp) = interp_redexp env sigma' r in
+        let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
 	let redfun env evm c =
           let (redfun, _) = reduction_of_red_expr env r_interp in
           let evm = Sigma.Unsafe.of_evar_map evm in
@@ -1512,7 +1438,7 @@ let vernac_check_may_eval redexp glopt rc =
 
 let vernac_declare_reduction locality s r =
   let local = make_locality locality in
-  declare_red_expr local s (snd (interp_redexp (Global.env()) Evd.empty r))
+  declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
@@ -1580,7 +1506,6 @@ let vernac_print = function
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintLtac qid -> msg_notice (Tacintern.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> msg_notice (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
@@ -1820,8 +1745,6 @@ let interp ?proof ~loc locality poly c =
   | VernacError e -> raise e
 
   (* Syntax *)
-  | VernacTacticNotation (n,r,e) ->
-      Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e)
   | VernacSyntaxExtension (local,sl) ->
       vernac_syntax_extension locality local sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
@@ -1899,8 +1822,6 @@ let interp ?proof ~loc locality poly c =
   | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
 
   (* Commands *)
-  | VernacDeclareTacticDefinition def ->
-      vernac_declare_tactic_definition locality def
   | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
   | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
   | VernacHints (local,dbnames,hints) ->
@@ -1976,15 +1897,13 @@ let check_vernac_supports_locality c l =
   match l, c with
   | None, _ -> ()
   | Some _, (
-      VernacTacticNotation _
-    | VernacOpenCloseScope _
+      VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
     | VernacAssumption _ | VernacStartTheoremProof _
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
     | VernacDeclareMLModule _
-    | VernacDeclareTacticDefinition _
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
     | VernacSyntacticDefinition _
     | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4a59b1299b..4e7fa4a087 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -61,3 +61,6 @@ val vernac_end_proof :
 val with_fail : bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind
+
+val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr ->
+  Evd.evar_map * Redexpr.red_expr) Hook.t