diff options
| -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 6ba8a51120..291c089784 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 0000000000..0533d21e0c --- /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. |