From f39543a752d05e5661749bbc3f221d75e525b3b4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 03:10:54 +0100
Subject: Moving Tactic_debug to Hightactic.

---
 dev/printers.mllib        |  1 -
 tactics/hightactics.mllib |  1 +
 tactics/tacinterp.ml      |  2 +-
 tactics/tactic_debug.ml   | 20 ++++++++++++++++----
 tactics/tactic_debug.mli  |  4 ++--
 tactics/tactics.mllib     |  1 -
 toplevel/cerrors.ml       | 28 +++++++++++++---------------
 toplevel/cerrors.mli      |  1 +
 8 files changed, 34 insertions(+), 24 deletions(-)

diff --git a/dev/printers.mllib b/dev/printers.mllib
index a3ba42ba78..aad56f586b 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -201,7 +201,6 @@ Egramml
 Egramcoq
 Tacsubst
 Tacenv
-Tactic_debug
 Trie
 Dn
 Btermdn
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 468b938b6a..76455f4ac3 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,4 @@
+Tactic_debug
 Tacintern
 Tacentries
 Tacinterp
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6bf0e2aa73..5dab244afa 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -365,7 +365,7 @@ let debugging_exception_step ist signal_anomaly e pp =
     if signal_anomaly then explain_logic_error
     else explain_logic_error_no_anomaly in
   debugging_step ist (fun () ->
-    pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e)
+    pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
 let error_ltac_variable loc id env v s =
    user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml
index e991eb86dc..d661f9677c 100644
--- a/tactics/tactic_debug.ml
+++ b/tactics/tactic_debug.ml
@@ -14,6 +14,7 @@ open Termops
 open Nameops
 open Proofview.Notations
 
+
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
 let prtac x =
@@ -34,9 +35,11 @@ type debug_info =
   | DebugOff
 
 (* An exception handler *)
-let explain_logic_error = ref (fun e -> mt())
+let explain_logic_error e =
+  Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
 
-let explain_logic_error_no_anomaly = ref (fun e -> mt())
+let explain_logic_error_no_anomaly e =
+  Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
 
 let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
 let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
@@ -202,7 +205,7 @@ let debug_prompt lev tac f =
         (Proofview.tclLIFT begin
           (skip:=0) >> (skipped:=0) >>
             if Logic.catchable_exception reraise then
-              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise)
+              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise)
             else return ()
         end)
         (Proofview.tclZERO ~info reraise)
@@ -304,7 +307,7 @@ let db_logic_failure debug err =
   is_debug debug >>= fun db ->
   if db then
   begin
-    msg_tac_debug (Pervasives.(!) explain_logic_error err) >>
+    msg_tac_debug (explain_logic_error err) >>
     msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
            str "Let us try the next one...")
   end
@@ -398,3 +401,12 @@ let extract_ltac_trace trace eloc =
         | [] -> Loc.ghost in
         aux trace in
     None, best_loc
+
+let get_ltac_trace (_, info) =
+  let ltac_trace = Exninfo.get info ltac_trace_info in
+  let loc = Option.default Loc.ghost (Loc.get_loc info) in
+  match ltac_trace with
+  | None -> None
+  | Some trace -> Some (extract_ltac_trace trace loc)
+
+let () = Cerrors.register_additional_error_info get_ltac_trace
diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli
index 523398e75a..520fb41eff 100644
--- a/tactics/tactic_debug.mli
+++ b/tactics/tactic_debug.mli
@@ -61,13 +61,13 @@ val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
 val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
 
 (** An exception handler *)
-val explain_logic_error: (exn -> Pp.std_ppcmds) ref
+val explain_logic_error: exn -> Pp.std_ppcmds
 
 (** For use in the Ltac debugger: some exception that are usually
    consider anomalies are acceptable because they are caught later in
    the process that is being debugged.  One should not require
    from users that they report these anomalies. *)
-val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
+val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds
 
 (** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index b495a885f8..c290ce228c 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -20,5 +20,4 @@ Tacenv
 Hints
 Auto
 Tactic_matching
-Tactic_debug
 Term_dnet
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0b8edd91c1..4f3ffbcaee 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -110,6 +110,11 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
+let additional_error_info = ref []
+
+let register_additional_error_info f =
+  additional_error_info := f :: !additional_error_info
+
 let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error with_header (exc, info) in
@@ -120,19 +125,12 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
       let err = Errors.make_anomaly msg in
       Util.iraise (err, info)
   in
-  let ltac_trace = Exninfo.get info Tactic_debug.ltac_trace_info in
-  let loc = Option.default Loc.ghost (Loc.get_loc info) in
-  match ltac_trace with
+  let e' =
+    try Some (CList.find_map (fun f -> f e) !additional_error_info)
+    with _ -> None
+  in
+  match e' with
   | None -> e
-  | Some trace ->
-    let (e, info) = e in
-    match Tactic_debug.extract_ltac_trace trace loc with
-    | None, loc -> (e, Loc.add_loc info loc)
-    | Some msg, loc ->
-      (EvaluatedError (msg, Some e), Loc.add_loc info loc)
-
-let _ = Tactic_debug.explain_logic_error :=
-  (fun e -> Errors.print (fst (process_vernac_interp_error (e, Exninfo.null))))
-
-let _ = Tactic_debug.explain_logic_error_no_anomaly :=
-  (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null))))
+  | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc)
+  | Some (Some msg, loc) ->
+    (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc)
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 68c46010b5..a0e3e3c199 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -19,3 +19,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> U
 
 val explain_exn_default : exn -> Pp.std_ppcmds
 
+val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit
-- 
cgit v1.2.3


From 6de9f13ba666250ea397c7db1d9d37075a9dc1c2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 03:37:55 +0100
Subject: Moving Tacenv to Hightactics.

---
 dev/printers.mllib        | 1 -
 tactics/hightactics.mllib | 1 +
 tactics/tactics.mllib     | 1 -
 3 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/dev/printers.mllib b/dev/printers.mllib
index aad56f586b..9f25ba55e7 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -200,7 +200,6 @@ Ppdecl_proof
 Egramml
 Egramcoq
 Tacsubst
-Tacenv
 Trie
 Dn
 Btermdn
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 76455f4ac3..2bd748414c 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,4 @@
+Tacenv
 Tactic_debug
 Tacintern
 Tacentries
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index c290ce228c..038bb59f09 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -16,7 +16,6 @@ Inv
 Leminv
 Tacsubst
 Taccoerce
-Tacenv
 Hints
 Auto
 Tactic_matching
-- 
cgit v1.2.3


From dc7b77f09fe5e59e6e48486d9a8c0bdc6acf83b7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 16:59:15 +0100
Subject: Adding a new Ltac generic argument for forced tactics returing unit.

---
 interp/constrarg.ml  | 2 ++
 interp/constrarg.mli | 5 +++++
 parsing/pcoq.ml      | 1 +
 printing/pptactic.ml | 5 +++++
 tactics/tacintern.ml | 1 +
 tactics/tacinterp.ml | 4 ++++
 tactics/tacsubst.ml  | 1 +
 7 files changed, 19 insertions(+)

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 81e942d828..46be0b8a1f 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -28,6 +28,8 @@ let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
   Genarg.make0 "tactic"
 
+let wit_ltac = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
+
 let wit_ident =
   Genarg.make0 "ident"
 
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 1197b85a25..d38b1183c5 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -71,6 +71,11 @@ val wit_red_expr :
 
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
 
+(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
+    toplevel interpretation. The one of [wit_ltac] forces the tactic and
+    discards the result. *)
+val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
+
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
 
 (** Aliases for compatibility *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index c7cb62d592..207b43064c 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -881,5 +881,6 @@ let () =
 (*   Grammar.register0 wit_hyp_location_flag; *)
   Grammar.register0 wit_red_expr (Tactic.red_expr);
   Grammar.register0 wit_tactic (Tactic.tactic);
+  Grammar.register0 wit_ltac (Tactic.tactic);
   Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl);
   ()
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index d99a5f0d89..982c18ec61 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1415,6 +1415,11 @@ let () =
   let printer _ _ prtac = prtac (0, E) in
   declare_extra_genarg_pprule wit_tactic printer printer printer
 
+let () =
+  let pr_unit _ _ _ () = str "()" in
+  let printer _ _ prtac = prtac (0, E) in
+  declare_extra_genarg_pprule wit_ltac printer printer pr_unit
+
 module Richpp = struct
 
   include Make (Ppconstr.Richpp) (struct
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 89dc843cb8..a75805b4f8 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -795,6 +795,7 @@ let () =
   Genintern.register_intern0 wit_ident intern_ident';
   Genintern.register_intern0 wit_var (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
+  Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
   Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c));
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5dab244afa..8afc73526e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2143,6 +2143,10 @@ let () =
   let interp ist tac = Ftactic.return (Value.of_closure ist tac) in
   Geninterp.register_interp0 wit_tactic interp
 
+let () =
+  let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
+  Geninterp.register_interp0 wit_ltac interp
+
 let () =
   Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
     Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 55941c1ca6..4059877b75 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -299,6 +299,7 @@ let () =
   Genintern.register_subst0 wit_var (fun _ v -> v);
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
+  Genintern.register_subst0 wit_ltac subst_tactic;
   Genintern.register_subst0 wit_constr subst_glob_constr;
   Genintern.register_subst0 wit_sort (fun _ v -> v);
   Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
-- 
cgit v1.2.3


From bc1d2825b7f7d0fc828b4ed99cee8ce62c646148 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 23:00:46 +0100
Subject: Relying on generic arguments to represent Extern hints.

---
 tactics/auto.ml      | 10 +++++++---
 tactics/auto.mli     |  5 +----
 tactics/hints.ml     |  7 ++++---
 tactics/hints.mli    |  2 +-
 tactics/tacinterp.ml |  6 ------
 5 files changed, 13 insertions(+), 17 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 761c41da6f..fc6ff03b4b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -140,8 +140,6 @@ si après Intros la conclusion matche le pattern.
 
 (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
-let (forward_interp_tactic, extern_interp) = Hook.make ()
-
 let conclPattern concl pat tac =
   let constr_bindings env sigma =
     match pat with
@@ -156,7 +154,13 @@ let conclPattern concl pat tac =
      let env = Proofview.Goal.env gl in
      let sigma = Tacmach.New.project gl in
        constr_bindings env sigma >>= fun constr_bindings ->
-     Hook.get forward_interp_tactic constr_bindings tac
+     let open Genarg in
+     let open Geninterp in
+     let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in
+     let fold id c accu = Id.Map.add id (inj c) accu in
+     let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
+     let ist = { lfun; extra = TacStore.empty } in
+     Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
   end }
 
 (***********************************************************)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index cd2de99be5..8c4f359041 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -13,9 +13,6 @@ open Pattern
 open Decl_kinds
 open Hints
 
-val extern_interp :
-  (patvar_map -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic) Hook.t
-
 (** Auto and related automation tactics *)
 
 val priority : ('a * full_hint) list -> ('a * full_hint) list
@@ -35,7 +32,7 @@ val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clause
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
-val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic
+val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argument -> unit Proofview.tactic
 
 (** The Auto tactic *)
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e5abad6863..b2104ba433 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -76,7 +76,7 @@ type 'a hint_ast =
   | Give_exact of 'a
   | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
-  | Extern     of glob_tactic_expr       (* Hint Extern *)
+  | Extern     of Genarg.glob_generic_argument (* Hint Extern *)
 
 type hints_path_atom = 
   | PathHints of global_reference list
@@ -749,6 +749,7 @@ let make_unfold eref =
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
+  let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
    { pri = pri;
@@ -900,7 +901,7 @@ let subst_autohint (subst, obj) =
           let ref' = subst_evaluable_reference subst ref in
           if ref==ref' then data.code.obj else Unfold_nth ref'
       | Extern tac ->
-	  let tac' = Tacsubst.subst_tactic subst tac in
+	  let tac' = Genintern.generic_substitute subst tac in
 	  if tac==tac' then data.code.obj else Extern tac'
     in
     let name' = subst_path_atom subst data.name in
@@ -1219,7 +1220,7 @@ let pr_hint h = match h.obj with
           env
         with e when Errors.noncritical e -> Global.env ()
       in
-      (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
+      (str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
 
 let pr_id_hint (id, v) =
   (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 3e08060f81..df9d792121 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -33,7 +33,7 @@ type 'a hint_ast =
   | Give_exact of 'a
   | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
-  | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
+  | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
 type hint
 type raw_hint = constr * types * Univ.universe_context_set
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8afc73526e..4506f81596 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2179,12 +2179,6 @@ let _ =
   in
   Hook.set Pretyping.genarg_interp_hook eval
 
-let _ = Hook.set Auto.extern_interp
-  (fun l ->
-    let lfun = Id.Map.map (fun c -> Value.of_constr c) l in
-    let ist = { (default_ist ()) with lfun; } in
-    interp_tactic ist)
-
 (** Used in tactic extension **)
 
 let dummy_id = Id.of_string "_"
-- 
cgit v1.2.3


From 87e27056beee0f7b63326d0a1cb3f68249539bee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 23:24:10 +0100
Subject: Moving Tacsubst to hightactics.

---
 tactics/hightactics.mllib | 1 +
 tactics/tactics.mllib     | 1 -
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 2bd748414c..7987d774d1 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,4 @@
+Tacsubst
 Tacenv
 Tactic_debug
 Tacintern
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 038bb59f09..cb327e52c1 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -14,7 +14,6 @@ Equality
 Contradiction
 Inv
 Leminv
-Tacsubst
 Taccoerce
 Hints
 Auto
-- 
cgit v1.2.3