blob: 9982b96f7923429f1d03c5cde7e4987dad11ee19 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require Import JMeq.
Axiom test : forall n m : nat, JMeq n m.
Goal forall n m : nat, JMeq n m.
(* I) with no intros nor variable hints, this should produce a regular error
instead of Uncaught exception Failure("nth"). *)
Fail rewrite test.
(* II) with intros but indication of variables, still an error *)
Fail (intros; rewrite test).
(* III) a working variant: *)
intros; rewrite (test n m).
Abort.
|
