diff options
Diffstat (limited to 'test-suite/bugs/closed/4203.v')
| -rw-r--r-- | test-suite/bugs/closed/4203.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v index 076a3c3d..eb6867a0 100644 --- a/test-suite/bugs/closed/4203.v +++ b/test-suite/bugs/closed/4203.v @@ -16,4 +16,4 @@ Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok. Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok. Check (eq_refl t : t = t'). -Check (eq_refl t : t = t'').
\ No newline at end of file +Check (eq_refl t : t = t''). |