diff options
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 1c75059b8..f7713f015 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -235,17 +235,8 @@ let rec tauto_intuit t_reduce solver ist = $t_solver ) >> - (* The unfolding of "iff" below is a priori too strong since it - reduces all occurrences in subterms even if not necessary to do - so. However we cannot renounce to them (even with iff dealt with - in "simplif") w/o breaking some intro naming. This is because, a - "and" or an "iff" can arrive in the scope of an inductive type, - say "{x:A|P x}" and "case"ing on a such an hypothesis will name P - x "a" or "i" depending on whether "P" is an "and" or a "iff". - (idem for "not" if "simplif" has a primitive treatment *) - let reduction_not _ist = - <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >> + <:tactic< unfold Coq.Init.Logic.not in * >> let t_reduction_not = tacticIn reduction_not |