diff options
| author | Emilio Jesus Gallego Arias | 2018-05-17 18:28:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-17 18:28:42 +0200 |
| commit | 5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (patch) | |
| tree | 49b5ee04830560ff74a3a27c7add6000e28c0980 /test-suite/ide | |
| parent | b0cf6c4042ed8e91c6f7081a6f0c4b83ec9407c2 (diff) | |
| parent | c9b4073104385f6079f260c5183bb3a6a989b7d9 (diff) | |
Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by default.
Diffstat (limited to 'test-suite/ide')
| -rw-r--r-- | test-suite/ide/undo012.fake | 1 | ||||
| -rw-r--r-- | test-suite/ide/undo013.fake | 1 | ||||
| -rw-r--r-- | test-suite/ide/undo014.fake | 1 | ||||
| -rw-r--r-- | test-suite/ide/undo015.fake | 1 | ||||
| -rw-r--r-- | test-suite/ide/undo016.fake | 1 |
5 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake index b3d1c6d534..c95df1b11c 100644 --- a/test-suite/ide/undo012.fake +++ b/test-suite/ide/undo012.fake @@ -3,6 +3,7 @@ # # Test backtracking in presence of nested proofs # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake index 921a9d0f0d..a3ccefd2ca 100644 --- a/test-suite/ide/undo013.fake +++ b/test-suite/ide/undo013.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Second, trigger the undo of an inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake index f5fe774704..13e718229c 100644 --- a/test-suite/ide/undo014.fake +++ b/test-suite/ide/undo014.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Third, undo inside an inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake index a1e5c947b3..9cbd64460d 100644 --- a/test-suite/ide/undo015.fake +++ b/test-suite/ide/undo015.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Fourth, undo from an inner proof to a above proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake index f9414c1ea7..15bd3cc92d 100644 --- a/test-suite/ide/undo016.fake +++ b/test-suite/ide/undo016.fake @@ -4,6 +4,7 @@ # Test backtracking in presence of nested proofs # Fifth, undo from an inner proof to a previous inner proof # +ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } |