diff options
| -rw-r--r-- | test-suite/output/Cases.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Cases.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index f846f4ee10..f44465456f 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -47,10 +47,10 @@ foo' = if A 0 then true else false f = fun H : B => match H with -| AC H0 => +| AC x => let b0 := b in (if b0 as b return (P b -> True) then fun _ : P true => Logic.I - else fun _ : P false => Logic.I) H0 + else fun _ : P false => Logic.I) x end : B -> True diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index a95b085ac0..a4d19d6930 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -72,7 +72,7 @@ Inductive B : Prop := AC : P b -> B. Definition f : B -> True. Proof. -intros []. +intros [x]. destruct b as [|] ; exact Logic.I. Defined. |