Make evarconv and unification able to handle eta for records in presence

of metas/evars

1 files changed, 9 insertions, 16 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 14bc45e0ce..6d77658087 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -418,23 +418,16 @@ let is_unification_pattern_meta env nb m l t =
   else
     None
 
-let is_unification_pattern_evar_occur env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l
+let is_unification_pattern_evar env evd (evk,args) l t =
+  if List.for_all (fun x -> isRel x || isVar x) l 
+    && noccur_evar env evd evk t
   then
-    if not (noccur_evar env evd evk t) then raise Occur
-    else
-      let args = remove_instance_local_defs evd evk args in
-      let n = List.length args in
-	match find_unification_pattern_args env (args @ l) t with
-	| Some l -> Some (List.skipn n l)
-	| _ -> None
-  else
-    if noccur_evar env evd evk t then None
-    else raise Occur
-
-let is_unification_pattern_evar env evd ev l t =
-  try is_unification_pattern_evar_occur env evd ev l t
-  with Occur -> None
+    let args = remove_instance_local_defs evd evk args in
+    let n = List.length args in
+      match find_unification_pattern_args env (args @ l) t with
+      | Some l -> Some (List.skipn n l)
+      | _ -> None
+  else None
 
 let is_unification_pattern_pure_evar env evd (evk,args) t =
   let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in