From aa27ea16ab398eda93bdccc9c82b163ba1e23100 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 14 Oct 2002 14:14:00 +0000
Subject: L'application de ltac attend une référence; meilleure protection
 contre les erreurs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index eefee41f5..b63588aaa 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -209,7 +209,8 @@ and ('constr,'cst,'ind,'id) gen_tactic_arg =
   | ConstrMayEval  of 'constr may_eval
   | Reference      of reference_expr
   | Integer        of int
-  | TacCall of loc * ('constr,'cst,'ind,'id) gen_tactic_arg * ('constr,'cst,'ind,'id) gen_tactic_arg list
+  | TacCall        of loc *
+      reference_expr * ('constr,'cst,'ind,'id) gen_tactic_arg list
   | Tacexp of raw_tactic_expr
 
 type raw_atomic_tactic_expr =
-- 
cgit v1.2.3