aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/rewrite-2172.v
blob: 212b1c125970be9594eeb2d6a44e37315f541852 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(* This checks an error message as reported in bug #2172 *)

Axiom axiom : forall (E F : nat), E = F.
Lemma test : forall (E F : nat), E = F.
Proof.
  intros.
(* This used to raise the following non understandable error message:

   Error: Unable to find an instance for the variable x

   The reason this error was that rewrite generated the proof

   "eq_ind ?A ?x ?P ? ?y (axiom ?E ?F)"

   and the equation ?x=?E was solved in the way ?E:=?x leaving ?x
   unresolved. A stupid hack for solve this consisted in ordering
   meta=meta equations the other way round (with most recent evars
   instantiated first - since they are assumed to come first from the
   user in rewrite/induction/destruct calls).
*)
  Fail rewrite <- axiom.