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.

1 files changed, 15 insertions, 8 deletions

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