diff options
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 14a9ae9c2..d6e51a15d 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -65,7 +65,7 @@ let contradiction_context gl = let is_negation_of env sigma typ t = match kind_of_term (whd_betadeltaiota env sigma t) with - | Prod (na,t,u) -> is_empty_type u & is_conv_leq env sigma typ t + | Prod (na,t,u) -> is_empty_type u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) gl = |