diff options
Diffstat (limited to 'test-suite/output/Cases.v')
| -rw-r--r-- | test-suite/output/Cases.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 37ee71e9..b6337586 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -12,7 +12,7 @@ Require Import Arith. Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y := match eq_nat_dec x y return P y with - | left eqprf => + | left eqprf => match eqprf in (_ = z) return (P z) with | refl_equal => def end |