blob: 5d984463957cc872b87d47f8315821cd42f59f47 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
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).
|
