diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 587890ca5f..e5a657e697 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -132,9 +132,7 @@ let make_inv_predicate env sigma ind id status concl = abstract_list_all env sigma p concl (realargs@[VAR id]) in let hyps,_ = decompose_lam pred in - let c3 = - whd_beta env sigma - (applist (pred,rel_list nrealargs (nrealargs +1))) + let c3 = whd_beta (applist (pred,rel_list nrealargs (nrealargs +1))) in (hyps,c3) in |