From b1b8243b7fc0bd8e2b9db3ddb28941646b3bd1ff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Oct 2014 15:17:07 +0200
Subject: When facing problem ?id = ?id' in resolution of return predicate,
 early call the standard resolution function which e.g. does restriction and
 maybe solve the problem if pattern-like, instead of postponing the problem.

---
 pretyping/cases.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 411f2c550f..78837b9d8c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1604,9 +1604,12 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let ev = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in
-        evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref;
-        ev
+        let ev' = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in
+        begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
+        | Success evd -> evdref := evd
+        | UnifFailure _ -> assert false
+        end;
+        ev'
     | _ ->
     let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in
     match good with
-- 
cgit v1.2.3