Two fixes in unification (bugs #3782 and #3709)

- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.

3 files changed, 37 insertions, 33 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b1f2019956..80cb631653 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -112,7 +112,7 @@ let occur_rigidly ev evd t =
     | Case _ -> false
   in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app
 
-(* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
+(* [check_conv_record env sigma (t1,l1) (t2,l2)] tries to decompose the problem
    (t1 l1) = (t2 l2) into a problem
 
      l1 = params1@c1::extra_args1
@@ -132,7 +132,7 @@ let occur_rigidly ev evd t =
    object c in structure R (since, if c1 were not an evar, the
    projection would have been reduced) *)
 
-let check_conv_record (t1,sk1) (t2,sk2) =
+let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let (proji, u), arg = Universes.global_app_of_constr t1 in
   let canon_s,sk2_effective =
     try
@@ -156,7 +156,11 @@ let check_conv_record (t1,sk1) (t2,sk2) =
   let params1, c1, extra_args1 =
     match arg with
     | Some c -> (* A primitive projection applied to c *)
-      [], c, sk1
+      let ty = Retyping.get_type_of ~lax:true env sigma c in
+      let (i,u), ind_args = 
+	try Inductiveops.find_mrectype env sigma ty 
+	with _ -> raise Not_found
+      in Stack.append_app_list ind_args Stack.empty, c, sk1
     | None ->
       match Stack.strip_n_app nparams sk1 with
       | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
@@ -612,8 +616,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  (try 
 	     if not (snd ts) then raise Not_found
 	     else conv_record ts env i
-               (try check_conv_record appr1 appr2
-		with Not_found -> check_conv_record appr2 appr1)
+               (try check_conv_record env i appr1 appr2
+		with Not_found -> check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f3 i =
           (* heuristic: unfold second argument first, exception made
@@ -672,7 +676,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	let f3 i =
 	  (try 
 	     if not (snd ts) then raise Not_found
-	     else conv_record ts env i (check_conv_record appr1 appr2)
+	     else conv_record ts env i (check_conv_record env i appr1 appr2)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
 	  evar_eqappr_x ts env i pbty
@@ -686,7 +690,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	let f3 i =
 	  (try
 	     if not (snd ts) then raise Not_found
-	     else conv_record ts env i (check_conv_record appr2 appr1)
+	     else conv_record ts env i (check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
 	  evar_eqappr_x ts env i pbty (appr1,csts1)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index f3363e3587..f559db2537 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -42,7 +42,8 @@ val check_problems_are_solved : env -> evar_map -> unit
 
 (** Check if a canonical structure is applicable *)
 
-val check_conv_record : constr * types Stack.t -> constr * types Stack.t ->
+val check_conv_record : env -> evar_map -> 
+  constr * types Stack.t -> constr * types Stack.t ->
   Univ.universe_context_set * (constr * constr) 
   * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * types Stack.t) *
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a53240a1cf..3c89bf27a2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -732,8 +732,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
 	   with ex when precatchable_exception ex ->
 	     match kind_of_term cN with
-	     | App(f2,l2) when isMeta f2 || isEvar f2 ->
-	       unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	     | App(f2,l2) when
+		 (isMeta f2 && use_metas_pattern_unification flags nb l2
+		  || use_evars_pattern_unification flags && isAllowedEvar flags f2) ->
+	       unify_app_pattern false curenvnb pb opt substn cM f1 l1 cN f2 l2
 	     | _ -> raise ex)
 
 	| _, App (f2, l2) when flags.modulo_eta && 
@@ -744,8 +746,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
 	   with ex when precatchable_exception ex ->
 	     match kind_of_term cM with
-	     | App(f1,l1) when isMeta f1 || isEvar f1 ->
-	       unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	     | App(f1,l1) when 
+		 (isMeta f1 && use_metas_pattern_unification flags nb l1
+		  || use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
+	       unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2
 	     | _ -> raise ex)
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
@@ -761,30 +765,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| App (f1,l1), _ when 
 	    (isMeta f1 && use_metas_pattern_unification flags nb l1
             || use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
-            (match
-                is_unification_pattern curenvnb sigma f1 (Array.to_list l1) cN
-             with
-             | None ->
-                 (match kind_of_term cN with
-                 | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
-                 | Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN cN [||]
-                 | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
-             | Some l ->
-                 solve_pattern_eqn_array curenvnb f1 l cN substn)
+	  unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN cN [||]
 
 	| _, App (f2,l2) when
 	    (isMeta f2 && use_metas_pattern_unification flags nb l2
             || use_evars_pattern_unification flags && isAllowedEvar flags f2) ->
-            (match
-                is_unification_pattern curenvnb sigma f2 (Array.to_list l2) cM
-             with
-             | None ->
-                 (match kind_of_term cM with
-                 | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
-                 | Proj _ -> unify_app curenvnb pb opt substn cM cM [||] cN f2 l2
-                 | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
-             | Some l ->
-	         solve_pattern_eqn_array curenvnb f2 l cM substn)
+	  unify_app_pattern false curenvnb pb opt substn cM cM [||] cN f2 l2
 
 	| App (f1,l1), App (f2,l2) ->
 	  unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
@@ -798,6 +784,19 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| _ ->
           unify_not_same_head curenvnb pb opt substn cM cN
 
+  and unify_app_pattern dir curenvnb pb opt substn cM f1 l1 cN f2 l2 =
+    let f, l, t = if dir then f1, l1, cN else f2, l2, cM in
+      match is_unification_pattern curenvnb sigma f (Array.to_list l) t with
+      | None ->
+	(match kind_of_term t with
+	| App (f',l') -> 
+	  if dir then unify_app curenvnb pb opt substn cM f1 l1 t f' l'
+	  else unify_app curenvnb pb opt substn t f' l' cN f2 l2
+	| Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	| _ -> unify_not_same_head curenvnb pb opt substn cM cN)
+      | Some l ->
+	solve_pattern_eqn_array curenvnb f l t substn
+
   and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
     try
       let needs_expansion p c' = 
@@ -963,7 +962,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 
   and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
     let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
-      try Evarconv.check_conv_record f1l1 f2l2
+      try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
     if Reductionops.Stack.compare_shape ts ts1 then