aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--pretyping/evd.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 09e34c6aa4..902ec9f154 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -242,7 +242,8 @@ let make_evar_instance_array info args =
| true :: filter, (id, _, _) :: ctxt ->
if i < len then
let c = Array.unsafe_get args i in
- (id, c) :: instrec filter ctxt (succ i)
+ if isVarId id c then instrec filter ctxt (succ i)
+ else (id, c) :: instrec filter ctxt (succ i)
else instance_mismatch ()
| _ -> instance_mismatch ()
in