From 8b276e32141188c9ace282cf24f733b2e0f1ec1d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 25 Jan 2002 09:29:52 +0000
Subject: Bug calcul de la signature incorrecte en présence de letin

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

diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2451a89794..bb3aa3761d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -123,7 +123,7 @@ val elimination_sort_of_goal : goal sigma -> sorts_family
 (*i val suff              : goal sigma -> constr -> string i*)
 
 val general_elim_then_using :
-  constr ->  (inductive -> int -> bool list) -> 
+  constr ->  (inductive -> bool list array) -> 
     (branch_args -> tactic) -> constr option -> 
       (arg_bindings * arg_bindings) -> constr -> tactic
 	  
-- 
cgit v1.2.3