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

(limited to 'interp/constrarg.ml')

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