Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 414 insertions, 200 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d080016..04f86e70 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 open Names
@@ -24,44 +22,52 @@ open Evd
 
 type flex_kind_of_term =
   | Rigid of constr
-  | MaybeFlexible of constr
+  | PseudoRigid of constr (* approximated as rigid but not necessarily so *)
+  | MaybeFlexible of constr (* approx'ed as reducible but not necessarily so *)
   | Flexible of existential
 
 let flex_kind_of_term c l =
   match kind_of_term c with
-    | Const _ -> MaybeFlexible c
-    | Rel n -> MaybeFlexible c
-    | Var id -> MaybeFlexible c
+    | Rel _ | Const _ | Var _ -> MaybeFlexible c
     | Lambda _ when l<>[] -> MaybeFlexible c
     | LetIn _  -> MaybeFlexible c
     | Evar ev -> Flexible ev
-    | _ -> Rigid c
+    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid c
+    | Meta _ | Case _ | Fix _ -> PseudoRigid c
+    | Cast _ | App _ -> assert false
 
-let eval_flexible_term env c =
+let eval_flexible_term ts env c =
   match kind_of_term c with
-  | Const c -> constant_opt_value env c
+  | Const c -> 
+      if is_transparent_constant ts c
+      then constant_opt_value env c
+      else None
   | Rel n ->
       (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v
       with Not_found -> None)
   | Var id ->
-      (try let (_,v,_) = lookup_named id env in v with Not_found -> None)
+      (try
+	 if is_transparent_variable ts id then
+	   let (_,v,_) = lookup_named id env in v 
+	 else None 
+       with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c)
   | Lambda _ -> Some c
   | _ -> assert false
 
-let evar_apprec env evd stack c =
+let evar_apprec ts env evd stack c =
   let sigma =  evd in
   let rec aux s =
-    let (t,stack) = whd_betaiota_deltazeta_for_iota_state env sigma s in
+    let (t,stack) = whd_betaiota_deltazeta_for_iota_state ts env sigma s in
     match kind_of_term t with
       | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
 	  aux (Evd.existential_value sigma ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack_list stack empty_stack)
 
-let apprec_nohdbeta env evd c =
+let apprec_nohdbeta ts env evd c =
   match kind_of_term (fst (Reductionops.whd_stack evd c)) with
-    | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
+    | (Case _ | Fix _) -> applist (evar_apprec ts env evd [] c)
     | _ -> c
 
 let position_problem l2r = function
@@ -159,16 +165,15 @@ let ise_array2 evd f v1 v2 =
   if lv1 = Array.length v2 then allrec evd (pred lv1)
   else (evd,false)
 
-let rec evar_conv_x env evd pbty term1 term2 =
-  let sigma =  evd in
-  let term1 = whd_head_evar sigma term1 in
-  let term2 = whd_head_evar sigma term2 in
+let rec evar_conv_x ts env evd pbty term1 term2 =
+  let term1 = whd_head_evar evd term1 in
+  let term2 = whd_head_evar evd term2 in
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then
-      if is_fconv pbty env evd term1 term2 then
+      if is_trans_fconv pbty ts env evd term1 term2 then
         Some true
       else if is_ground_env evd env then Some false
       else None
@@ -176,19 +181,22 @@ let rec evar_conv_x env evd pbty term1 term2 =
   match ground_test with
       Some b -> (evd,b)
     | None ->
-        let term1 = apprec_nohdbeta env evd term1 in
-        let term2 = apprec_nohdbeta env evd term2 in
+	(* Until pattern-unification is used consistently, use nohdbeta to not
+	   destroy beta-redexes that can be used for 1st-order unification *)
+        let term1 = apprec_nohdbeta ts env evd term1 in
+        let term2 = apprec_nohdbeta ts env evd term2 in
         if is_undefined_evar evd term1 then
-          solve_simple_eqn evar_conv_x env evd
+          solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,destEvar term1,term2)
         else if is_undefined_evar evd term2 then
-          solve_simple_eqn evar_conv_x env evd
+          solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem false pbty,destEvar term2,term1)
         else
-          evar_eqappr_x env evd pbty
+          evar_eqappr_x ts env evd pbty
             (decompose_app term1) (decompose_app term2)
 
-and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
+and evar_eqappr_x ?(rhs_is_stuck_proj = false)
+  ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have flushed evars *)
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -196,23 +204,23 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  if List.length l1 > List.length l2 then
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
-              [(fun i -> solve_simple_eqn evar_conv_x env i
+              [(fun i -> solve_simple_eqn (evar_conv_x ts) env i
 	        (position_problem false pbty,ev2,applist(term1,deb1)));
               (fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) rest1 l2)]
+                  (fun i -> evar_conv_x ts env i CONV) rest1 l2)]
 	  else
 	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
             ise_and i
-              [(fun i -> solve_simple_eqn evar_conv_x env i
+              [(fun i -> solve_simple_eqn (evar_conv_x ts) env i
 	          (position_problem true pbty,ev1,applist(term2,deb2)));
               (fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) l1 rest2)]
+                  (fun i -> evar_conv_x ts env i CONV) l1 rest2)]
 	and f2 i =
           if sp1 = sp2 then
             ise_and i
             [(fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) l1 l2);
-             (fun i -> solve_refl evar_conv_x env i sp1 al1 al2,
+                  (fun i -> evar_conv_x ts env i CONV) l1 l2);
+             (fun i -> solve_refl (evar_conv_x ts) env i sp1 al1 al2,
                   true)]
           else (i,false)
 	in
@@ -220,17 +228,17 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
-	  if
-	    is_unification_pattern_evar env ev1 l1 (applist appr2) &
-	    not (occur_evar (fst ev1) (applist appr2))
-	  then
+          match is_unification_pattern_evar env evd ev1 l1 (applist appr2) with
+          | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t2 = nf_evar evd (applist appr2) in
-	    let t2 = solve_pattern_eqn env l1 t2 in
-	    solve_simple_eqn evar_conv_x env evd
+	    let t2 = solve_pattern_eqn env l1' t2 in
+	    solve_simple_eqn (evar_conv_x ts) env evd
 	      (position_problem true pbty,ev1,t2)
-	  else if
+          | None -> (i,false)
+        and f2 i =
+	  if
             List.length l1 <= List.length l2
 	  then
 	    (* Try first-order unification *)
@@ -240,30 +248,30 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and i
               (* First compare extra args for better failure message *)
               [(fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) l1 rest2);
-               (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))]
+                  (fun i -> evar_conv_x ts env i CONV) l1 rest2);
+               (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
           else (i,false)
-	and f4 i =
-	  match eval_flexible_term env flex2 with
+	and f3 i =
+	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
-		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f4]
+	ise_try evd [f1; f2; f3]
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
-	  if
-	    is_unification_pattern_evar env ev2 l2 (applist appr1) &
-	    not (occur_evar (fst ev2) (applist appr1))
-	  then
+	  match is_unification_pattern_evar env evd ev2 l2 (applist appr1) with
+          | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t1 = nf_evar evd (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
-	    solve_simple_eqn evar_conv_x env evd
+	    solve_simple_eqn (evar_conv_x ts) env evd
 	      (position_problem false pbty,ev2,t1)
-	  else if
+          | None -> (i,false)
+        and f2 i =
+          if
        	    List.length l2 <= List.length l1
 	  then
 	    (* Try first-order unification *)
@@ -272,25 +280,43 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and i
             (* First compare extra args for better failure message *)
               [(fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) rest1 l2);
-               (fun i -> evar_conv_x env i pbty (applist(term1,deb1)) term2)]
+                  (fun i -> evar_conv_x ts env i CONV) rest1 l2);
+               (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
           else (i,false)
-	and f4 i =
-	  match eval_flexible_term env flex1 with
+	and f3 i =
+	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f4]
+	ise_try evd [f1; f2; f3]
+
+    | MaybeFlexible flex1, MaybeFlexible flex2 -> begin
+        match kind_of_term flex1, kind_of_term flex2 with
+        | LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
+        let f1 i =
+          ise_and i
+	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
+	     (fun i ->
+	       let b = nf_evar i b1 in
+	       let t = nf_evar i t1 in
+	       evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
+	     (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)]
+	and f2 i =
+          let appr1 = evar_apprec ts env i l1 (subst1 b1 c'1)
+          and appr2 = evar_apprec ts env i l2 (subst1 b2 c'2)
+	  in evar_eqappr_x ts env i pbty appr1 appr2
+	in
+	ise_try evd [f1; f2]
 
-    | MaybeFlexible flex1, MaybeFlexible flex2 ->
+	| _, _ ->
 	let f1 i =
-	  if flex1 = flex2 then
-	    ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
+	  if eq_constr flex1 flex2 then
+	    ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2
 	  else
 	     (i,false)
 	and f2 i =
-	  (try conv_record env i
+	  (try conv_record ts env i
              (try check_conv_record appr1 appr2
 	      with Not_found -> check_conv_record appr2 appr1)
            with Not_found -> (i,false))
@@ -299,186 +325,204 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
              if the first argument is a beta-redex (expand a constant
              only if necessary) or the second argument is potentially
              usable as a canonical projection *)
-	  if isLambda flex1 or is_open_canonical_projection i appr2
-	  then
-	    match eval_flexible_term env flex1 with
+          let rhs_is_stuck_proj =
+            rhs_is_stuck_proj || is_open_canonical_projection env i appr2 in
+	  if isLambda flex1 || rhs_is_stuck_proj then
+	    match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ~rhs_is_stuck_proj 
+                  ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None ->
-		match eval_flexible_term env flex2 with
+		match eval_flexible_term ts env flex2 with
 		| Some v2 ->
-		    evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		    evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 		| None -> (i,false)
 	  else
-	    match eval_flexible_term env flex2 with
+	    match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
-		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 	    | None ->
-		match eval_flexible_term env flex1 with
+		match eval_flexible_term ts env flex1 with
 		| Some v1 ->
-		    evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		    evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 		| None -> (i,false)
 	in
 	ise_try evd [f1; f2; f3]
-
-    | Flexible ev1, Rigid _ ->
-	if
-	  is_unification_pattern_evar env ev1 l1 (applist appr2) &
-	  not (occur_evar (fst ev1) (applist appr2))
-	then
-	  (* Miller-Pfenning's patterns unification *)
-	  (* Preserve generality (except that CCI has no eta-conversion) *)
+      end
+
+    | Rigid c1, Rigid c2 when isLambda c1 & isLambda c2 ->
+        let (na,c1,c'1) = destLambda c1 in
+        let (_,c2,c'2) = destLambda c2 in
+        assert (l1=[] & l2=[]);
+        ise_and evd
+          [(fun i -> evar_conv_x ts env i CONV c1 c2);
+           (fun i ->
+	     let c = nf_evar i c1 in
+	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
+
+    | Flexible ev1, (Rigid _ | PseudoRigid _) ->
+	(match is_unification_pattern_evar env evd ev1 l1 (applist appr2) with
+        | Some l1 ->
+	  (* Miller-Pfenning's pattern unification *)
+	  (* Preserve generality thanks to eta-conversion) *)
 	  let t2 = nf_evar evd (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
-	  solve_simple_eqn evar_conv_x env evd
+	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,ev1,t2)
-	else
+        | None ->
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
-	  true
-
-    | Rigid _, Flexible ev2 ->
-	if
-	  is_unification_pattern_evar env ev2 l2 (applist appr1) &
-	  not (occur_evar (fst ev2) (applist appr1))
-	then
-	  (* Miller-Pfenning's patterns unification *)
-	  (* Preserve generality (except that CCI has no eta-conversion) *)
+	  true)
+
+    | (Rigid _ | PseudoRigid _), Flexible ev2 ->
+	(match is_unification_pattern_evar env evd ev2 l2 (applist appr1) with
+        | Some l2 ->
+	  (* Miller-Pfenning's pattern unification *)
+	  (* Preserve generality thanks to eta-conversion) *)
 	  let t1 = nf_evar evd (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
-	  solve_simple_eqn evar_conv_x env evd
+	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem false pbty,ev2,t1)
-	else
+        | None ->
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
-	  true
+	  true)
 
-    | MaybeFlexible flex1, Rigid _ ->
+    | MaybeFlexible flex1, (Rigid _ | PseudoRigid _) ->
 	let f3 i =
-	  (try conv_record env i (check_conv_record appr1 appr2)
+	  (try conv_record ts env i (check_conv_record appr1 appr2)
            with Not_found -> (i,false))
 	and f4 i =
-	  match eval_flexible_term env flex1 with
+	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
- 		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
 
-    | Rigid _ , MaybeFlexible flex2 ->
+    | (Rigid _ | PseudoRigid _), MaybeFlexible flex2 ->
 	let f3 i =
-	  (try conv_record env i (check_conv_record appr2 appr1)
+	  (try conv_record ts env i (check_conv_record appr2 appr1)
            with Not_found -> (i,false))
 	and f4 i =
-	  match eval_flexible_term env flex2 with
+	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
- 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
 
-    | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
-
-	| Cast (c1,_,_), _ -> evar_eqappr_x env evd pbty (c1,l1) appr2
-
-	| _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
+    (* Eta-expansion *)
+    | Rigid c1, _ when isLambda c1 ->
+	assert (l1 = []);
+	let (na,c1,c'1) = destLambda c1 in
+        let c = nf_evar evd c1 in
+	let env' = push_rel (na,None,c) env in
+        let appr1 = evar_apprec ts env' evd [] c'1 in
+	let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
+	evar_eqappr_x ts env' evd CONV appr1 appr2
+
+    | _, Rigid c2 when isLambda c2 ->
+	assert (l2 = []);
+	let (na,c2,c'2) = destLambda c2 in
+        let c = nf_evar evd c2 in
+	let env' = push_rel (na,None,c) env in
+	let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
+        let appr2 = evar_apprec ts env' evd [] c'2 in
+	evar_eqappr_x ts env' evd CONV appr1 appr2
+
+    | Rigid c1, Rigid c2 -> begin
+        match kind_of_term c1, kind_of_term c2 with
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-            (evd,base_sort_cmp pbty s1 s2)
-
-	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] ->
-            ise_and evd
-              [(fun i -> evar_conv_x env i CONV c1 c2);
-               (fun i ->
-                 let c = nf_evar i c1 in
-                 evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
-
-	| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
-	    let f1 i =
-              ise_and i
-                [(fun i -> evar_conv_x env i CONV b1 b2);
-                 (fun i ->
-                   let b = nf_evar i b1 in
-	           let t = nf_evar i t1 in
-                   evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
-                 (fun i -> ise_list2 i
-                     (fun i -> evar_conv_x env i CONV) l1 l2)]
-	    and f2 i =
-              let appr1 = evar_apprec env i l1 (subst1 b1 c'1)
-              and appr2 = evar_apprec env i l2 (subst1 b2 c'2)
-	      in evar_eqappr_x env i pbty appr1 appr2
-	    in
-	    ise_try evd [f1; f2]
-
-	| LetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
-	     let appr1 = evar_apprec env evd l1 (subst1 b1 c'1)
-             in evar_eqappr_x env evd pbty appr1 appr2
-
-	| _, LetIn (_,b2,_,c'2) ->
-	    let appr2 = evar_apprec env evd l2 (subst1 b2 c'2)
-            in evar_eqappr_x env evd pbty appr1 appr2
+	    (try 
+	       let evd' = 
+		 if pbty = CONV 
+		 then Evd.set_eq_sort evd s1 s2 
+		 else Evd.set_leq_sort evd s1 s2 
+	       in (evd', true)
+	     with Univ.UniverseInconsistency _ -> (evd, false)
+	     | _ -> (evd, false))
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
             ise_and evd
-              [(fun i -> evar_conv_x env i CONV c1 c2);
+              [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
-	         evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
+	         evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
 
 	| Ind sp1, Ind sp2 ->
 	    if eq_ind sp1 sp2 then
-              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+              ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
             else (evd, false)
 
 	| Construct sp1, Construct sp2 ->
 	    if eq_constructor sp1 sp2 then
-              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+              ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
             else (evd, false)
 
+	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
+            if i1=i2  then
+              ise_and evd
+                [(fun i -> ise_array2 i
+                    (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
+                 (fun i -> ise_array2 i
+		     (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
+		     bds1 bds2);
+                 (fun i -> ise_list2 i
+                     (fun i -> evar_conv_x ts env i CONV) l1 l2)]
+            else (evd,false)
+
+	| (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ -> (evd,false)
+	| _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) -> (evd,false)
+
+	| (App _ | Meta _ | Cast _ | Case _ | Fix _), _ -> assert false
+	| (LetIn _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false
+	| (Lambda _), _ -> assert false
+
+      end
+
+    | PseudoRigid c1, PseudoRigid c2 -> begin
+        match kind_of_term c1, kind_of_term c2 with
+
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             ise_and evd
-              [(fun i -> evar_conv_x env i CONV p1 p2);
-               (fun i -> evar_conv_x env i CONV c1 c2);
+              [(fun i -> evar_conv_x ts env i CONV p1 p2);
+               (fun i -> evar_conv_x ts env i CONV c1 c2);
 	       (fun i -> ise_array2 i
-                   (fun i -> evar_conv_x env i CONV) cl1 cl2);
-               (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)]
+                   (fun i -> evar_conv_x ts env i CONV) cl1 cl2);
+               (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)]
 
 	| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
             if li1=li2 then
               ise_and evd
                 [(fun i -> ise_array2 i
-                    (fun i -> evar_conv_x env i CONV) tys1 tys2);
+                    (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
-		     (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+		     (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
 		     bds1 bds2);
 	         (fun i -> ise_list2 i
-                     (fun i -> evar_conv_x env i CONV) l1 l2)]
+                     (fun i -> evar_conv_x ts env i CONV) l1 l2)]
 	    else (evd,false)
-	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
-            if i1=i2  then
-              ise_and evd
-                [(fun i -> ise_array2 i
-                    (fun i -> evar_conv_x env i CONV) tys1 tys2);
-                 (fun i -> ise_array2 i
-		     (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
-		     bds1 bds2);
-                 (fun i -> ise_list2 i
-                     (fun i -> evar_conv_x env i CONV) l1 l2)]
-            else (evd,false)
 
-	| (Meta _ | Lambda _), _ -> (evd,false)
-	| _, (Meta _ | Lambda _) -> (evd,false)
+	| (Meta _ | Case _ | Fix _ | CoFix _),
+	  (Meta _ | Case _ | Fix _ | CoFix _) -> (evd,false)
+
+	| (App _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> assert false
+	| _, (App _ | Ind _ | Construct _ | Sort _ | Prod _) -> assert false
 
-	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
-	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
+	| (LetIn _ | Cast _), _ -> assert false
+	| _, (LetIn _ | Cast _) -> assert false
 
-	| (App _ | Case _ | Fix _ | CoFix _),
-	  (App _ | Case _ | Fix _ | CoFix _) -> (evd,false)
+	| (Lambda _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false
+	| _, (Lambda _ | Rel _ | Var _ | Const _ | Evar _) -> assert false
+      end
 
-	| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
-	| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
+    | PseudoRigid _, Rigid _ ->  (evd,false)
 
-and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+    | Rigid _, PseudoRigid _ ->  (evd,false)
+
+and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   let (evd',ks,_) =
     List.fold_left
       (fun (i,ks,m) b ->
@@ -491,89 +535,259 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   ise_and evd'
     [(fun i ->
        ise_list2 i
-         (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x))
+         (fun i x1 x -> evar_conv_x trs env i CONV x1 (substl ks x))
          params1 params);
     (fun i ->
       ise_list2 i
-        (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
+        (fun i u1 u -> evar_conv_x trs env i CONV u1 (substl ks u))
         us2 us);
-    (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))));
-    (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1)]
+    (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))));
+    (fun i -> ise_list2 i (fun i -> evar_conv_x trs env i CONV) ts ts1)]
+
+(* getting rid of the optional argument rhs_is_stuck_proj *)
+let evar_eqappr_x ts env evd pbty appr1 appr2 =
+  evar_eqappr_x ts env evd pbty appr1 appr2
 
 (* We assume here |l1| <= |l2| *)
 
-let first_order_unification env evd (ev1,l1) (term2,l2) =
+let first_order_unification ts env evd (ev1,l1) (term2,l2) =
   let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
   ise_and evd
     (* First compare extra args for better failure message *)
-    [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
+    [(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
     (fun i ->
       (* Then instantiate evar unless already done by unifying args *)
       let t2 = applist(term2,deb2) in
       if is_defined_evar i ev1 then
-	evar_conv_x env i CONV t2 (mkEvar ev1)
+	evar_conv_x ts env i CONV t2 (mkEvar ev1)
       else
-	solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))]
+	solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
-  let evi = Evd.find evd evk in
+  let evi = Evd.find_undefined evd evk in
   let subst = make_pure_subst evi args in
-  let subst' = List.filter (fun (id,c) -> c = term) subst in
+  let subst' = List.filter (fun (id,c) -> eq_constr c term) subst in
   if subst' = [] then error "Too complex unification problem." else
   Evd.define evk (mkVar (fst (List.hd subst'))) evd
 
-let apply_conversion_problem_heuristic env evd pbty t1 t2 =
-  let t1 = apprec_nohdbeta env evd (whd_head_evar evd t1) in
-  let t2 = apprec_nohdbeta env evd (whd_head_evar evd t2) in
+let apply_on_subterm f c t =
+  let rec applyrec (k,c as kc) t =
+    (* By using eq_constr, we make an approximation, for instance, we *)
+    (* could also be interested in finding a term u convertible to t *)
+    (* such that c occurs in u *)
+    if eq_constr c t then f k
+    else
+      map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
+	applyrec kc t
+  in
+  applyrec (0,c) t
+
+let filter_possible_projections c args =
+  let fv1 = free_rels c in
+  let fv2 = collect_vars c in
+  List.map (fun a ->
+    a == c ||
+    (* Here we make an approximation, for instance, we could also be *)
+    (* interested in finding a term u convertible to c such that a occurs *)
+    (* in u *)
+    isRel a && Intset.mem (destRel a) fv1 ||
+    isVar a && Idset.mem (destVar a) fv2)
+    args
+
+let initial_evar_data evi =
+  let ids = List.map pi1 (evar_context evi) in
+  (evar_filter evi, List.map mkVar ids)
+
+let solve_evars = ref (fun _ -> failwith "solve_evars not installed")
+let set_solve_evars f = solve_evars := f
+
+(* We solve the problem env_rhs |- ?e[u1..un] = rhs knowing
+ * x1:T1 .. xn:Tn |- ev : ty
+ * by looking for a maximal well-typed abtraction over u1..un in rhs
+ *
+ * We first build C[e11..e1p1,..,en1..enpn] obtained from rhs by replacing
+ * all occurrences of u1..un by evars eij of type Ti' where itself Ti' has
+ * been obtained from the type of ui by also replacing all occurrences of
+ * u1..ui-1 by evars.
+ *
+ * Then, we use typing to infer the relations between the different
+ * occurrences. If some occurrence is still unconstrained after typing,
+ * we instantiate successively the unresolved occurrences of un by xn,
+ * of un-1 by xn-1, etc [the idea comes from Chung-Kil Hur, that he
+ * used for his Heq plugin; extensions to several arguments based on a
+ * proposition from Dan Grayson]
+ *)
+
+let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
+  try
+  let args = Array.to_list args in
+  let evi = Evd.find_undefined evd evk in
+  let env_evar = evar_env evi in
+  let sign = named_context_val env_evar in
+  let ctxt = evar_filtered_context evi in
+  let filter = evar_filter evi in
+  let instance = List.map mkVar (List.map pi1 ctxt) in
+
+  let rec make_subst = function
+  | (id,_,t)::ctxt, c::l, occs::occsl when isVarId id c ->
+      if occs<>None then
+        error "Cannot force abstraction on identity instance."
+      else
+        make_subst (ctxt,l,occsl)
+  | (id,_,t)::ctxt, c::l, occs::occsl ->
+      let evs = ref [] in
+      let filter = List.map2 (&&) filter (filter_possible_projections c args) in
+      let ty = Retyping.get_type_of env_rhs evd c in
+      (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt,l,occsl)
+  | [], [], [] -> []
+  | _ -> anomaly "Signature, instance and occurrences list do not match" in
+
+  let rec set_holes evdref rhs = function
+  | (id,_,c,cty,evsref,filter,occs)::subst ->
+      let set_var k =
+        match occs with
+        | Some (false,[]) -> mkVar id
+        | Some _ -> error "Selection of specific occurrences not supported"
+        | None ->
+        let evty = set_holes evdref cty subst in
+        let instance = snd (list_filter2 (fun b c -> b) (filter,instance)) in
+        let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
+        evdref := evd;
+        evsref := (fst (destEvar ev),evty)::!evsref;
+        ev in
+      set_holes evdref (apply_on_subterm set_var c rhs) subst
+  | [] -> rhs in
+
+  let subst = make_subst (ctxt,args,argoccs) in
+
+  let evdref = ref evd in
+  let rhs = set_holes evdref rhs subst in
+  let evd = !evdref in
+
+  (* We instantiate the evars of which the value is forced by typing *)
+  let evd,rhs =
+    try !solve_evars env_evar evd rhs
+    with e when Pretype_errors.precatchable_exception e ->
+      (* Could not revert all subterms *)
+      raise Exit in
+
+  let rec abstract_free_holes evd = function
+  | (id,idty,c,_,evsref,_,_)::l ->
+      let rec force_instantiation evd = function
+      | (evk,evty)::evs ->
+          let evd =
+            if is_undefined evd evk then
+              (* We force abstraction over this unconstrained occurrence *)
+              (* and we use typing to propagate this instantiation *)
+              (* This is an arbitrary choice *)
+              let evd = Evd.define evk (mkVar id) evd in
+              let evd,b = evar_conv_x ts env_evar evd CUMUL idty evty in
+              if not b then error "Cannot find an instance";
+              let evd,b = reconsider_conv_pbs (evar_conv_x ts) evd in
+              if not b then error "Cannot find an instance";
+              evd
+            else
+              evd
+          in
+          force_instantiation evd evs
+      | [] ->
+          abstract_free_holes evd l
+      in
+      force_instantiation evd !evsref
+  | [] ->
+      Evd.define evk rhs evd in
+
+  abstract_free_holes evd subst, true
+  with Exit -> evd, false
+
+let second_order_matching_with_args ts env evd ev l t =
+(*
+  let evd,ev = evar_absorb_arguments env evd ev l in
+  let argoccs = array_map_to_list (fun _ -> None) (snd ev) in
+  second_order_matching ts env evd ev argoccs t
+*)
+  (evd,false)
+
+let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
+  let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
+  let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = decompose_app t1 in
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
   | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = []
-      & array_for_all (fun a -> a = term2 or isEvar a) args1 ->
+      & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
       choose_less_dependent_instance evk1 evd term2 args1, true
   | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
-      & array_for_all (fun a -> a = term1 or isEvar a) args2 ->
+      & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
       choose_less_dependent_instance evk2 evd term1 args2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
-      first_order_unification env evd (ev1,l1) appr2
+      (* and otherwise second-order matching *)
+      ise_try evd
+        [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2);
+         (fun evd ->
+           second_order_matching_with_args ts env evd ev1 l1 (applist appr2))]
   | _,Evar ev2 when List.length l2 <= List.length l1 ->
       (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
-      first_order_unification env evd (ev2,l2) appr1
+      (* and otherwise second-order matching *)
+      ise_try evd
+        [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1);
+         (fun evd ->
+           second_order_matching_with_args ts env evd ev2 l2 (applist appr1))]
+  | Evar ev1,_ ->
+      (* Try second-order pattern-matching *)
+      second_order_matching_with_args ts env evd ev1 l1 (applist appr2)
+  | _,Evar ev2 ->
+      (* Try second-order pattern-matching *)
+      second_order_matching_with_args ts env evd ev2 l2 (applist appr1)
   | _ ->
       (* Some head evar have been instantiated, or unknown kind of problem *)
-      evar_conv_x env evd pbty t1 t2
+      evar_conv_x ts env evd pbty t1 t2
+
+let check_problems_are_solved env evd =
+  match snd (extract_all_conv_pbs evd) with
+  | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
+  | _ -> ()
 
-let consider_remaining_unif_problems env evd =
+let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
-  List.fold_left
+  let heuristic_solved_evd = List.fold_left
     (fun evd (pbty,env,t1,t2) ->
-      let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in
+      let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
 	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
-    evd pbs
+    evd pbs in
+  check_problems_are_solved env heuristic_solved_evd;
+  Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
+			  |_,ImpossibleCase -> 
+			     Evd.define ev (j_type (coq_unit_judge ())) evd'
+			  |_ ->
+                             match ev_info.evar_candidates with
+                             | Some (a::l) -> Evd.define ev a evd'
+                             | Some [] -> error "Unsolvable existential variables"
+                             | None -> evd') heuristic_solved_evd heuristic_solved_evd
 
 (* Main entry points *)
 
-let the_conv_x     env t1 t2 evd =
-  match evar_conv_x env evd CONV  t1 t2 with
+let the_conv_x ?(ts=full_transparent_state) env t1 t2 evd =
+  match evar_conv_x ts env evd CONV  t1 t2 with
       (evd',true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-let the_conv_x_leq env t1 t2 evd =
-  match evar_conv_x env evd CUMUL t1 t2 with
+let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd =
+  match evar_conv_x ts env evd CUMUL t1 t2 with
       (evd', true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-let e_conv env evd t1 t2 =
-  match evar_conv_x env !evd CONV t1 t2 with
+let e_conv ?(ts=full_transparent_state) env evd t1 t2 =
+  match evar_conv_x ts env !evd CONV t1 t2 with
       (evd',true) -> evd := evd'; true
     | _ -> false
 
-let e_cumul env evd t1 t2 =
-  match evar_conv_x env !evd CUMUL t1 t2 with
+let e_cumul ?(ts=full_transparent_state) env evd t1 t2 =
+  match evar_conv_x ts env !evd CUMUL t1 t2 with
       (evd',true) -> evd := evd'; true
     | _ -> false