test-suite/bugs/closed/bug_11552.v


1
2
3
4
5
6
7
8
9

From Ltac2 Require Import Ltac2.

Goal True.
Proof.
  Search unit.
  (* Unbound constructor Search *)
  Check tt.
  (* Unbound constructor Check *)
Abort.