diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index ed22ab0e1..ec96a887d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -49,7 +49,7 @@ let check_no_metas clenv ccl = let var_occurs_in_pf gl id = let env = pf_env gl in - occur_var env id (pf_concl gl) or + occur_var env id (pf_concl gl) || List.exists (occur_var_in_decl env id) (pf_hyps gl) (* [make_inv_predicate (ity,args) C] |