aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/interactive/Evar.v
blob: 50c5bba0f09456f393a30810dae4060e4318cf4e (plain)
1
2
3
4
5
6
(* Check that no toplevel "unresolved evar" flees through Declare
   Implicit Tactic support (bug #1229) *)

Goal True.
(* should raise an error, not an anomaly *)
set (x := _).