From 8ab38a81abd3df8b94ca133a6a679d2504eb577a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 27 Jan 2004 13:55:56 +0000
Subject: Bug (destruct/induction ne savent pas traiter le cas non atomique
 avec paramètres)

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a1d6a0435c..687c5ad07a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1235,7 +1235,7 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl =
       let tmptyp0 = pf_get_hyp_typ gl hyp0 in
       (* If argl <> [], we expect typ0 not to be quantified, in order to
          avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
-      let indtyp = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
+      let indtyp = pf_apply reduce_to_atomic_ref gl indref tmptyp0 in
       let argl = snd (decompose_app indtyp) in
       let c = List.nth argl (i-1) in
       match kind_of_term c with
-- 
cgit v1.2.3