aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4ebe089e96..a4269b17c6 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -240,7 +240,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
let eqclause =
if metas then eqclause
- else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
+ else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
in
let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function