test-suite/bugs/closed/7113.v


1
2
3
4
5
6
7
8
9
10

Require Import Program.Tactics.
Section visibility.

  (* used to anomaly *)
  Program Let Fixpoint ev' (n : nat) : bool := _.
  Next Obligation. exact true. Qed.

  Check ev'.
End visibility.
Fail Check ev'.