From 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 25 Aug 2014 21:46:26 +0200
Subject: Fixing bug #3377 by giving env and sigma to constrMathching. Now it's
 possible to match on a primitive projection application c.(p) using "?f _",
 binding f to (fun x => x.(p)) with the correct typing.

---
 pretyping/evarsolve.ml | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 08b704bdea..14bc45e0ce 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -418,16 +418,23 @@ let is_unification_pattern_meta env nb m l t =
   else
     None
 
-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
+let is_unification_pattern_evar_occur env evd (evk,args) l t =
+  if List.for_all (fun x -> isRel x || isVar x) l
   then
-    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
+    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
-    None
+    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 is_unification_pattern_pure_evar env evd (evk,args) t =
   let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
-- 
cgit v1.2.3