diff options
| -rw-r--r-- | test-suite/output/Cases.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Tactics.out | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 63137edbac..a3033e94fc 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -2,7 +2,7 @@ t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with - | k x x0 => f x0 (F x0) + | k _ x0 => f x0 (F x0) end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index cf3a887b9f..8e8b8059f9 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. |