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

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a1d6a0435..687c5ad07 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