Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 24 insertions, 1 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 01109d8af9..690a673c6e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -239,7 +239,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       match (kind_of_term cM,kind_of_term cN) with
 	| Meta k1, Meta k2 ->
 	    let stM,stN = extract_instance_status pb in
-	    if k1 < k2
+	    if k2 < k1
 	    then sigma,(k1,cN,stN)::metasubst,evarsubst
 	    else if k1 = k2 then substn
 	    else sigma,(k2,cM,stM)::metasubst,evarsubst
diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out
new file mode 100644
index 0000000000..30385072c2
--- /dev/null
+++ b/test-suite/output/rewrite-2172.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+=> Error: Unable to find an instance for the variable E.
diff --git a/test-suite/output/rewrite-2172.v b/test-suite/output/rewrite-2172.v
new file mode 100644
index 0000000000..212b1c1259
--- /dev/null
+++ b/test-suite/output/rewrite-2172.v
@@ -0,0 +1,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.