From 78692ad28ded4f94d5cf7e54240fe0b71d1be282 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 30 Jul 2014 12:12:21 +0200
Subject: Add [numgoal] to Ltac.

---
 intf/tacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 940aa6d1cb..d319081145 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -186,6 +186,7 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg =
   | TacFreshId of string or_var list
   | Tacexp of ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr
   | TacPretype of 'trm
+  | TacNumgoals
 
 (** Generic ltac expressions.
     't : terms, 'p : patterns, 'c : constants, 'i : inductive,
-- 
cgit v1.2.3