diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/interactive/Paral-ITP.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v index 09ec9de170..d8961c98d1 100644 --- a/test-suite/interactive/Paral-ITP.v +++ b/test-suite/interactive/Paral-ITP.v @@ -22,6 +22,7 @@ Qed. Lemma b : True. Proof. + do 11 (cut Type; [ intro foo; clear foo | exact Type]). sleep time. idtac. (* change in semantics: Print a. *) |