aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/rewrite.ml')
-rw-r--r--plugins/ltac/rewrite.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 321b05b97c..76c7e0bb9e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1559,7 +1559,7 @@ let assert_replacing id newt tac =
if Id.equal n id then ev' else mkVar n
in
let (e, _) = destEvar sigma ev in
- (sigma, mkEvar (e, Array.map_of_list map nc))
+ (sigma, mkEvar (e, List.map map nc))
end
end in
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)