diff options
| -rw-r--r-- | tactics/eqdecide.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 472cd8f22b..641929a77b 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -67,7 +67,6 @@ let choose_noteq eqonleft = left_with_bindings false Misctypes.NoBindings open Sigma.Notations -open Context.Rel.Declaration (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) |