test-suite/interactive/Evar.v


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 := _).