diff options
Diffstat (limited to 'test-suite/interactive')
| -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 09ec9de17..d8961c98d 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. *) |