Fix for stronger Coq unification between fixpoints.

[SkySkimmer]

We have a definition

Variable A (ea:A -> A -> Prop).
  Fixpoint In_gen(a : A)(ls : list A) : Prop :=
    match ls with
      | nil => False
      | a' :: ls' =>
        ea a a' \/ In_gen a ls'
    end.

with a proof In_gen_eq that In_gen eq is equivalent to In (the standard Coq In). Note that In has the equality the other way around, ie In is convertible to In_gen (fun x y => y = x).

Then at some point we have a goal In_gen ?e a l and apply In_gen_eq. Before the Coq update we cannot unify with the In side of the equivalence and so we get a new goal In a l with ?e := eq. After the Coq update we can unify with In a l using ?e := fun x y => y = x and get a new goal In_gen eq a l. This doesn't match an hypothesis H6 : In a l so the next tactic trivial does nothing and the script goes off-road.

[SkySkimmer]

The patch should be backward compatible but let's see what travis says.

[SkySkimmer]

Travis says it's OK.