diff options
| -rw-r--r-- | tactics/auto.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 1a179ecb8b..fc9c63b68e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -201,7 +201,8 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) = match kind_of_term cty with | IsProd _ -> let ce = mk_clenv_from () (c,cty) in - let pat = Pattern.pattern_of_constr (clenv_template_type ce).rebus in + let c' = (clenv_template_type ce).rebus in + let pat = Pattern.pattern_of_constr (whd_betaiota c') in let hd = (try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry") in let nmiss = |