aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_2995.v
blob: 1a4d7e5040b8db991b7d410a9a832907f510ab17 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Module Type Interface.
  Parameter error: nat.
End Interface.

Module Implementation <: Interface.
  Definition t := bool.
  Definition error: t := false.
Fail End Implementation.
(* A UserError here is expected, not an uncaught Not_found *)

 Reset error.
 Definition error := 0.
End Implementation.