diff options
| -rw-r--r-- | test-suite/modules/mod_decl.v | 2 | ||||
| -rw-r--r-- | test-suite/output/Tactics.out | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v index aad493cee..b886eb59d 100644 --- a/test-suite/modules/mod_decl.v +++ b/test-suite/modules/mod_decl.v @@ -34,7 +34,7 @@ Module Type T. Declare Module M1: SIG. - Declare Module M2 <: SIG. + Module M2 <: SIG. Definition A := nat. End M2. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 8e8b8059f..cf3a887b9 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -1,4 +1,4 @@ -intro H; split; [ a H | e H ]. +intro H; split; [ a H | e H ]. intros; match goal with | |- context [if ?X then _ else _] => case X end; trivial. |