diff options
author | 2016-10-15 16:27:37 +0200 | |
---|---|---|
committer | 2016-10-15 16:28:34 +0200 | |
commit | c3b9a7bf9fcd162628ce6a2a544652ca096cfe54 (patch) | |
tree | 28459c0899c47ee8f2229c602cab3d1637985f68 | |
parent | 7c047370dc9032e3ded3365a45de5b92e7c9033f (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.ml | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/5145.v | 10 |
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. |