diff options
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index e193b20a97..d971c0c1e0 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -34,7 +34,8 @@ let is_unit ist = <:tactic<Fail>> let is_conj ist = - if (is_conjunction (List.assoc 1 ist.lmatch)) then + let ind=(List.assoc 1 ist.lmatch) in + if (is_conjunction ind) && (is_nodep_ind ind) then <:tactic<Idtac>> else <:tactic<Fail>> |