diff options
Diffstat (limited to 'test-suite/bugs/closed/4095.v')
-rw-r--r-- | test-suite/bugs/closed/4095.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v index ffd33d38..8d7dfbd4 100644 --- a/test-suite/bugs/closed/4095.v +++ b/test-suite/bugs/closed/4095.v @@ -84,4 +84,4 @@ O1 : T -> PointedOPred tr : T -> T O2 : PointedOPred x0 : T -H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file +H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *) |