diff options
| author | Maxime Dénès | 2017-05-05 15:39:17 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-05 15:39:17 +0200 |
| commit | 5548e5f6bc5446f7541cfc7d93b0b47e4b751e86 (patch) | |
| tree | ebf3e269042cf4ea74193576681e7e9c37a60fb4 | |
| parent | 1b4b828c3045263aee55ac19e7b9ba45a4743af2 (diff) | |
Remove unused open.
| -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) *) |