From 1e095dd3f8b61a50dfd19f72d12e37a26a64435a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 May 2005 12:48:57 +0000
Subject: Allow auto to have a parametric argument (wish #967)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7019 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 3d060a8a3f..7ee45f67de 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -148,12 +148,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Automation tactics *)
   | TacTrivial of string list option
-  | TacAuto of int option * string list option
+  | TacAuto of int or_var option * string list option
   | TacAutoTDB of int option
   | TacDestructHyp of (bool * identifier located)
   | TacDestructConcl
   | TacSuperAuto of (int option * reference list * bool * bool)
-  | TacDAuto of int option * int option
+  | TacDAuto of int or_var option * int option
 
   (* Context management *)
   | TacClear of bool * 'id list
-- 
cgit v1.2.3