3 files changed, 38 insertions, 1 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ad1409f5b..7f81d1aa3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -842,6 +842,15 @@ let rec find_solution_type evarenv = function
   | (id,ProjectEvar _)::l -> find_solution_type evarenv l
   | [] -> assert false
 
+let find_most_recent_projection evi sols =
+  let sign = List.map get_id (evar_filtered_context evi) in
+  match sols with
+  | y::l ->
+     List.fold_right (fun (id,p as x) (id',_ as y) ->
+         if List.index Id.equal id sign < List.index Id.equal id' sign then x else y)
+    l y
+  | _ -> assert false
+
 (* In case the solution to a projection problem requires the instantiation of
  * subsidiary evars, [do_projection_effects] performs them; it
  * also try to instantiate the type of those subsidiary evars if their
@@ -1429,7 +1438,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
       let c, p = match sols with
         | [] -> raise Not_found
         | [id,p] -> (mkVar id, p)
-        | (id,p)::_::_ ->
+        | _ ->
+            let (id,p) = find_most_recent_projection evi sols in
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
       let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3b3ad021e..aaa946706 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -96,6 +96,31 @@ let rec occur_meta_pattern = function
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
+let rec occurn_pattern n = function
+  | PRel p -> Int.equal n p
+  | PApp (f,args) ->
+      (occurn_pattern n f) || (Array.exists (occurn_pattern n) args)
+  | PProj (_,arg) -> occurn_pattern n arg
+  | PLambda (na,t,c)  -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+  | PProd (na,t,c)  -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+  | PLetIn (na,b,t,c)  ->
+     Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t ||
+     (occurn_pattern (n+1) c)
+  | PIf (c,c1,c2)  ->
+      (occurn_pattern n c) ||
+      (occurn_pattern n c1) || (occurn_pattern n c2)
+  | PCase(_,p,c,br) ->
+      (occurn_pattern n p) ||
+      (occurn_pattern n c) ||
+      (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
+  | PMeta _ | PSoApp _ -> true
+  | PEvar (_,args) -> Array.exists (occurn_pattern n) args
+  | PVar _ | PRef _ | PSort _ -> false
+  | PFix fix -> not (noccurn n (mkFix fix))
+  | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+
+let noccurn_pattern n c = not (occurn_pattern n c)
+
 exception BoundPattern;;
 
 let rec head_pattern_bound t =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index ffe0186af..2d1ce1dbc 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -22,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool
 
 val subst_pattern : substitution -> constr_pattern -> constr_pattern
 
+val noccurn_pattern : int -> constr_pattern -> bool
+
 exception BoundPattern
 
 (** [head_pattern_bound t] extracts the head variable/constant of the