aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-15 16:27:37 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-15 16:28:34 +0200
commitc3b9a7bf9fcd162628ce6a2a544652ca096cfe54 (patch)
tree28459c0899c47ee8f2229c602cab3d1637985f68
parent7c047370dc9032e3ded3365a45de5b92e7c9033f (diff)
Fix bug #5145: Anomaly: index to an anonymous variable.
When printing evar constraints, we ensure that every variable from the rel context has a name.
-rw-r--r--engine/evd.ml1
-rw-r--r--test-suite/bugs/closed/5145.v10
2 files changed, 11 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 6ba8a5112..291c08978 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1411,6 +1411,7 @@ let print_env_short env =
let pr_evar_constraints pbs =
let pr_evconstr (pbty, env, t1, t2) =
+ let env = Namegen.make_all_name_different env in
print_env_short env ++ spc () ++ str "|-" ++ spc () ++
print_constr_env env t1 ++ spc () ++
str (match pbty with
diff --git a/test-suite/bugs/closed/5145.v b/test-suite/bugs/closed/5145.v
new file mode 100644
index 000000000..0533d21e0
--- /dev/null
+++ b/test-suite/bugs/closed/5145.v
@@ -0,0 +1,10 @@
+Class instructions :=
+ {
+ W : Type;
+ ldi : nat -> W
+ }.
+
+Fail Definition foo :=
+ let y2 := ldi 0 in
+ let '(CF, _) := (true, 0) in
+ y2.