diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |