diff options
| -rw-r--r-- | tactics/rewrite.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 6a81f9ada9..c792367c3b 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1648,8 +1648,7 @@ let setoid_transitivity c gl = let proof = get_transitive_proof env evm car rel in match c with | None -> eapply proof - | Some c -> - apply_with_bindings (proof,Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ])) + | Some c -> apply_with_bindings (proof,Rawterm.ImplicitBindings [ c ])) (transitivity_red true c) let setoid_symmetry_in id gl = |