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 +++++
 2 files changed, 7 insertions(+)

(limited to 'interp')

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 *)
-- 
cgit v1.2.3