From ef5551e4ca73a93c0820f03ac702ee96e5e7b431 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 30 Sep 2007 19:02:14 +0000
Subject: Ajout infos de débogage de "universe inconsistency" quand option Set 
  Printing Universes est active. Ajout de l'option "using" à la tactique non
 documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto
 decomp" avec des   principes élémentaires tels que le dépliage de "iff".
 Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts.

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

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index f99ce1a88c..d68d125bd7 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -160,7 +160,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacDestructHyp of (bool * identifier located)
   | TacDestructConcl
   | TacSuperAuto of (int option * reference list * bool * bool)
-  | TacDAuto of int or_var option * int option
+  | TacDAuto of int or_var option * int option * 'constr list
 
   (* Context management *)
   | TacClear of bool * 'id list
-- 
cgit v1.2.3