Merge branch 'trunk' into located_switch

25 files changed, 91 insertions, 76 deletions

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index a5d9697ae..470a93f2b 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -9,7 +9,6 @@
 open Util
 open Names
 open Term
-open EConstr
 open CErrors
 open Evar_refiner
 open Tacmach
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index aa81f148e..a3310c2d8 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause
 | [ in_clause'(cl) ] -> [ cl ]
 END
 
+let local_test_lpar_id_colon =
+  let err () = raise Stream.Failure in
+  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+    (fun strm ->
+      match Util.stream_nth 0 strm with
+        | Tok.KEYWORD "(" ->
+            (match Util.stream_nth 1 strm with
+              | Tok.IDENT _ ->
+                  (match Util.stream_nth 2 strm with
+                    | Tok.KEYWORD ":" -> ()
+                    | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
+let pr_lpar_id_colon _ _ _ _ = mt ()
+
+ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
+| [ local_test_lpar_id_colon(x) ] -> [ () ]
+END
+
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
 let pr_r_nat_field natf =
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7d4bccfad..9b4167512 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,6 +67,10 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 9d50b6e6f..cbd8a7f0f 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -21,7 +21,6 @@ open Tacexpr
 open Glob_ops
 open CErrors
 open Util
-open Evd
 open Termops
 open Equality
 open Misctypes
@@ -52,8 +51,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
-let clause = Pltac.clause_dft_concl
-
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
@@ -466,7 +463,7 @@ open Evar_tactics
 (* TODO: add support for some test similar to g_constr.name_colon so that
    expressions like "evar (list A)" do not raise a syntax error *)
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
@@ -815,6 +812,19 @@ TACTIC EXTEND destauto
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
+(**********************************************************************)
+
+(**********************************************************************)
+(* A version of abstract constructing transparent terms               *)
+(* Introduced by Jason Gross and Benjamin Delaware in June 2016       *)
+(**********************************************************************)
+
+TACTIC EXTEND transparent_abstract
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+END
 
 (* ********************************************************************* *)
 
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfa8331ff..50e8255a6 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,7 +16,6 @@ open Pcoq.Constr
 open Pltac
 open Hints
 open Tacexpr
-open Proofview.Notations
 open Names
 
 DECLARE PLUGIN "g_auto"
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 40f30c794..23ce368ee 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,9 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Misctypes
 open Class_tactics
-open Pltac
 open Stdarg
 open Tacarg
 open Names
@@ -85,7 +83,7 @@ TACTIC EXTEND not_evar
 END
 
 TACTIC EXTEND is_ground
-  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
+  [ "is_ground" constr(ty) ] -> [ is_ground ty ]
 END
 
 TACTIC EXTEND autoapply
@@ -95,7 +93,6 @@ END
 (** TODO: DEPRECATE *)
 (* A progress test that allows to see if the evars have changed *)
 open Term
-open Proofview.Goal
 open Proofview.Notations
 
 let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 5fc22cb4a..b5028190f 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -460,7 +460,9 @@ END
 
 let pr_ltac_production_item = function
 | Tacentries.TacTerm s -> quote (str s)
-| Tacentries.TacNonTerm (_, ((arg, sep), id)) ->
+| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg
+| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false
+| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) ->
   let sep = match sep with
   | None -> mt ()
   | Some sep -> str "," ++ spc () ++ quote (str sep)
@@ -470,7 +472,9 @@ let pr_ltac_production_item = function
 VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
 | [ string(s) ] -> [ Tacentries.TacTerm s ]
 | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
-  [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), p)) ]
+  [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ]
+| [ ident(nt) ] ->
+  [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ]
 END
 
 VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b4a0e46ae..5adf8475a 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,7 @@ open Glob_term
 open Geninterp
 open Extraargs
 open Tacmach
-open Tacticals
+open Proofview.Notations
 open Rewrite
 open Stdarg
 open Pcoq.Vernac_
@@ -123,15 +123,19 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
-  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id'} when Id.equal id' id -> true | _ -> false in
-    Tacticals.onAllHypsAndConcl
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
+    Tacticals.New.tclMAP
       (fun cl ->
         match cl with
-          | Some id when is_tac id -> tclIDTAC
-          | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
+          | Some id when is_tac id -> Tacticals.New.tclIDTAC
+          | _ -> cl_rewrite_clause c o AllOccurrences cl)
+      (None :: List.map (fun id -> Some id) hyps)
+  end }
 
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
 END
 
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 60deb443a..257100b01 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq =
         | _ -> err ())
 
 (* idem for (x:t) *)
-let test_lpar_id_colon =
-  Gram.Entry.of_parser "lpar_id_colon"
-    (fun strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae..7e979d269 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Pcoq
 
 (* Main entry for extensions *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 87b79374e..75ab1c5ee 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of ('a * Names.Id.t) Loc.located
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
 
 type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
@@ -250,7 +250,7 @@ type 'a extra_genarg_printer =
   let pr_alias_key key =
     try
       let prods = (KNmap.find key !prnotation_tab).pptac_prods in
-      let rec pr = function
+      let pr = function
       | TacTerm s -> primitive s
       | TacNonTerm (_, (symb, _)) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
       in
@@ -264,8 +264,9 @@ type 'a extra_genarg_printer =
       let rec pack prods args = match prods, args with
       | [], [] -> []
       | TacTerm s :: prods, args -> TacTerm s :: pack prods args
-      | TacNonTerm (loc, (symb, id)) :: prods, arg :: args ->
-        TacNonTerm (loc, ((symb, arg), id)) :: pack prods args
+      | TacNonTerm (_, (_, None)) :: prods, args -> pack prods args
+      | TacNonTerm (loc, (symb, (Some _ as ido))) :: prods, arg :: args ->
+        TacNonTerm (loc, ((symb, arg), ido)) :: pack prods args
       | _ -> raise Not_found
       in
       let prods = pack pp.pptac_prods l in
@@ -314,7 +315,7 @@ type 'a extra_genarg_printer =
   | Extend.Uentry _ | Extend.Uentryl _ ->
     str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
 
-  let rec pr_targ prtac symb arg = match symb with
+  let pr_targ prtac symb arg = match symb with
   | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
     prtac (1, Any) arg
   | Extend.Uentryl (_, l) -> prtac (l, Any) arg
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 23570392d..19bdf2d49 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -21,7 +21,7 @@ open Ppextend
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of ('a * Names.Id.t) Loc.located
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) ->
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index eb97a0e70..c5dbc8a14 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -136,7 +136,6 @@ let feedback_results results =
 let format_sec x = (Printf.sprintf "%.3fs" x)
 let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
 let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
-let padr n s = str s ++ ws (max 0 (n - utf8_length s))
 let padr_with c n s =
   let ulength = utf8_length s in
   str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2ef435b6b..e8c9f4eba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
 open Vars
 open Reduction
 open Tacticals.New
-open Tacmach
 open Tactics
 open Pretype_errors
 open Typeclasses
@@ -39,7 +38,7 @@ open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 
 (** Typeclass-based generalized rewriting. *)
 
@@ -2196,7 +2195,8 @@ let setoid_transitivity c =
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
-  Proofview.V82.tactic (fun gl ->
+  let open Tacmach.New in
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let ctype = pf_unsafe_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum sigma ctype in
@@ -2210,11 +2210,10 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-   Proofview.V82.of_tactic
     (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
       (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
-      gl)
+  end }
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 7a20838a2..6683d753b 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -14,7 +14,6 @@ open Constrexpr
 open Tacexpr
 open Misctypes
 open Evd
-open Proof_type
 open Tacinterp
 
 (** TODO: document and clean me! *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index b09672a12..9883c03c4 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open EConstr
 open Misctypes
 open Pattern
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 1de4024fd..4d7b0f929 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -15,14 +15,13 @@ open Genarg
 open Extend
 open Pcoq
 open Egramml
-open Egramcoq
 open Vernacexpr
 open Libnames
 open Nameops
 
 type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of ('a * Names.Id.t) Loc.located
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
 
 type raw_argument = string * string option
 type argument = Genarg.ArgT.any Extend.user_symbol
@@ -88,9 +87,6 @@ let rec parse_user_entry s sep =
   else
     Uentry s
 
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
 let interp_entry_name interp symb =
   let rec eval = function
   | Ulist1 e -> Ulist1 (eval e)
@@ -178,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let map = function
   | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, (s, _)) ->
+  | TacNonTerm (loc, (s, ido)) ->
     let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
-    GramNonTerminal (Loc.tag ?loc (typ, e))
+    GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e))
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
@@ -206,7 +202,7 @@ let register_tactic_notation_entry name entry =
 
 let interp_prod_item = function
   | TacTerm s -> TacTerm s
-  | TacNonTerm (loc, ((nt, sep), id)) ->
+  | TacNonTerm (loc, ((nt, sep), ido)) ->
     let symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
@@ -224,7 +220,7 @@ let interp_prod_item = function
       end
     in
     let symbol = interp_entry_name interp symbol in
-    TacNonTerm (loc, (symbol, id))
+    TacNonTerm (loc, (symbol, ido))
 
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -300,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
 
 let cons_production_parameter = function
 | TacTerm _ -> None
-| TacNonTerm (_, (_, id)) -> Some id
+| TacNonTerm (_, (_, ido)) -> ido
 
 let add_glob_tactic_notation local ~level prods forml ids tac =
   let parule = {
@@ -320,7 +316,7 @@ 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 prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local n prods false ids tac
+  add_glob_tactic_notation local ~level:n prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
@@ -366,7 +362,7 @@ let add_ml_tactic_notation name ~level prods =
     let open Tacexpr in
     let get_id = function
     | TacTerm s -> None
-    | TacNonTerm (_, (_, id)) -> Some id
+    | TacNonTerm (_, (_, ido)) -> ido
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 48598f7f4..07aa7ad82 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
 
 type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of ('a * Names.Id.t) Loc.located
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
 
 type raw_argument = string * string option
 (** An argument type as provided in Tactic notations, i.e. a string like
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223a..d1e2a7bbe 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Genarg
 open Names
 open Tacexpr
 open Geninterp
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 8751a14c7..da7f11472 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -116,12 +116,6 @@ let intern_constr_reference strict ist = function
       CAst.make @@ GRef (locate_global_with_alias lqid,None), 
 	if strict then None else Some (CAst.make @@ CRef (r,None))
 
-let intern_move_location ist = function
-  | MoveAfter id -> MoveAfter (intern_hyp ist id)
-  | MoveBefore id -> MoveBefore (intern_hyp ist id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 91bc46fe7..f63c38d4f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -25,7 +25,6 @@ open Refiner
 open Tacmach.New
 open Tactic_debug
 open Constrexpr
-open Term
 open Termops
 open Tacexpr
 open Genarg
@@ -434,12 +433,6 @@ let interp_hyp_list_as_list ist env sigma (loc,id as x) =
 let interp_hyp_list ist env sigma l =
   List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l)
 
-let interp_move_location ist env sigma = function
-  | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id)
-  | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
   | ArgVar (loc, id) ->
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 6cd5a63b3..2ec45312e 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Tactic_debug
-open Term
 open EConstr
 open Tacexpr
 open Genarg
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index f04495c61..20a2013a5 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
 let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
 let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
 
+let batch = ref false
+
+open Goptions
+
+let _ =
+  declare_bool_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "Ltac batch debug";
+      optkey   = ["Ltac";"Batch";"Debug"];
+      optread  = (fun () -> !batch);
+      optwrite = (fun x -> batch := x) }
+
 let rec drop_spaces inst i =
   if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
   else i
@@ -150,6 +163,7 @@ let rec prompt level =
   begin
     let open Proofview.NonLogical in
     Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+    if Pervasives.(!batch) then return (DebugOn (level+1)) else
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 38d8caca6..ac35464c4 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -10,7 +10,6 @@ open Environ
 open Pattern
 open Names
 open Tacexpr
-open Term
 open EConstr
 open Evd
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index df186cc46..1e46c253d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -10,7 +10,6 @@ open Term
 open EConstr
 open Hipattern
 open Names
-open Pp
 open Geninterp
 open Misctypes
 open Tacexpr
@@ -241,7 +240,7 @@ let tauto_uniform_unit_flags = {
 }
 
 (* This is the compatibility mode (not used) *)
-let tauto_legacy_flags = {
+let _tauto_legacy_flags = {
   binary_mode = true;
   binary_mode_bugged_detection = true;
   strict_in_contravariant_hyp = true;