Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

18 files changed, 1068 insertions, 727 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8963ea5e..9ed28f8b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -77,8 +77,9 @@ let rec list_try_compile f = function
   | [] -> anomaly "try_find_f"
   | h::t ->
       try f h
-      with UserError _ | TypeError _ | PretypeError _
-	| Loc.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
+      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _
+	| Loc.Exc_located
+	    (_, (UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _)) ->
 	    list_try_compile f t
 
 let force_name =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 553c9127..bfa0034f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -110,7 +110,7 @@ module Default = struct
 
   let saturate_evd env evd =
     Typeclasses.resolve_typeclasses
-      ~onlyargs:true ~split:true ~fail:false env evd
+      ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
 
   (* appliquer le chemin de coercions p à hj *)
   let apply_coercion env sigma p hj typ_cl =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c194a0f2..aae003b8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -532,7 +532,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
   buildrec [] [] avoid env construct_nargs branch
 
 and detype_binder isgoal bk avoid env na ty c =
-  let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
+  let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
   let na',avoid' =
     if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
     else compute_displayed_name_in flag avoid na c in
@@ -552,9 +552,11 @@ let rec detype_rel_context where avoid env sign =
 	| None -> na,avoid
 	| Some c ->
 	    if b<>None then
-	      compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+	      compute_displayed_let_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c
 	    else
-	      compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
+	      compute_displayed_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c in
       let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
       (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 04f86e70..fa45f6fb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -195,7 +195,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
           evar_eqappr_x ts env evd pbty
             (decompose_app term1) (decompose_app term2)
 
-and evar_eqappr_x ?(rhs_is_stuck_proj = false)
+and evar_eqappr_x ?(rhs_is_already_stuck = 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
@@ -324,13 +324,25 @@ and evar_eqappr_x ?(rhs_is_stuck_proj = false)
           (* heuristic: unfold second argument first, exception made
              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 *)
-          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
+             usable as a canonical projection or canonical value *)
+          let rec is_unnamed (hd, args) = match kind_of_term hd with
+            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) -> false
+            | (Case _|Fix _|CoFix _|Meta _|Rel _)-> true
+            | Evar _ -> false (* immediate solution without Canon Struct *)
+            | Lambda _ -> assert(args = []); true
+            | LetIn (_,b,_,c) -> 
+                is_unnamed (evar_apprec ts env i args (subst1 b c))
+            | App _| Cast _ -> assert false in
+          let rhs_is_stuck_and_unnamed () =
+            match eval_flexible_term ts env flex2 with
+            | None -> false
+            | Some v2 -> is_unnamed (evar_apprec ts env i l2 v2) in
+          let rhs_is_already_stuck =
+            rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
+	  if isLambda flex1 || rhs_is_already_stuck then
 	    match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x ~rhs_is_stuck_proj 
+		evar_eqappr_x ~rhs_is_already_stuck 
                   ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None ->
 		match eval_flexible_term ts env flex2 with
@@ -544,7 +556,7 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
     (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 *)
+(* getting rid of the optional argument rhs_is_already_stuck *)
 let evar_eqappr_x ts env evd pbty appr1 appr2 =
   evar_eqappr_x ts env evd pbty appr1 appr2
 
@@ -582,17 +594,19 @@ let apply_on_subterm f c t =
   in
   applyrec (0,c) t
 
-let filter_possible_projections c args =
+let filter_possible_projections c ty ctxt args =
   let fv1 = free_rels c in
   let fv2 = collect_vars c in
-  List.map (fun a ->
+  let tyvars = collect_vars ty in
+  List.map2 (fun (id,_,_) 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
+    isVar a && Idset.mem (destVar a) fv2 ||
+    Idset.mem id tyvars)
+    ctxt args
 
 let initial_evar_data evi =
   let ids = List.map pi1 (evar_context evi) in
@@ -629,16 +643,17 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   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 ->
+  | (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 ->
+        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)
+      let filter' = filter_possible_projections c ty ctxt args in
+      let filter = List.map2 (&&) filter filter' in
+      (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt',l,occsl)
   | [], [], [] -> []
   | _ -> anomaly "Signature, instance and occurrences list do not match" in
 
@@ -724,6 +739,12 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
       choose_less_dependent_instance evk2 evd term1 args2, true
+  | Evar (evk1,args1), Evar (evk2,args2) when evk1 = evk2 ->
+      let f env evd pbty x y = (evd,is_trans_fconv pbty ts env evd x y) in
+      solve_refl ~can_drop:true f env evd evk1 args1 args2, true
+  | Evar ev1, Evar ev2 ->
+      solve_evar_evar ~force:true
+        (evar_define (evar_conv_x ts)) (evar_conv_x ts) env evd ev1 ev2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       (* and otherwise second-order matching *)
@@ -753,7 +774,52 @@ let check_problems_are_solved env evd =
   | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
   | _ -> ()
 
+let max_undefined_with_candidates evd =
+  (* If evar were ordered with highest index first, fold_undefined
+     would be going decreasingly and we could use fold_undefined to
+     find the undefined evar of maximum index (alternatively,
+     max_bindings from ocaml 3.12 could be used); instead we traverse
+     the whole map *)
+  let l = Evd.fold_undefined
+    (fun evk ev_info evars ->
+        match ev_info.evar_candidates with
+        | None -> evars
+        | Some l -> (evk,ev_info,l)::evars) evd [] in
+  match l with
+  | [] -> None
+  | a::l -> Some (list_last (a::l))
+
+let rec solve_unconstrained_evars_with_canditates evd =
+  (* max_undefined is supposed to return the most recent, hence
+     possibly most dependent evar *)
+  match max_undefined_with_candidates evd with
+  | None -> evd
+  | Some (evk,ev_info,l) ->
+      let rec aux = function
+      | [] -> error "Unsolvable existential variables."
+      | a::l ->
+          try
+            let conv_algo = evar_conv_x full_transparent_state in
+            let evd = check_evar_instance evd evk a conv_algo in
+            let evd = Evd.define evk a evd in
+            let evd,b = reconsider_conv_pbs conv_algo evd in
+            if b then solve_unconstrained_evars_with_canditates evd
+            else aux l
+          with e when Pretype_errors.precatchable_exception e ->
+            aux l in
+      (* List.rev is there to favor most dependent solutions *)
+      (* and favor progress when used with the refine tactics *)
+      let evd = aux (List.rev l) in
+      solve_unconstrained_evars_with_canditates evd
+
+let solve_unconstrained_impossible_cases evd =
+  Evd.fold_undefined (fun evk ev_info evd' ->
+    match ev_info.evar_source with
+    | _,ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd'
+    | _ -> evd') evd evd
+
 let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
+  let evd = solve_unconstrained_evars_with_canditates evd in
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = List.fold_left
     (fun evd (pbty,env,t1,t2) ->
@@ -761,14 +827,7 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
 	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
     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
+  solve_unconstrained_impossible_cases heuristic_solved_evd
 
 (* Main entry points *)
 
@@ -782,12 +841,12 @@ let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd =
       (evd', true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-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
+let e_conv ?(ts=full_transparent_state) env evdref t1 t2 =
+  match evar_conv_x ts env !evdref CONV t1 t2 with
+      (evd',true) -> evdref := evd'; true
     | _ -> false
 
-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
+let e_cumul ?(ts=full_transparent_state) env evdref t1 t2 =
+  match evar_conv_x ts env !evdref CUMUL t1 t2 with
+      (evd',true) -> evdref := evd'; true
     | _ -> false
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 7d66bee0..689fab50 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -21,8 +21,11 @@ open Reductionops
 open Pretype_errors
 open Retyping
 
-(* Expanding existential variables *)
-(* 1- flush_and_check_evars fails if an existential is undefined *)
+(****************************************************)
+(* Expanding/testing/exposing existential variables *)
+(****************************************************)
+
+(* flush_and_check_evars fails if an existential is undefined *)
 
 exception Uninstantiated_evar of existential_key
 
@@ -71,6 +74,77 @@ let nf_evars_undefined evm =
 let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
 let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd
 
+(*-------------------*)
+(* Auxiliary functions for the conversion algorithms modulo evars
+ *)
+
+let has_undefined_evars_or_sorts evd t =
+  let rec has_ev t =
+    match kind_of_term t with
+    | Evar (ev,args) ->
+        (match evar_body (Evd.find evd ev) with
+        | Evar_defined c ->
+            has_ev c; Array.iter has_ev args
+        | Evar_empty ->
+	    raise NotInstantiatedEvar)
+    | Sort s when is_sort_variable evd s -> raise Not_found
+    | _ -> iter_constr has_ev t in
+  try let _ = has_ev t in false
+  with (Not_found | NotInstantiatedEvar) -> true
+
+let is_ground_term evd t =
+  not (has_undefined_evars_or_sorts evd t)
+
+let is_ground_env evd env =
+  let is_ground_decl = function
+      (_,Some b,_) -> is_ground_term evd b
+    | _ -> true in
+  List.for_all is_ground_decl (rel_context env) &&
+  List.for_all is_ground_decl (named_context env)
+(* Memoization is safe since evar_map and environ are applicative
+   structures *)
+let is_ground_env = memo1_2 is_ground_env
+
+(* Return the head evar if any *)
+
+exception NoHeadEvar
+
+let head_evar =
+  let rec hrec c = match kind_of_term c with
+    | Evar (evk,_)   -> evk
+    | Case (_,_,c,_) -> hrec c
+    | App (c,_)      -> hrec c
+    | Cast (c,_,_)   -> hrec c
+    | _              -> raise NoHeadEvar
+  in
+  hrec
+
+(* Expand head evar if any (currently consider only applications but I
+   guess it should consider Case too) *)
+
+let whd_head_evar_stack sigma c =
+  let rec whrec (c, l as s) =
+    match kind_of_term c with
+      | Evar (evk,args as ev) when Evd.is_defined sigma evk
+	  -> whrec (existential_value sigma ev, l)
+      | Cast (c,_,_) -> whrec (c, l)
+      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+      | _ -> s
+  in
+  whrec (c, [])
+
+let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
+
+let noccur_evar evd evk c =
+  let rec occur_rec c = match kind_of_term c with
+  | Evar (evk',_ as ev') ->
+      (match safe_evar_value evd ev' with
+       | Some c -> occur_rec c
+       | None -> if evk = evk' then raise Occur)
+  | _ -> iter_constr occur_rec c
+  in
+  try occur_rec c; true with Occur -> false
+
 (**********************)
 (* Creating new metas *)
 (**********************)
@@ -125,6 +199,19 @@ let evars_to_metas sigma (emap, c) =
   let emap = nf_evar_map_undefined emap in
   let sigma',emap' = push_dependent_evars sigma emap in
   let sigma',emap' = push_duplicated_evars sigma' emap' c in
+  (* if an evar has been instantiated in [emap] (as part of typing [c])
+     then it is instantiated in [sigma]. *)
+  let repair_evars sigma emap =
+    fold_undefined begin fun ev _ sigma' ->
+      try
+	let info = find emap ev in
+	match evar_body info with
+	| Evar_empty -> sigma'
+	| Evar_defined body -> define ev body sigma'
+      with Not_found -> sigma'
+    end sigma sigma
+  in
+  let sigma' = repair_evars sigma' emap in
   let change_exist evar =
     let ty = nf_betaiota emap (existential_type emap evar) in
     let n = new_meta() in
@@ -141,6 +228,18 @@ let non_instantiated sigma =
   let listev = Evd.undefined_list sigma in
   List.map (fun (ev,evi) -> (ev,nf_evar_info sigma evi)) listev
 
+(************************)
+(* Manipulating filters *)
+(************************)
+
+let apply_subfilter filter subfilter =
+  fst (List.fold_right (fun oldb (l,filter) ->
+    if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
+         filter ([], List.rev subfilter))
+
+let extract_subfilter initial_filter refined_filter =
+  snd (list_filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
+
 (**********************)
 (* Creating new evars *)
 (**********************)
@@ -158,14 +257,153 @@ let new_untyped_evar =
  * functional operations on evar sets *
  *------------------------------------*)
 
-let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter ?candidates instance =
-  assert
-    (let ctxt = named_context_of_val sign in
-     list_distinct (ids_of_named_context ctxt));
+(* [push_rel_context_to_named_context] builds the defining context and the
+ * initial instance of an evar. If the evar is to be used in context
+ *
+ * Gamma =  a1     ...    an xp      ...       x1
+ *          \- named part -/ \- de Bruijn part -/
+ *
+ * then the x1...xp are turned into variables so that the evar is declared in
+ * context
+ *
+ *          a1     ...    an xp      ...       x1
+ *          \----------- named part ------------/
+ *
+ * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
+ * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
+ * in context Gamma.
+ *
+ * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
+ * Remark 2: If some of the ai or xj are definitions, we keep them in the
+ *   instance. This is necessary so that no unfolding of local definitions
+ *   happens when inferring implicit arguments (consider e.g. the problem
+ *   "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
+ *   produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
+ *   the hole to be instantiated by x', not by x (which would have been
+ *   the case in [invert_definition] if x' had disappeared from the instance).
+ *   Note that at any time, if, in some context env, the instance of
+ *   declaration x:A is t and the instance of definition x':=phi(x) is u, then
+ *   we have the property that u and phi(t) are convertible in env.
+ *)
+
+let push_rel_context_to_named_context env typ =
+  (* compute the instances relative to the named context and rel_context *)
+  let ids = List.map pi1 (named_context env) in
+  let inst_vars = List.map mkVar ids in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
+  (* move the rel context to a named context and extend the named instance *)
+  (* with vars of the rel context *)
+  (* We do keep the instances corresponding to local definition (see above) *)
+  let (subst, _, env) =
+    Sign.fold_rel_context
+      (fun (na,c,t) (subst, avoid, env) ->
+	let id = next_name_away na avoid in
+	let d = (id,Option.map (substl subst) c,substl subst t) in
+	(mkVar id :: subst, id::avoid, push_named d env))
+      (rel_context env) ~init:([], ids, env) in
+  (named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
+
+(*------------------------------------*
+ * Entry points to define new evars   *
+ *------------------------------------*)
+
+let default_source = (dummy_loc,InternalHole)
+
+let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
   let newevk = new_untyped_evar() in
-  let evd = evar_declare sign newevk typ ~src:src ?filter ?candidates evd in
+  let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in
+  (evd,newevk)
+
+let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
+  assert (not !Flags.debug ||
+            list_distinct (ids_of_named_context (named_context_of_val sign)));
+  let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
   (evd,mkEvar (newevk,Array.of_list instance))
 
+(* [new_evar] declares a new existential in an env env with type typ *)
+(* Converting the env into the sign of the evar to define *)
+
+let new_evar evd env ?src ?filter ?candidates typ =
+  let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
+  let candidates = Option.map (List.map (substl subst)) candidates in
+  let instance =
+    match filter with
+    | None -> instance
+    | Some filter -> list_filter_with filter instance in
+  new_evar_instance sign evd typ' ?src ?filter ?candidates instance
+
+let new_type_evar ?src ?filter evd env =
+  let evd', s = new_sort_variable evd in
+  new_evar evd' env ?src ?filter (mkSort s)
+
+  (* The same using side-effect *)
+let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty =
+  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
+  evdref := evd';
+  ev
+
+(*------------------------------------*
+ * Restricting existing evars         *
+ *------------------------------------*)
+
+let restrict_evar_key evd evk filter candidates =
+  if filter = None && candidates = None then
+    evd,evk
+  else
+    let evi = Evd.find_undefined evd evk in
+    let oldfilter = evar_filter evi in
+    if filter = Some oldfilter && candidates = None then
+      evd,evk
+    else
+    let filter =
+      match filter with
+      | None -> evar_filter evi
+      | Some filter -> filter in
+    let candidates =
+      match candidates with None -> evi.evar_candidates | _ -> candidates in
+    let ccl = evi.evar_concl in
+    let sign = evar_hyps evi in
+    let src = evi.evar_source in
+    let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
+    let ctxt = snd (list_filter2 (fun b c -> b) (filter,evar_context evi)) in
+    let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
+    Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
+
+(* Restrict an applied evar and returns its restriction in the same context *)
+let restrict_applied_evar evd (evk,argsv) filter candidates =
+  let evd,newevk = restrict_evar_key evd evk filter candidates in
+  let newargsv = match filter with
+  | None -> (* optim *) argsv
+  | Some filter ->
+      let evi = Evd.find evd evk in
+      let subfilter = extract_subfilter (evar_filter evi) filter in
+      array_filter_with subfilter argsv in
+  evd,(newevk,newargsv)
+
+(* Restrict an evar in the current evar_map *)
+let restrict_evar evd evk filter candidates =
+  fst (restrict_evar_key evd evk filter candidates)
+
+(* Restrict an evar in the current evar_map *)
+let restrict_instance evd evk filter argsv =
+  match filter with None -> argsv | Some filter ->
+  let evi = Evd.find evd evk in
+  array_filter_with (extract_subfilter (evar_filter evi) filter) argsv
+
+(* This assumes an evar with identity instance and generalizes it over only
+   the De Bruijn part of the context *)
+let generalize_evar_over_rels sigma (ev,args) =
+  let evi = Evd.find sigma ev in
+  let sign = named_context_of_val evi.evar_hyps in
+  List.fold_left2
+    (fun (c,inst as x) a d ->
+      if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
+     (evi.evar_concl,[]) (Array.to_list args) sign
+
+(***************************************)
+(* Managing chains of local definitons *)
+(***************************************)
+
 (* Expand rels and vars that are bound to other rels or vars so that
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
@@ -209,6 +447,12 @@ let make_alias_map env =
   let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in
   (var_aliases,rel_aliases)
 
+let lift_aliases n (var_aliases,rel_aliases as aliases) =
+  if n = 0 then aliases else
+  (var_aliases,
+   Intmap.fold (fun p l -> Intmap.add (p+n) (List.map (lift n) l))
+     rel_aliases Intmap.empty)
+
 let get_alias_chain_of aliases x = match kind_of_term x with
   | Rel n -> (try Intmap.find n (snd aliases) with Not_found -> [])
   | Var id -> (try Idmap.find id (fst aliases) with Not_found -> [])
@@ -250,6 +494,11 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) =
     | None -> rel_aliases in
   (var_aliases, rel_aliases)
 
+let expand_alias_once aliases x =
+  match get_alias_chain_of aliases x with
+  | []  -> None
+  | l -> Some (list_last l)
+
 let rec expansions_of_var aliases x =
   match get_alias_chain_of aliases x with
   | [] -> [x]
@@ -272,15 +521,25 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Intset.empty and acc2 = ref Idset.empty in
-  let rec frec (aliases,depth) c = match kind_of_term c with
-    | Rel _ | Var _ ->
+  let cache_rel = ref Intset.empty and cache_var = ref Idset.empty in
+  let is_in_cache depth = function
+    | Rel n -> Intset.mem (n-depth) !cache_rel
+    | Var s -> Idset.mem s !cache_var
+    | _ -> false in
+  let put_in_cache depth = function
+    | Rel n -> cache_rel := Intset.add (n-depth) !cache_rel
+    | Var s -> cache_var := Idset.add s !cache_var
+    | _ -> () in
+  let rec frec (aliases,depth) c =
+    match kind_of_term c with
+    | Rel _ | Var _ as ck ->
+      if is_in_cache depth ck then () else begin
+      put_in_cache depth ck;
       let c = expansion_of_var aliases c in
-        (match kind_of_term c with
+        match kind_of_term c with
         | Var id -> acc2 := Idset.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1
-        | _ -> 
-            (* not optimal: would need sharing if alias occurs more than once *)
-            frec (aliases,depth) c)
+        | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
         acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2
     | _ ->
@@ -291,259 +550,9 @@ let free_vars_and_rels_up_alias_expansion aliases c =
   frec (aliases,0) c;
   (!acc1,!acc2)
 
-(* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
- * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
- * If a variable and an alias of it are bound to the same instance, we skip
- * the alias (we just use eq_constr -- instead of conv --, since anyway,
- * only instances that are variables -- or evars -- are later considered;
- * morever, we can bet that similar instances came at some time from
- * the very same substitution. The removal of aliased duplicates is
- * useful to ensure the uniqueness of a projection.
-*)
-
-let make_projectable_subst aliases sigma evi args =
-  let sign = evar_filtered_context evi in
-  let evar_aliases = compute_var_aliases sign in
-  let (_,full_subst,cstr_subst) =
-    List.fold_right
-      (fun (id,b,c) (args,all,cstrs) ->
-        match b,args with
-	| None, a::rest ->
-	    let a = whd_evar sigma a in
-	    let cstrs =
-	      let a',args = decompose_app_vect a in
-	      match kind_of_term a' with
-	      | Construct cstr ->
-		  let l = try Constrmap.find cstr cstrs with Not_found -> [] in
-		  Constrmap.add cstr ((args,id)::l) cstrs
-	      | _ -> cstrs in
-	    (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
-	| Some c, a::rest ->
-	    let a = whd_evar sigma a in
-	    (match kind_of_term c with
-	    | Var id' ->
-		let idc = normalize_alias_var evar_aliases id' in
-		let sub = try Idmap.find idc all with Not_found -> [] in
-		if List.exists (fun (c,_,_) -> eq_constr a c) sub then
-		  (rest,all,cstrs)
-		else
-		  (rest,
-		   Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
-		   cstrs)
-	    | _ ->
-		(rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
-	| _ -> anomaly "Instance does not match its signature")
-      sign (array_rev_to_list args,Idmap.empty,Constrmap.empty) in
-  (full_subst,cstr_subst)
-
-let make_pure_subst evi args =
-  snd (List.fold_right
-    (fun (id,b,c) (args,l) ->
-      match args with
-	| a::rest -> (rest, (id,a)::l)
-	| _ -> anomaly "Instance does not match its signature")
-    (evar_filtered_context evi) (array_rev_to_list args,[]))
-
-(* [push_rel_context_to_named_context] builds the defining context and the
- * initial instance of an evar. If the evar is to be used in context
- *
- * Gamma =  a1     ...    an xp      ...       x1
- *          \- named part -/ \- de Bruijn part -/
- *
- * then the x1...xp are turned into variables so that the evar is declared in
- * context
- *
- *          a1     ...    an xp      ...       x1
- *          \----------- named part ------------/
- *
- * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
- * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
- * in context Gamma.
- *
- * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
- * Remark 2: If some of the ai or xj are definitions, we keep them in the
- *   instance. This is necessary so that no unfolding of local definitions
- *   happens when inferring implicit arguments (consider e.g. the problem
- *   "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
- *   produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
- *   the hole to be instantiated by x', not by x (which would have been
- *   the case in [invert_definition] if x' had disappeared from the instance).
- *   Note that at any time, if, in some context env, the instance of
- *   declaration x:A is t and the instance of definition x':=phi(x) is u, then
- *   we have the property that u and phi(t) are convertible in env.
- *)
-
-let push_rel_context_to_named_context env typ =
-  (* compute the instances relative to the named context and rel_context *)
-  let ids = List.map pi1 (named_context env) in
-  let inst_vars = List.map mkVar ids in
-  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
-  (* move the rel context to a named context and extend the named instance *)
-  (* with vars of the rel context *)
-  (* We do keep the instances corresponding to local definition (see above) *)
-  let (subst, _, env) =
-    Sign.fold_rel_context
-      (fun (na,c,t) (subst, avoid, env) ->
-	let id = next_name_away na avoid in
-	let d = (id,Option.map (substl subst) c,substl subst t) in
-	(mkVar id :: subst, id::avoid, push_named d env))
-      (rel_context env) ~init:([], ids, env) in
-  (named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
-
-(* [new_evar] declares a new existential in an env env with type typ *)
-(* Converting the env into the sign of the evar to define *)
-
-let new_evar evd env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates typ =
-  let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
-  let candidates = Option.map (List.map (substl subst)) candidates in
-  let instance =
-    match filter with
-    | None -> instance
-    | Some filter -> snd (list_filter2 (fun b c -> b) (filter,instance)) in
-  new_evar_instance sign evd typ' ~src:src ?filter ?candidates instance
-
-  (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty =
-  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
-  evdref := evd';
-  ev
-
-(* This assumes an evar with identity instance and generalizes it over only
-   the de Bruijn part of the context *)
-let generalize_evar_over_rels sigma (ev,args) =
-  let evi = Evd.find sigma ev in
-  let sign = named_context_of_val evi.evar_hyps in
-  List.fold_left2
-    (fun (c,inst as x) a d ->
-      if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
-     (evi.evar_concl,[]) (Array.to_list args) sign
-
-(*------------------------------------*
- * operations on the evar constraints *
- *------------------------------------*)
-
-exception IllTypedFilter
-
-let check_restricted_occur evd refine env filter constr =
-  let filter = Array.of_list filter in
-  let rec aux k c =
-    let c = whd_evar evd c in
-    match kind_of_term c with
-    | Var id ->
-      let idx = list_try_find_i (fun i (id', _, _) -> if id' = id then i else raise (Failure "")) 0 env in
-	if not filter.(idx)
-	then if refine then
-	  (filter.(idx) <- true; c)
-	else raise IllTypedFilter
-	else c
-    | _ -> map_constr_with_binders succ aux k c
-  in
-  let res = aux 0 constr in
-    Array.to_list filter, res
-
-(* We have a unification problem Σ; Γ |- ?e[u1..uq] = t : s where ?e is not yet
- * declared in Σ but yet known to be declarable in some context x1:T1..xq:Tq.
- * [define_evar_from_virtual_equation ... Γ Σ t (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)]
- * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
- *)
-
-let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env
-    inst_in_sign =
-  let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
-  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
-  let t_in_env = whd_evar evd t_in_env in
-  let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
-  let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
-  (evd,whd_evar evd evar_in_sign)
-
-(* We have x1..xq |- ?e1 : Ï„ and had to solve something like
- * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
- * ?e2[v1..vn], hence flexible. We had to go through k binders and now
- * virtually have x1..xq, y1'..yk' | ?e1' : Ï„' and the equation
- * Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
- * [materialize_evar Γ evd k (?e1[u1..uq]) τ'] extends Σ with the declaration
- * of ?e1' and returns both its instance ?e1'[x1..xq y1..yk] in an extension
- * of the context of e1 so that e1 can be instantiated by
- * (...\y1' ... \yk' ... ?e1'[x1..xq y1'..yk']),
- * and the instance ?e1'[u1..uq y1..yk] so that the remaining equation
- * ?e1'[u1..uq y1..yk] = c can be registered
- *
- * Note that, because invert_definition does not check types, we need to
- * guess the types of y1'..yn' by inverting the types of y1..yn along the
- * substitution u1..uq.
- *)
-
-let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
-  let evi1 = Evd.find_undefined evd evk1 in
-  let env1,rel_sign = env_rel_context_chop k env in
-  let sign1 = evar_hyps evi1 in
-  let filter1 = evar_filter evi1 in
-  let ids1 = List.map pi1 (named_context_of_val sign1) in
-  let inst_in_sign =
-    List.map mkVar (snd (list_filter2 (fun b id -> b) (filter1,ids1))) in
-  let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
-    List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
-      match b with
-      | None ->
-          let id = next_name_away na avoid in
-          let evd,t_in_sign =
-            define_evar_from_virtual_equation define_fun env evd t_in_env
-              sign filter inst_in_env inst_in_sign in
-          (push_named_context_val (id,None,t_in_sign) sign,true::filter,
-           (mkRel 1)::(List.map (lift 1) inst_in_env),(mkVar id)::inst_in_sign,
-           push_rel d env,evd,id::avoid)
-      | Some b ->
-          (sign,filter,inst_in_env,inst_in_sign,
-           push_rel d env,evd,avoid))
-      rel_sign
-      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
-  in
-  let evd,ev2ty_in_sign =
-    define_evar_from_virtual_equation define_fun env evd ty_in_env
-      sign2 filter2 inst2_in_env inst2_in_sign in
-  let evd,ev2_in_sign =
-    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
-  let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
-  (evd, ev2_in_sign, ev2_in_env)
-
-let subfilter env ccl filter newfilter args =
-  let vars = collect_vars ccl in
-  let (filter, _, _, newargs) =
-    List.fold_left2
-      (fun (filter, newl, args, newargs) oldf (n, _, _) ->
-       if oldf then
-	 let a, oldargs = match args with hd :: tl -> hd, tl | _ -> assert false in
-	   if Idset.mem n vars then
-	     (oldf :: filter, List.tl newl, oldargs, a :: newargs)
-	   else if List.hd newl then (true :: filter, List.tl newl, oldargs, a :: newargs)
-	   else (false :: filter, List.tl newl, oldargs, newargs)
-       else (oldf :: filter, newl, args, newargs))
-    ([], newfilter, args, []) filter env
-  in List.rev filter, List.rev newargs
-
-let restrict_upon_filter ?(refine=false) evd evi evk p args =
-  let filter = evar_filter evi in
-  let newfilter = List.map p args in
-  let env = evar_unfiltered_env evi in
-  let ccl = nf_evar evd evi.evar_concl in
-  let newfilter, newargs =
-    subfilter (named_context env) ccl filter newfilter args
-  in
-  if newfilter <> filter then
-    let (evd,newev) = new_evar evd env ~src:(evar_source evk evd)
-	~filter:newfilter ccl in
-    let evd = Evd.define evk newev evd in
-      evd,fst (destEvar newev), newargs
-  else
-    evd,evk,args
-
-let collect_vars c =
-  let rec collrec acc c =
-    match kind_of_term c with
-    | Var id -> list_add_set id acc
-    | _      -> fold_constr collrec acc c
-  in
-  collrec [] c
+(************************************)
+(* Removing a dependency in an evar *)
+(************************************)
 
 type clear_dependency_error =
 | OccurHypInSimpleClause of identifier option
@@ -590,7 +599,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 		  (* Check if some id to clear occurs in the instance
 		     a of rid in ev and remember the dependency *)
 		  match
-		    List.filter (fun id -> List.mem id ids) (collect_vars a)
+		    List.filter (fun id -> List.mem id ids) (Idset.elements (collect_vars a))
 		  with
 		  | id :: _ -> (hy,ar,(rid,id)::ri)
 		  | _ ->
@@ -655,6 +664,255 @@ let clear_hyps_in_evi evdref hyps concl ids =
   in
   (nhyps,nconcl)
 
+(********************************)
+(* Managing pattern-unification *)
+(********************************)
+
+let rec expand_and_check_vars aliases = function
+  | [] -> []
+  | a::l when isRel a or isVar a ->
+      let a = expansion_of_var aliases a in
+      if isRel a or isVar a then a :: expand_and_check_vars aliases l
+      else raise Exit
+  | _ ->
+      raise Exit
+
+module Constrhash = Hashtbl.Make
+  (struct type t = constr
+	  let equal = eq_constr
+	  let hash = hash_constr
+   end)
+
+let rec constr_list_distinct l =
+  let visited = Constrhash.create 23 in
+  let rec loop = function
+    | h::t ->
+	if Constrhash.mem visited h then false
+	else (Constrhash.add visited h h; loop t)
+    | [] -> true
+  in loop l
+
+let get_actual_deps aliases l t =
+  if occur_meta_or_existential t then
+    (* Probably no restrictions on allowed vars in presence of evars *)
+    l
+  else
+    (* Probably strong restrictions coming from t being evar-closed *)
+    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+    List.filter (fun c ->
+      match kind_of_term c with
+      | Var id -> Idset.mem id fv_ids
+      | Rel n -> Intset.mem n fv_rels
+      | _ -> assert false) l
+
+let remove_instance_local_defs evd evk args =
+  let evi = Evd.find evd evk in
+  let rec aux = function
+  | (_,Some _,_)::sign, a::args -> aux (sign,args)
+  | (_,None,_)::sign, a::args -> a::aux (sign,args)
+  | [], [] -> []
+  | _ -> assert false in
+  aux (evar_filtered_context evi, args)
+
+(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
+
+let find_unification_pattern_args env l t =
+  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
+    let aliases = make_alias_map env in
+    match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
+    | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
+    | _ -> None
+  else
+    None
+
+let is_unification_pattern_meta env nb m l t =
+  (* Variables from context and rels > nb are implicitly all there *)
+  (* so we need to be a rel <= nb *)
+  if List.for_all (fun x -> isRel x && destRel x <= nb) l then
+    match find_unification_pattern_args env l t with
+    | Some _ as x when not (dependent (mkMeta m) t) -> x
+    | _ -> None
+  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 evd evk t then
+    let args = remove_instance_local_defs evd evk (Array.to_list 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 =
+  is_unification_pattern_evar env evd (evk,args) [] t <> None
+
+let is_unification_pattern (env,nb) evd f l t =
+  match kind_of_term f with
+  | Meta m -> is_unification_pattern_meta env nb m l t
+  | Evar ev -> is_unification_pattern_evar env evd ev l t
+  | _ -> None
+
+(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
+   (pattern unification). It is assumed that l is made of rel's that
+   are distinct and not bound to aliases. *)
+(* It is also assumed that c does not contain metas because metas
+   *implicitly* depend on Vars but lambda abstraction will not reflect this
+   dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
+   return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
+let solve_pattern_eqn env l c =
+  let c' = List.fold_right (fun a c ->
+    let c' = subst_term (lift 1 a) (lift 1 c) in
+    match kind_of_term a with
+      (* Rem: if [a] links to a let-in, do as if it were an assumption *)
+      | Rel n ->
+          let d = map_rel_declaration (lift n) (lookup_rel n env) in
+          mkLambda_or_LetIn d c'
+      | Var id ->
+          let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
+      | _ -> assert false)
+    l c in
+  (* Warning: we may miss some opportunity to eta-reduce more since c'
+     is not in normal form *)
+  whd_eta c'
+
+(*****************************************)
+(* Refining/solving unification problems *)
+(*****************************************)
+
+(* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
+ * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
+ * If a variable and an alias of it are bound to the same instance, we skip
+ * the alias (we just use eq_constr -- instead of conv --, since anyway,
+ * only instances that are variables -- or evars -- are later considered;
+ * morever, we can bet that similar instances came at some time from
+ * the very same substitution. The removal of aliased duplicates is
+ * useful to ensure the uniqueness of a projection.
+*)
+
+let make_projectable_subst aliases sigma evi args =
+  let sign = evar_filtered_context evi in
+  let evar_aliases = compute_var_aliases sign in
+  let (_,full_subst,cstr_subst) =
+    List.fold_right
+      (fun (id,b,c) (args,all,cstrs) ->
+        match b,args with
+	| None, a::rest ->
+	    let a = whd_evar sigma a in
+	    let cstrs =
+	      let a',args = decompose_app_vect a in
+	      match kind_of_term a' with
+	      | Construct cstr ->
+		  let l = try Constrmap.find cstr cstrs with Not_found -> [] in
+		  Constrmap.add cstr ((args,id)::l) cstrs
+	      | _ -> cstrs in
+	    (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
+	| Some c, a::rest ->
+	    let a = whd_evar sigma a in
+	    (match kind_of_term c with
+	    | Var id' ->
+		let idc = normalize_alias_var evar_aliases id' in
+		let sub = try Idmap.find idc all with Not_found -> [] in
+		if List.exists (fun (c,_,_) -> eq_constr a c) sub then
+		  (rest,all,cstrs)
+		else
+		  (rest,
+		   Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
+		   cstrs)
+	    | _ ->
+		(rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
+	| _ -> anomaly "Instance does not match its signature")
+      sign (array_rev_to_list args,Idmap.empty,Constrmap.empty) in
+  (full_subst,cstr_subst)
+
+let make_pure_subst evi args =
+  snd (List.fold_right
+    (fun (id,b,c) (args,l) ->
+      match args with
+	| a::rest -> (rest, (id,a)::l)
+	| _ -> anomaly "Instance does not match its signature")
+    (evar_filtered_context evi) (array_rev_to_list args,[]))
+
+(*------------------------------------*
+ * operations on the evar constraints *
+ *------------------------------------*)
+
+(* We have a unification problem Σ; Γ |- ?e[u1..uq] = t : s where ?e is not yet
+ * declared in Σ but yet known to be declarable in some context x1:T1..xq:Tq.
+ * [define_evar_from_virtual_equation ... Γ Σ t (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)]
+ * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
+ *)
+
+let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env =
+  let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
+  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
+  let t_in_env = whd_evar evd t_in_env in
+  let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
+  let ids = List.map pi1 (named_context_of_val sign) in
+  let inst_in_sign = List.map mkVar (list_filter_with filter ids) in
+  let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
+  (evd,whd_evar evd evar_in_sign)
+
+(* We have x1..xq |- ?e1 : Ï„ and had to solve something like
+ * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
+ * ?e2[v1..vn], hence flexible. We had to go through k binders and now
+ * virtually have x1..xq, y1'..yk' | ?e1' : Ï„' and the equation
+ * Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
+ * [materialize_evar Γ evd k (?e1[u1..uq]) τ'] extends Σ with the declaration
+ * of ?e1' and returns both its instance ?e1'[x1..xq y1..yk] in an extension
+ * of the context of e1 so that e1 can be instantiated by
+ * (...\y1' ... \yk' ... ?e1'[x1..xq y1'..yk']),
+ * and the instance ?e1'[u1..uq y1..yk] so that the remaining equation
+ * ?e1'[u1..uq y1..yk] = c can be registered
+ *
+ * Note that, because invert_definition does not check types, we need to
+ * guess the types of y1'..yn' by inverting the types of y1..yn along the
+ * substitution u1..uq.
+ *)
+
+let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+  let evi1 = Evd.find_undefined evd evk1 in
+  let env1,rel_sign = env_rel_context_chop k env in
+  let sign1 = evar_hyps evi1 in
+  let filter1 = evar_filter evi1 in
+  let ids1 = List.map pi1 (named_context_of_val sign1) in
+  let inst_in_sign = List.map mkVar (list_filter_with filter1 ids1) in
+  let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
+    List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
+      let id = next_name_away na avoid in
+      let evd,t_in_sign =
+        define_evar_from_virtual_equation define_fun env evd t_in_env
+          sign filter inst_in_env in
+      let evd,b_in_sign = match b with
+      | None -> evd,None
+      | Some b ->
+          let evd,b = define_evar_from_virtual_equation define_fun env evd b
+            sign filter inst_in_env in
+          evd,Some b in
+      (push_named_context_val (id,b_in_sign,t_in_sign) sign,true::filter,
+       (mkRel 1)::(List.map (lift 1) inst_in_env),
+       (mkRel 1)::(List.map (lift 1) inst_in_sign),
+       push_rel d env,evd,id::avoid))
+      rel_sign
+      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
+  in
+  let evd,ev2ty_in_sign =
+    define_evar_from_virtual_equation define_fun env evd ty_in_env
+      sign2 filter2 inst2_in_env in
+  let evd,ev2_in_sign =
+    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
+  let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
+  (evd, ev2_in_sign, ev2_in_env)
+
+let restrict_upon_filter evd evk p args =
+  let newfilter = List.map p args in
+  if List.for_all (fun id -> id) newfilter then
+    None
+  else
+    let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
+    Some (apply_subfilter oldfullfilter newfilter)
+
 (* Inverting constructors in instances (common when inferring type of match) *)
 
 let find_projectable_constructor env evd cstr k args cstr_subst =
@@ -702,13 +960,13 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
  * [make_projectable_subst])
  *)
 
-exception NotUnique
-exception NotUniqueInType of types
-
 type evar_projection =
 | ProjectVar
 | ProjectEvar of existential * evar_info * identifier * evar_projection
 
+exception NotUnique
+exception NotUniqueInType of (identifier * evar_projection) list
+
 let rec assoc_up_to_alias sigma aliases y yc = function
   | [] -> raise Not_found
   | (c,cc,id)::l ->
@@ -828,30 +1086,34 @@ type projectibility_status =
   | CannotInvert
   | Invertible of projectibility_kind
 
-let invert_arg_from_subst aliases k sigma subst_in_env c_in_env_extended_with_k_binders =
+let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
   let effects = ref [] in
   let rec aux k t =
-    let t = whd_evar sigma t in
+    let t = whd_evar evd t in
     match kind_of_term t with
-    | Rel i when i>k ->
-	project_with_effects aliases sigma effects (mkRel (i-k)) subst_in_env
-    | Var id ->
-	project_with_effects aliases sigma effects t subst_in_env
-    | _ ->
-	map_constr_with_binders succ aux k t in
+    | Rel i when i>k0+k -> aux' k (mkRel (i-k))
+    | Var id -> aux' k t
+    | _ -> map_constr_with_binders succ aux k t
+  and aux' k t =
+    try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
+    with Not_found ->
+      match expand_alias_once aliases t with
+      | None -> raise Not_found
+      | Some c -> aux k c in
   try
-    let c = aux k c_in_env_extended_with_k_binders in
+    let c = aux 0 c_in_env_extended_with_k_binders in
     Invertible (UniqueProjection (c,!effects))
   with
     | Not_found -> CannotInvert
     | NotUnique -> Invertible NoUniqueProjection
 
-let invert_arg aliases k sigma evk subst_in_env c_in_env_extended_with_k_binders =
-  let res = invert_arg_from_subst aliases k sigma subst_in_env c_in_env_extended_with_k_binders in
+let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
+  let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
   match res with
-  | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
-  | _ -> res
-
+  | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) ->
+      CannotInvert
+  | _ ->
+      res
 
 let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
@@ -863,12 +1125,34 @@ let instance_of_projection f env t evd projs =
   | UniqueProjection (c,effects) ->
       (List.fold_left (do_projection_effects f env ty) evd effects, c)
 
-let filter_of_projection = function CannotInvert -> false | _ -> true
+exception NotEnoughInformationToInvert
+
+let extract_unique_projections projs =
+  List.map (function
+    | Invertible (UniqueProjection (c,_)) -> c
+    | _ ->
+        (* For instance, there are evars with non-invertible arguments and *)
+        (* we cannot arbitrarily restrict these evars before knowing if there *)
+        (* will really be used; it can also be due to some argument *)
+        (* (typically a rel) that is not inversible and that cannot be *)
+        (* inverted either because it is needed for typing the conclusion *)
+        (* of the evar to project *)
+      raise NotEnoughInformationToInvert) projs
+
+let extract_candidates sols =
+  try
+    Some
+      (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
+  with Exit ->
+    None
+
+let filter_of_projection = function Invertible _ -> true | _ -> false
 
-let filter_along f projs v =
-  let l = Array.to_list v in
-  let _,l = list_filter2 (fun b c -> f b) (projs,l) in
-  Array.of_list l
+let invert_invertible_arg evd aliases k (evk,argsv) args' =
+  let evi = Evd.find_undefined evd evk in
+  let subst,_ = make_projectable_subst aliases evd evi argsv in
+  let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in
+  Array.of_list (extract_unique_projections projs)
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
  * variables) such that c becomes closed.
@@ -883,7 +1167,27 @@ let filter_along f projs v =
  * such that "hyps' |- ?e : T"
  *)
 
-let restrict_hyps ?(refine=false) evd evk filter =
+let filter_candidates evd evk filter candidates =
+  let evi = Evd.find_undefined evd evk in
+  let candidates = match candidates with
+  | None -> evi.evar_candidates
+  | Some _ -> candidates in
+  match candidates,filter with
+  | None,_ | _, None -> candidates
+  | Some l, Some filter ->
+      let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
+      Some (List.filter (fun a ->
+        list_subset (Idset.elements (collect_vars a)) ids) l)
+
+let closure_of_filter evd evk filter =
+  let evi = Evd.find_undefined evd evk in
+  let vars = collect_vars (evar_concl evi) in
+  let ids = List.map pi1 (evar_context evi) in
+  let test id b = b || Idset.mem id vars in
+  let newfilter = List.map2 test ids filter in
+  if newfilter = evar_filter evi then None else Some newfilter
+
+let restrict_hyps evd evk filter candidates =
     (* What to do with dependencies?
        Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
        - If y is in a non-erasable position in C(x,y) (i.e. it is not below an
@@ -894,66 +1198,75 @@ let restrict_hyps ?(refine=false) evd evk filter =
        interest for this early detection in practice is not obvious. We let
        it for future work. In any case, thanks to the use of filters, the whole
        (unrestricted) context remains consistent. *)
-    let evi = Evd.find evd evk in
-    let env = evar_unfiltered_env evi in
-    let oldfilter = evar_filter evi in
-    let filter,_ = List.fold_right (fun oldb (l,filter) ->
-      if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
-      oldfilter ([], List.rev filter) in
-    let filter, ccl = check_restricted_occur evd refine (named_context env) filter evi.evar_concl in
-    (env,evar_source evk evd,filter,ccl)
-
-let do_restrict_hyps evd evk projs =
-  let filter = List.map filter_of_projection projs in
-  if List.for_all (fun x -> x) filter then
-    evd,evk
-  else
-    let env,src,filter,ccl = restrict_hyps evd evk filter in
-      if List.for_all (fun x -> x) filter then
-	evd,evk
-      else
-	let evd,nc = new_evar evd env ~src ~filter ccl in
-	let evd = Evd.define evk nc evd in
-	let evk',_ = destEvar nc in
-	  evd,evk'
-
-(* [postpone_evar_term] postpones an equation of the form ?e[σ] = c *)
-
-let postpone_evar_term env evd (evk,argsv) rhs =
-  assert (isVar rhs or isRel rhs);
+    let candidates = filter_candidates evd evk (Some filter) candidates in
+    let typablefilter = closure_of_filter evd evk filter in
+    (typablefilter,candidates)
+
+exception EvarSolvedWhileRestricting of evar_map * constr
+
+let do_restrict_hyps evd (evk,args as ev) filter candidates =
+  let filter,candidates = match filter with
+  | None -> None,candidates
+  | Some filter -> restrict_hyps evd evk filter candidates in
+  match candidates,filter with
+  | Some [], _ -> error "Not solvable."
+  | Some [nc],_ ->
+      let evd = Evd.define evk nc evd in
+      raise (EvarSolvedWhileRestricting (evd,whd_evar evd (mkEvar ev)))
+  | None, None -> evd,ev
+  | _ -> restrict_applied_evar evd ev filter candidates
+
+(* [postpone_non_unique_projection] postpones equation of the form ?e[?] = c *)
+(* ?e is assumed to have no candidates *)
+
+let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs =
   let rhs = expand_vars_in_term env rhs in
-  let evi = Evd.find evd evk in
-  let evd,evk,args =
-    restrict_upon_filter evd evi evk
-      (* Keep only variables that depends in rhs *)
+  let filter =
+    restrict_upon_filter evd evk
+      (* Keep only variables that occur in rhs *)
       (* This is not safe: is the variable is a local def, its body *)
       (* may contain references to variables that are removed, leading to *)
       (* a ill-formed context. We would actually need a notion of filter *)
       (* that says that the body is hidden. Note that expand_vars_in_term *)
       (* expands only rels and vars aliases, not rels or vars bound to an *)
       (* arbitrary complex term *)
-      (fun a -> not (isRel a || isVar a) || dependent a rhs)
+      (fun a -> not (isRel a || isVar a)
+                || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols)
       (Array.to_list argsv) in
-  let args = Array.of_list args in
-  let pb = (Reduction.CONV,env,mkEvar(evk,args),rhs) in
-  Evd.add_conv_pb pb evd
+  let filter = match filter with
+  | None -> None
+  | Some filter -> closure_of_filter evd evk filter in
+  let candidates = extract_candidates sols in
+  if candidates <> None then
+    restrict_evar evd evk filter candidates
+  else
+    (* We made an approximation by not expanding a local definition *)
+    let evd,ev = restrict_applied_evar evd ev filter None in
+    let pb = (Reduction.CONV,env,mkEvar ev,rhs) in
+    Evd.add_conv_pb pb evd
 
-(* [postpone_evar_evar] postpones an equation of the form ?e1[σ1] = ?e2[σ2] *)
+(* [postpone_evar_evar] postpones an equation of the form ?e1[?1] = ?e2[?2] *)
 
-let postpone_evar_evar env evd projs1 (evk1,args1) projs2 (evk2,args2) =
+let postpone_evar_evar f env evd filter1 ev1 filter2 ev2 =
   (* Leave an equation between (restrictions of) ev1 andv ev2 *)
-  let args1' = filter_along filter_of_projection projs1 args1 in
-  let evd,evk1' = do_restrict_hyps evd evk1 projs1 in
-  let args2' = filter_along filter_of_projection projs2 args2 in
-  let evd,evk2' = do_restrict_hyps evd evk2 projs2 in
-  let pb = (Reduction.CONV,env,mkEvar(evk1',args1'),mkEvar (evk2',args2')) in
-  add_conv_pb pb evd
+  try
+    let evd,ev1' = do_restrict_hyps evd ev1 filter1 None in
+    try
+      let evd,ev2' = do_restrict_hyps evd ev2 filter2 None in
+      add_conv_pb (Reduction.CONV,env,mkEvar ev1',mkEvar ev2') evd
+    with EvarSolvedWhileRestricting (evd,ev2) ->
+      (* ev2 solved on the fly *)
+      f env evd ev1' ev2
+  with EvarSolvedWhileRestricting (evd,ev1) ->
+    (* ev1 solved on the fly *)
+    f env evd ev2 ev1
 
 (* [solve_evar_evar f Γ Σ ?e1[u1..un] ?e2[v1..vp]] applies an heuristic
  * to solve the equation Σ; Γ ⊢ ?e1[u1..un] = ?e2[v1..vp]:
  * - if there are at most one φj for each vj s.t. vj = φj(u1..un),
- *   we first restrict ?2 to the subset v_k1..v_kq of the vj that are
- *   inversible and we set ?1[x1..xn] := ?2[φk1(x1..xn)..φkp(x1..xn)]
+ *   we first restrict ?e2 to the subset v_k1..v_kq of the vj that are
+ *   inversible and we set ?e1[x1..xn] := ?e2[φk1(x1..xn)..φkp(x1..xn)]
+ *   (this is a case of pattern-unification)
  * - symmetrically if there are at most one ψj for each uj s.t.
  *   uj = ψj(v1..vp),
  * - otherwise, each position i s.t. ui does not occur in v1..vp has to
@@ -971,55 +1284,139 @@ let are_canonical_instances args1 args2 env =
   let n2 = Array.length args2 in
   let rec aux n = function
     | (id,_,c)::sign
-	when n < n1 && isVar args1.(n) && destVar args1.(n) = id && eq_constr args1.(n) args2.(n) ->
+	when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
 	aux (n+1) sign
     | [] ->
 	let rec aux2 n =
 	  n = n1 ||
-	  (isRel args1.(n) && destRel args1.(n) = n1-n &&
-	   isRel args2.(n) && destRel args2.(n) = n1-n && aux2 (n+1))
+	  (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
 	in aux2 n
     | _ -> false in
   n1 = n2 & aux 0 (named_context env)
 
-exception CannotProject of projectibility_status list
+let filter_compatible_candidates conv_algo env evd evi args rhs c =
+  let c' = instantiate_evar (evar_filtered_context evi) c args in
+  let evd, b = conv_algo env evd Reduction.CONV rhs c' in
+  if b then Some (c,evd) else None
+
+exception DoesNotPreserveCandidateRestriction
+
+let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
+  let evi1 = Evd.find evd evk1 in
+  let evi2 = Evd.find evd evk2 in
+  let cand1 = filter_candidates evd evk1 filter1 None in
+  let cand2 = evi2.evar_candidates in
+  match cand1, cand2 with
+  | _, None -> cand1
+  | None, Some _ -> raise DoesNotPreserveCandidateRestriction
+  | Some l1, Some l2 ->
+      let args1 = Array.to_list argsv1 in
+      let args2 = Array.to_list argsv2 in
+      let l1' = List.filter (fun c1 ->
+        let c1' = instantiate_evar (evar_filtered_context evi1) c1 args1 in
+        List.filter (fun c2 ->
+          (filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2
+           <> None)) l2 <> []) l1 in
+      if List.length l1 = List.length l1' then None else Some l1'
+
+exception CannotProject of bool list option
+
+(* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U.
+   Can ?n be instantiated by a term u depending essentially on xi such that the
+   FV(u[x1:=t1..xn:=tn]) are in the set U?
+   - If ti is a variable, it has to be in U.
+   - If ti is a constructor, its parameters cannot be erased even if u
+     matches on it, so we have to discard ti if the parameters
+     contain variables not in U.
+   - If ti is rigid, we have to discard it if it contains variables in U.
+
+  Note: when restricting as part of an equation ?n[x1:=t1..xn:=tn] = ?m[...]
+  then, occurrences of ?m in the ti can be seen, like variables, as occurrences
+  of subterms to eventually discard so as to be allowed to keep ti.
+*)
 
-let is_variable_subst args =
-  array_for_all (fun c -> isRel c || isVar c) args
+let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
+  let f,args = decompose_app_vect t in
+  match kind_of_term f with
+  | Construct (ind,_) ->
+      let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+      let params,_ = array_chop nparams args in
+      array_for_all (is_constrainable_in k g) params
+  | Ind _ -> array_for_all (is_constrainable_in k g) args
+  | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
+  | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*)
+  | Var id -> Idset.mem id fv_ids
+  | Rel n -> n <= k || Intset.mem n fv_rels
+  | Sort _ -> true
+  | _ -> (* We don't try to be more clever *) true
+
+let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
+  let t = expansion_of_var aliases t in
+  match kind_of_term t with
+  | Var id -> Idset.mem id fv_ids
+  | Rel n -> n <= k || Intset.mem n fv_rels
+  | _ -> is_constrainable_in k (ev,fvs) t
+
+let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
+  let filter1 =
+    restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1)
+  in
+  let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
+  let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
+  let filter2 =
+    restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2)
+  in
+  let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
+  let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
+  evd,ev1,ev2
+
+exception EvarSolvedOnTheFly of evar_map * constr
+
+let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+  (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
+  let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
+  let filter1 = restrict_upon_filter evd evk1
+    (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
+    (Array.to_list argsv1) in
+  (* Only try pruning on variable substitutions, postpone otherwise. *)
+  (* Rules out non-linear instances. *)
+  if is_unification_pattern_pure_evar env evd ev2 (mkEvar ev1) then
+    try
+      let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
+      let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
+      evd,mkEvar (evk1',invert_invertible_arg evd aliases k2 ev2 args1)
+    with
+    | EvarSolvedWhileRestricting (evd,ev1) ->
+        raise (EvarSolvedOnTheFly (evd,ev1))
+    | DoesNotPreserveCandidateRestriction | NotEnoughInformationToInvert ->
+        raise (CannotProject filter1)
+  else
+    raise (CannotProject filter1)
 
-let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,args2 as ev2) =
-  let aliases = make_alias_map env in
-  let subst,_ = make_projectable_subst aliases evd (Evd.find evd evk2) args2 in
+let solve_evar_evar_l2r f g env evd aliases ev1 (evk2,_ as ev2) =
+  try
+    let evd,body = project_evar_on_evar g env evd aliases 0 ev1 ev2 in
+    Evd.define evk2 body evd
+  with EvarSolvedOnTheFly (evd,c) ->
+    f env evd ev2 c
+
+let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) =
   if are_canonical_instances args1 args2 env then
     (* If instances are canonical, we solve the problem in linear time *)
     let sign = evar_filtered_context (Evd.find evd evk2) in
-    let subst = List.map (fun (id,_,_) -> mkVar id) sign in
-    Evd.define evk2 (mkEvar(evk1,Array.of_list subst)) evd
+    let id_inst = list_map_to_array (fun (id,_,_) -> mkVar id) sign in
+    Evd.define evk2 (mkEvar(evk1,id_inst)) evd
   else
-    (* Only try pruning on variable substitutions, postpone otherwise. *)
-    if is_variable_subst args1 && is_variable_subst args2 then
-      let proj1 = array_map_to_list (invert_arg aliases 0 evd evk2 subst) args1 in
-	try
-	  (* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable.
-	     Rules out non-linear instances. *)
-	  let proj1' = effective_projections proj1 in
-	  let evd,args1' =
-	    list_fold_map (instance_of_projection f env (mkEvar ev2)) evd proj1' in
-	  let evd,evk1' = do_restrict_hyps evd evk1 proj1 in
-	    Evd.define evk2 (mkEvar(evk1',Array.of_list args1')) evd
-	with NotUnique -> raise (CannotProject proj1)
-    else raise IllTypedFilter
-
-let solve_evar_evar f env evd ev1 ev2 =
-  try
-    try solve_evar_evar_l2r f env evd ev1 ev2
-    with CannotProject projs1 ->
-    try solve_evar_evar_l2r f env evd ev2 ev1
-    with CannotProject projs2 ->
-    postpone_evar_evar env evd projs1 ev1 projs2 ev2
-  with IllTypedFilter ->
-    let pb = (Reduction.CONV,env,mkEvar(ev1),mkEvar (ev2)) in
-      add_conv_pb pb evd
+    let evd,ev1,ev2 =
+      (* If an evar occurs in the instance of the other evar and the
+         use of an heuristic is forced, we restrict *)
+      if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in
+    let aliases = make_alias_map env in
+    try solve_evar_evar_l2r f g env evd aliases ev1 ev2
+    with CannotProject filter1 ->
+    try solve_evar_evar_l2r f g env evd aliases ev2 ev1
+    with CannotProject filter2 ->
+    postpone_evar_evar f env evd filter1 ev1 filter2 ev2
 
 type conv_fun =
   env ->  evar_map -> conv_pb -> constr -> constr -> evar_map * bool
@@ -1037,24 +1434,32 @@ let check_evar_instance evd evk1 body conv_algo =
     user_err_loc (fst (evar_source evk1 evd),"",
 		  str "Unable to find a well-typed instantiation")
 
-(* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
- * definitions. We try to unify the xi with the yi pairwise. The pairs
- * that don't unify are discarded (i.e. ?i is redefined so that it does not
+(* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
+ * definitions. We try to unify the ti with the ui pairwise. The pairs
+ * that don't unify are discarded (i.e. ?e is redefined so that it does not
  * depend on these args). *)
 
-let solve_refl conv_algo env evd evk argsv1 argsv2 =
+let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
   if array_equal eq_constr argsv1 argsv2 then evd else
-  let evi = Evd.find_undefined evd evk in
   (* Filter and restrict if needed *)
-  let evd,evk,args =
-    restrict_upon_filter evd evi evk
+  let untypedfilter =
+    restrict_upon_filter evd evk
       (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
       (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
+  let candidates = filter_candidates evd evk untypedfilter None in
+  let filter = match untypedfilter with
+    | None -> None
+    | Some filter -> closure_of_filter evd evk filter in
+  let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
+  if fst ev1 = evk & can_drop then (* No refinement *) evd else
+    (* either progress, or not allowed to drop, e.g. to preserve possibly *)
+    (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
+    (* if e can depend on x until ?y is not resolved, or, conversely, we *)
+    (* don't know if ?y has to be unified with ?y, until e is resolved *)
+  let argsv2 = restrict_instance evd evk filter argsv2 in
+  let ev2 = (fst ev1,argsv2) in
   (* Leave a unification problem *)
-  let args1,args2 = List.split args in
-  let argsv1 = Array.of_list args1 and argsv2 = Array.of_list args2 in
-  let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
-    Evd.add_conv_pb pb evd
+  Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev1,mkEvar ev2) evd
 
 (* If the evar can be instantiated by a finite set of candidates known
    in advance, we check which of them apply *)
@@ -1067,23 +1472,15 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
   match evi.evar_candidates with
   | None -> raise NoCandidates
   | Some l ->
-      let l' = list_map_filter (fun c ->
-        let c' = instantiate_evar (evar_filtered_context evi) c args in
-        let evd, b = conv_algo env evd Reduction.CONV c' rhs in
-        if b then Some (c,evd) else None) l in
+      let l' =
+        list_map_filter
+          (filter_compatible_candidates conv_algo env evd evi args rhs) l in
       match l' with
       | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
       | [c,evd] -> Evd.define evk c evd
       | l when List.length l < List.length l' ->
           let candidates = List.map fst l in
-          let filter = evar_filter evi in
-          let sign = evar_hyps evi in
-          let ids = List.map pi1 (named_context_of_val sign) in
-          let inst_in_sign =
-            List.map mkVar (snd (list_filter2 (fun b id -> b) (filter,ids))) in
-          let evd,evar = new_evar_instance (evar_hyps evi) evd (evar_concl evi)
-            ~filter ~candidates inst_in_sign in
-          Evd.define evk evar evd
+          restrict_evar evd evk None (Some candidates)
       | l -> evd
 
 (* We try to instantiate the evar assuming the body won't depend
@@ -1110,7 +1507,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
  *)
 
 exception NotInvertibleUsingOurAlgorithm of constr
-exception NotEnoughInformationToProgress
+exception NotEnoughInformationToProgress of (identifier * evar_projection) list
 exception OccurCheckIn of evar_map * constr
 
 let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
@@ -1129,8 +1526,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 	| [] -> raise Not_found
 	| [id,p] -> (mkVar id, p)
 	| (id,p)::_::_ ->
-	    if choose then (mkVar id, p)
-	    else raise (NotUniqueInType(find_solution_type (evar_env evi) sols))
+	    if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
       let ty = lazy (Retyping.get_type_of env !evdref t) in
       let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in
@@ -1138,64 +1534,77 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
       c
     with
       | Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
-      | NotUniqueInType ty ->
-	  if not !progress then raise NotEnoughInformationToProgress;
+      | NotUniqueInType sols ->
+	  if not !progress then
+            raise (NotEnoughInformationToProgress sols);
 	  (* No unique projection but still restrict to where it is possible *)
           (* materializing is necessary, but is restricting useful? *)
+          let ty = find_solution_type (evar_env evi) sols in
           let sign = evar_filtered_context evi in
           let ty' = instantiate_evar sign ty (Array.to_list argsv) in
-	  let (evd,_,ev') =
+	  let (evd,evar,(evk',argsv' as ev')) =
             materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
 	  let ts = expansions_of_var aliases t in
 	  let test c = isEvar c or List.mem c ts in
-	  let filter = array_map_to_list test argsv in
-	  let evarenv,src,filter,_ = restrict_hyps ~refine:true evd (fst ev') filter in
-	  let args' = filter_along (fun x -> x) filter argsv in
-	  let evd,evar = new_evar !evdref evarenv ~src ~filter ty in
-	  let evk',_ = destEvar evar in
-	  let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in
-	  evdref := Evd.add_conv_pb pb evd;
+	  let filter = array_map_to_list test argsv' in
+          let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in
+
+          let filter = closure_of_filter evd evk' filter in
+          let candidates = extract_candidates sols in
+          let evd =
+            if candidates <> None then restrict_evar evd evk' filter candidates
+            else
+              let evd,ev'' = restrict_applied_evar evd ev' filter None in
+              Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd in
+          evdref := evd;
 	  evar in
 
   let rec imitate (env',k as envk) t =
     let t = whd_evar !evdref t in
     match kind_of_term t with
-    | Rel i when i>k -> project_variable (mkRel (i-k))
-    | Var id -> project_variable t
+    | Rel i when i>k ->
+        (match pi2 (Environ.lookup_rel (i-k) env') with
+        | None -> project_variable (mkRel (i-k))
+        | Some b ->
+          try project_variable (mkRel (i-k))
+          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b))
+    | Var id ->
+        (match pi2 (Environ.lookup_named id env') with
+        | None -> project_variable t
+        | Some b ->
+          try project_variable t
+          with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
     | Evar (evk',args' as ev') ->
         if evk = evk' then raise (OccurCheckIn (evd,rhs));
 	(* Evar/Evar problem (but left evar is virtual) *)
-	let projs' =
-	  array_map_to_list
-	    (invert_arg_from_subst aliases k !evdref subst) args'
-	in
-	  (try
-	     (* Try to project (a restriction of) the right evar *)
-	     let eprojs' = effective_projections projs' in
-	     let evd,args' =
-	       list_fold_map (instance_of_projection (evar_define conv_algo) env' t)
-	         !evdref eprojs' in
-	     let evd,evk' = do_restrict_hyps evd evk' projs' in
-	       evdref := evd;
-	       mkEvar (evk',Array.of_list args')
-	   with NotUnique | IllTypedFilter ->
-	   assert !progress;
-	   (* Make the virtual left evar real *)
-	   let ty = get_type_of env' !evdref t in
-	   let (evd,evar'',ev'') =
+        let aliases = lift_aliases k aliases in
+        (try
+          let ev = (evk,Array.map (lift k) argsv) in
+          let evd,body = project_evar_on_evar conv_algo env !evdref aliases k ev'  ev in
+	  evdref := evd;
+          body
+        with
+        | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t
+        | CannotProject filter' ->
+	  assert !progress;
+	  (* Make the virtual left evar real *)
+	  let ty = get_type_of env' !evdref t in
+	  let (evd,evar'',ev'') =
              materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
-	     (try
-		let evd =
-		  (* Try to project (a restriction of) the left evar ... *)
-		  try solve_evar_evar_l2r (evar_define conv_algo) env' evd ev'' ev'
-		  with CannotProject projs'' ->
-		    (* ... or postpone the problem *)
-		    postpone_evar_evar env' evd projs'' ev'' projs' ev'
-		in
-	          evdref := evd;
-		  evar''
-	      with IllTypedFilter -> raise (NotInvertibleUsingOurAlgorithm t)))
+	  let evd =
+	     (* Try to project (a restriction of) the left evar ... *)
+	    try
+              let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 ev'' ev' in
+              Evd.define evk' body evd
+	    with
+            | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
+            | CannotProject filter'' ->
+	      (* ... or postpone the problem *)
+	      postpone_evar_evar (evar_define conv_algo) env' evd filter'' ev'' filter' ev' in
+	  evdref := evd;
+	  evar'')
     | _ ->
+        progress := true;
 	match
 	  let c,args = decompose_app_vect t in
 	  match kind_of_term c with
@@ -1205,16 +1614,30 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
             (*  possible inversions; we do not treat overlap with a possible *)
             (*  alternative inversion of the subterms of the constructor, etc)*)
 	    (match find_projectable_constructor env evd cstr k args cstr_subst with
-	     | [id] -> Some (mkVar id)
+	     | _::_ as l -> Some (List.map mkVar l)
 	     | _ -> None)
 	  | _ -> None
 	with
-	| Some c -> c
+	| Some l ->
+            let ty = get_type_of env' !evdref t in
+            let candidates =
+              try
+                let t =
+                  map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
+	            imitate envk t in
+                t::l
+              with _ -> l in
+            (match candidates with
+            | [x] -> x
+            | _ ->
+	      let (evd,evar'',ev'') =
+                materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+              evdref := restrict_evar evd (fst ev'') None (Some candidates);
+              evar'')
 	| None ->
-	  progress := true;
 	  (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-	  map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-	    imitate envk t in
+	    map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
+	      imitate envk t in
 
   let rhs = whd_beta evd rhs (* heuristic *) in
   let body = imitate (env,0) rhs in
@@ -1230,8 +1653,11 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
   match kind_of_term rhs with
   | Evar (evk2,argsv2 as ev2) ->
-      if evk = evk2 then solve_refl conv_algo env evd evk argsv argsv2
-      else solve_evar_evar (evar_define conv_algo) env evd ev ev2
+      if evk = evk2 then
+        solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2
+      else
+        solve_evar_evar ~force:choose
+          (evar_define conv_algo) conv_algo env evd ev ev2
   | _ ->
   try solve_candidates conv_algo env evd ev rhs
   with NoCandidates ->
@@ -1262,8 +1688,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
     let evd' = Evd.define evk body evd' in
     check_evar_instance evd' evk body conv_algo
   with
-    | NotEnoughInformationToProgress ->
-	postpone_evar_term env evd ev rhs
+    | NotEnoughInformationToProgress sols ->
+	postpone_non_unique_projection env evd ev sols rhs
     | NotInvertibleUsingOurAlgorithm t ->
 	error_not_clean env evd evk t (evar_source evk evd)
     | OccurCheckIn (evd,rhs) ->
@@ -1277,173 +1703,6 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
 	| _ ->
 	    error_occur_check env evd evk rhs
 
-(*-------------------*)
-(* Auxiliary functions for the conversion algorithms modulo evars
- *)
-
-let has_undefined_evars_or_sorts evd t =
-  let rec has_ev t =
-    match kind_of_term t with
-    | Evar (ev,args) ->
-        (match evar_body (Evd.find evd ev) with
-        | Evar_defined c ->
-            has_ev c; Array.iter has_ev args
-        | Evar_empty ->
-	    raise NotInstantiatedEvar)
-    | Sort s when is_sort_variable evd s -> raise Not_found
-    | _ -> iter_constr has_ev t in
-  try let _ = has_ev t in false
-  with (Not_found | NotInstantiatedEvar) -> true
-
-let is_ground_term evd t =
-  not (has_undefined_evars_or_sorts evd t)
-
-let is_ground_env evd env =
-  let is_ground_decl = function
-      (_,Some b,_) -> is_ground_term evd b
-    | _ -> true in
-  List.for_all is_ground_decl (rel_context env) &&
-  List.for_all is_ground_decl (named_context env)
-(* Memoization is safe since evar_map and environ are applicative
-   structures *)
-let is_ground_env = memo1_2 is_ground_env
-
-(* Return the head evar if any *)
-
-exception NoHeadEvar
-
-let head_evar =
-  let rec hrec c = match kind_of_term c with
-    | Evar (evk,_)   -> evk
-    | Case (_,_,c,_) -> hrec c
-    | App (c,_)      -> hrec c
-    | Cast (c,_,_)   -> hrec c
-    | _              -> raise NoHeadEvar
-  in
-  hrec
-
-(* Expand head evar if any (currently consider only applications but I
-   guess it should consider Case too) *)
-
-let whd_head_evar_stack sigma c =
-  let rec whrec (c, l as s) =
-    match kind_of_term c with
-      | Evar (evk,args as ev) when Evd.is_defined sigma evk
-	  -> whrec (existential_value sigma ev, l)
-      | Cast (c,_,_) -> whrec (c, l)
-      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
-      | _ -> s
-  in
-  whrec (c, [])
-
-let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
-
-let rec expand_and_check_vars aliases = function
-  | [] -> []
-  | a::l when isRel a or isVar a ->
-      let a = expansion_of_var aliases a in
-      if isRel a or isVar a then a :: expand_and_check_vars aliases l
-      else raise Exit
-  | _ ->
-      raise Exit
-
-module Constrhash = Hashtbl.Make
-  (struct type t = constr
-	  let equal = eq_constr
-	  let hash = hash_constr
-   end)
-
-let rec constr_list_distinct l =
-  let visited = Constrhash.create 23 in
-  let rec loop = function
-    | h::t ->
-	if Constrhash.mem visited h then false
-	else (Constrhash.add visited h h; loop t)
-    | [] -> true
-  in loop l
-
-let get_actual_deps aliases l t =
-  if occur_meta_or_existential t then
-    (* Probably no restrictions on allowed vars in presence of evars *)
-    l
-  else
-    (* Probably strong restrictions coming from t being evar-closed *)
-    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
-    List.filter (fun c ->
-      match kind_of_term c with
-      | Var id -> Idset.mem id fv_ids
-      | Rel n -> Intset.mem n fv_rels
-      | _ -> assert false) l
-
-let remove_instance_local_defs evd evk args =
-  let evi = Evd.find evd evk in
-  let rec aux = function
-  | (_,Some _,_)::sign, a::args -> aux (sign,args)
-  | (_,None,_)::sign, a::args -> a::aux (sign,args)
-  | [], [] -> []
-  | _ -> assert false in
-  aux (evar_filtered_context evi, args)
-
-(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
-
-let find_unification_pattern_args env l t =
-  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
-    let aliases = make_alias_map env in
-    match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
-    | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
-    | _ -> None
-  else
-    None
-
-let is_unification_pattern_meta env nb m l t =
-  (* Variables from context and rels > nb are implicitly all there *)
-  (* so we need to be a rel <= nb *)
-  if List.for_all (fun x -> isRel x && destRel x <= nb) l then
-    match find_unification_pattern_args env l t with
-    | Some _ as x when not (dependent (mkMeta m) t) -> x
-    | _ -> None
-  else
-    None
-
-let is_unification_pattern_evar env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
-    let args = remove_instance_local_defs evd evk (Array.to_list args) in
-    let n = List.length args in
-    match find_unification_pattern_args env (args @ l) t with
-    | Some l when not (occur_evar evk t) -> Some (list_skipn n l)
-    | _ -> None
-  else
-    None
-
-let is_unification_pattern (env,nb) evd f l t =
-  match kind_of_term f with
-  | Meta m -> is_unification_pattern_meta env nb m l t
-  | Evar ev -> is_unification_pattern_evar env evd ev l t
-  | _ -> None
-
-(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
-   (pattern unification). It is assumed that l is made of rel's that
-   are distinct and not bound to aliases. *)
-(* It is also assumed that c does not contain metas because metas
-   *implicitly* depend on Vars but lambda abstraction will not reflect this
-   dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
-   return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
-let solve_pattern_eqn env l c =
-  let c' = List.fold_right (fun a c ->
-    let c' = subst_term (lift 1 a) (lift 1 c) in
-    match kind_of_term a with
-      (* Rem: if [a] links to a let-in, do as if it were an assumption *)
-      | Rel n ->
-          let d = map_rel_declaration (lift n) (lookup_rel n env) in
-          mkLambda_or_LetIn d c'
-      | Var id ->
-          let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
-      | _ -> assert false)
-    l c in
-  (* Warning: we may miss some opportunity to eta-reduce more since c'
-     is not in normal form *)
-  whd_eta c'
-
 (* This code (i.e. solve_pb, etc.) takes a unification
  * problem, and tries to solve it. If it solves it, then it removes
  * all the conversion problems, and re-runs conversion on each one, in
@@ -1624,7 +1883,9 @@ let check_evars env initial_sigma sigma c =
 
 open Glob_term
 
+(****************************************)
 (* Operations on value/type constraints *)
+(****************************************)
 
 type type_constraint_type = (int * int) option * constr
 type type_constraint = type_constraint_type option
@@ -1664,10 +1925,6 @@ let empty_valcon = None
 let mk_valcon c = Some c
 
 
-let new_type_evar ?src ?filter evd env =
-  let evd', s = new_sort_variable evd in
-    new_evar evd' env ?src ?filter (mkSort s)
-
 let idx = id_of_string "x"
 
 (* Refining an evar to a product *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 61f503c7..d3f6845c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -84,8 +84,12 @@ val whd_head_evar :  evar_map -> constr -> constr
 
 val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
-val solve_refl : conv_fun -> env ->  evar_map -> 
+val solve_refl : ?can_drop:bool -> conv_fun -> env ->  evar_map ->
   existential_key -> constr array -> constr array -> evar_map
+val solve_evar_evar : ?force:bool ->
+  (env -> evar_map -> existential -> constr -> evar_map) -> conv_fun ->
+  env ->  evar_map -> existential -> existential -> evar_map
+
 val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
   bool option * existential * constr -> evar_map * bool
 val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5d6ca2ca..3cfad524 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -778,10 +778,18 @@ let pr_evar_info evi =
       | Evar_empty -> mt ()
       | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
   in
+  let candidates =
+    match evi.evar_body, evi.evar_candidates with
+      | Evar_empty, Some l ->
+           spc () ++ str "{" ++
+           prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
+      | _ ->
+          mt ()
+  in
   let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
   hov 2
     (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]" ++
-       spc() ++ src)
+       candidates ++ spc() ++ src)
 
 let compute_evar_dependency_graph (sigma:evar_map) =
   (* Compute the map binding ev to the evars whose body depends on ev *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 55c54f2c..194880e2 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -147,6 +147,8 @@ val is_empty : evar_map -> bool
     there are uninstantiated evars in [sigma]. *)
 val has_undefined : evar_map -> bool
 
+(** [add sigma ev info] adds [ev] with evar info [info] in sigma.
+    Precondition: ev must not preexist in [sigma]. *)
 val add : evar_map -> evar -> evar_info -> evar_map
 
 val find : evar_map -> evar -> evar_info
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 15fd226f..0b59fc40 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -392,21 +392,6 @@ let arity_of_case_predicate env (ind,params) dep k =
 (* Inferring the sort of parameters of a polymorphic inductive type
    knowing the sort of the conclusion *)
 
-(* Check if u (sort of a parameter) appears in the sort of the
-   inductive (is). This is done by trying to enforce u > u' >= is
-   in the empty univ graph. If an inconsistency appears, then
-   is depends on u. *)
-let is_constrained is u =
-  try
-    let u' = fresh_local_univ() in
-    let _ =
-      merge_constraints
-        (enforce_geq u (super u')
-          (enforce_geq u' is empty_constraint))
-        initial_universes in
-    false
-  with UniverseInconsistency _ -> true
-
 (* Compute the inductive argument types: replace the sorts
    that appear in the type of the inductive by the sort of the
    conclusion, and the other ones by fresh universes. *)
@@ -418,7 +403,9 @@ let rec instantiate_universes env scl is = function
   | (na,None,ty)::sign, Some u::exp ->
       let ctx,_ = Reduction.dest_arity env ty in
       let s =
-        if is_constrained is u then
+	(* Does the sort of parameter [u] appear in (or equal)
+           the sort of inductive [is] ? *)
+        if univ_depends u is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstriained sort: replace by fresh universe *)
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 2ad2f351..23af7a63 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -53,7 +53,7 @@ let is_global id =
 let is_constructor id =
   try
     match locate (qualid_of_ident id) with
-      | ConstructRef _ as ref -> not (is_imported_ref ref)
+      | ConstructRef _ -> true
       | _ -> false
   with Not_found ->
     false
@@ -232,22 +232,27 @@ let make_all_name_different env =
    looks for name of same base with lower available subscript beyond current
    subscript *)
 
-let visibly_occur_id id c =
-  let rec occur c = match kind_of_term c with
+let occur_rel p env id =
+  try lookup_name_of_rel p env = Name id
+  with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+  let rec occur n c = match kind_of_term c with
     | Const _ | Ind _ | Construct _ | Var _
 	  when shortest_qualid_of_global Idset.empty (global_of_constr c)
 	    = qualid_of_ident id -> raise Occur
-    | _ -> iter_constr occur c
+    | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
+    | _ -> iter_constr_with_binders succ occur n c
   in
-  try occur c; false
+  try occur 1 c; false
   with Occur -> true
     | Not_found -> false (* Happens when a global is not in the env *)
 
-let next_ident_away_for_default_printing t id avoid =
-  let bad id = List.mem id avoid or visibly_occur_id id t in
+let next_ident_away_for_default_printing env_t id avoid =
+  let bad id = List.mem id avoid or visibly_occur_id id env_t in
   next_ident_away_from id bad
 
-let next_name_away_for_default_printing t na avoid =
+let next_name_away_for_default_printing env_t na avoid =
   let id = match na with
   | Name id   -> id
   | Anonymous ->
@@ -255,7 +260,7 @@ let next_name_away_for_default_printing t na avoid =
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
       id_of_string "H" in
-  next_ident_away_for_default_printing t id avoid
+  next_ident_away_for_default_printing env_t id avoid
 
 (**********************************************************************)
 (* Displaying terms avoiding bound variables clashes *)
@@ -278,13 +283,13 @@ let next_name_away_for_default_printing t na avoid =
 type renaming_flags =
   | RenamingForCasesPattern
   | RenamingForGoal
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 let next_name_for_display flags =
   match flags with
   | RenamingForCasesPattern -> next_name_away_in_cases_pattern
   | RenamingForGoal -> next_name_away_in_goal
-  | RenamingElsewhereFor t -> next_name_away_for_default_printing t
+  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
 let compute_displayed_name_in flags avoid na c =
@@ -306,16 +311,20 @@ let compute_displayed_let_name_in flags avoid na c =
   let fresh_id = next_name_for_display flags na avoid in
   (Name fresh_id, fresh_id::avoid)
 
-let rec rename_bound_vars_as_displayed avoid c =
-  let rec rename avoid c =
+let rec rename_bound_vars_as_displayed avoid env c =
+  let rec rename avoid env c =
     match kind_of_term c with
     | Prod (na,c1,c2)  ->
-	let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkProd (na', c1, rename avoid' c2)
+	let na',avoid' =
+          compute_displayed_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkProd (na', c1, rename avoid' (add_name na' env) c2)
     | LetIn (na,c1,t,c2) ->
-	let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkLetIn (na',c1,t, rename avoid' c2)
-    | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+	let na',avoid' =
+          compute_displayed_let_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+    | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
     | _ -> c
   in
-  rename avoid c
+  rename avoid env c
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 637cbf64..6ca03146 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -70,7 +70,7 @@ val set_reserved_typed_name : (types -> name) -> unit
 type renaming_flags =
   | RenamingForCasesPattern (** avoid only global constructors *)
   | RenamingForGoal (** avoid all globals (as in intro) *)
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 val make_all_name_different : env -> env
 
@@ -80,4 +80,5 @@ val compute_and_force_displayed_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
 val compute_displayed_let_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
-val rename_bound_vars_as_displayed : identifier list -> types -> types
+val rename_bound_vars_as_displayed :
+  identifier list -> name list -> types -> types
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 901936f3..d0c9df51 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -104,7 +104,7 @@ let interp_elimination_sort = function
 
 let resolve_evars env evdref fail_evar resolve_classes =
   if resolve_classes then
-    evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
+    evdref := (Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals
 		 ~split:true ~fail:fail_evar env !evdref);
   (* Resolve eagerly, potentially making wrong choices *)
   evdref := (try consider_remaining_unif_problems
@@ -160,13 +160,14 @@ sig
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
+     resolve_classes : launch typeclass resolution after typechecking.
      expand_evars : expand inferred evars by their value if any
      sigma : initial set of existential variables (typically dependent subgoals)
      ltac_env : partial substitution of variables (used for the tactic language)
      constraint : tell if interpreted as a possibly constrained term or a type
   *)
 
-  val understand_ltac :
+  val understand_ltac : ?resolve_classes:bool ->
     bool -> evar_map -> env -> ltac_var_map ->
     typing_constraint -> glob_constr -> pure_open_constr
 
@@ -762,8 +763,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_type sigma env c =
     snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
 
-  let understand_ltac expand_evar sigma env lvar kind c =
-    ise_pretype_gen expand_evar false false sigma env lvar kind c
+  let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c =
+    ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c
 
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
     ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 47b3ec87..b79e9489 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -58,13 +58,14 @@ sig
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
+     resolve_classes : launch typeclass resolution after typechecking.
      expand_evars : expand inferred evars by their value if any
      sigma : initial set of existential variables (typically dependent subgoals)
      ltac_env : partial substitution of variables (used for the tactic language)
      constraint : tell if interpreted as a possibly constrained term or a type
   *)
 
-  val understand_ltac :
+  val understand_ltac : ?resolve_classes:bool ->
     bool -> evar_map -> env -> ltac_var_map ->
     typing_constraint -> glob_constr -> pure_open_constr
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index fc35e2d3..6a26027c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -576,7 +576,6 @@ let inSimplBehaviour = declare_object { (default_object "SIMPLBEHAVIOUR") with
 
 let set_simpl_behaviour local r (recargs, nargs, flags as req) =
   let nargs = if List.mem `SimplNeverUnfold flags then max_int else nargs in
-  let nargs = List.fold_left max nargs recargs in
   let behaviour = {
     b_nargs = nargs; b_recargs = recargs;
     b_dont_expose_case = List.mem `SimplDontExposeCase flags } in
@@ -610,10 +609,11 @@ let dont_expose_case r =
 
 let rec red_elim_const env sigma ref largs =
   let nargs = stack_args_size largs in
-  let largs, unfold_anyway =
+  let largs, unfold_anyway, unfold_nonelim =
     match recargs ref with
-    | None -> largs, false
+    | None -> largs, false, false
     | Some (_,n) when nargs < n -> raise Redelimination
+    | Some (x::l,_) when nargs <= List.fold_left max x l -> raise Redelimination
     | Some (l,n) ->
         List.fold_left (fun stack i ->
           let arg = stack_nth stack i in
@@ -621,7 +621,8 @@ let rec red_elim_const env sigma ref largs =
           match kind_of_term (fst rarg) with
           | Construct _ -> stack_assign stack i (app_stack rarg)
           | _ -> raise Redelimination)
-        largs l, n >= 0 && l = [] && nargs >= n in
+        largs l, n >= 0 && l =  [] && nargs >= n, 
+                 n >= 0 && l <> [] && nargs >= n in
   try match reference_eval sigma env ref with
     | EliminationCases n when nargs >= n ->
 	let c = reference_value sigma env ref in
@@ -651,6 +652,9 @@ let rec red_elim_const env sigma ref largs =
 	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
 	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
+    | NotAnElimination when unfold_nonelim -> 
+         let c = reference_value sigma env ref in
+         whd_betaiotazeta sigma (app_stack (c, largs)), empty_stack
     | _ -> raise Redelimination
     with Redelimination when unfold_anyway ->
        let c = reference_value sigma env ref in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e85f174e..4471e68d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -450,12 +450,6 @@ let is_instance = function
       is_class (IndRef ind)
   | _ -> false
 
-let is_implicit_arg k =
-  match k with
-      ImplicitArg (ref, (n, id), b) -> true
-    | InternalHole -> true
-    | _ -> false
-
 
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to
@@ -473,26 +467,36 @@ let is_resolvable evi =
   assert (evi.evar_body = Evar_empty);
   Option.default true (resolvable.get evi.evar_extra)
 
-let mark_unresolvable_undef evi =
-  let t = resolvable.set false evi.evar_extra in
+let mark_resolvability_undef b evi =
+  let t = resolvable.set b evi.evar_extra in
   { evi with evar_extra = t }
 
-let mark_unresolvable evi =
+let mark_resolvability b evi =
   assert (evi.evar_body = Evar_empty);
-  mark_unresolvable_undef evi
+  mark_resolvability_undef b evi
+
+let mark_unresolvable evi = mark_resolvability false evi
+let mark_resolvable evi = mark_resolvability true evi
 
-let mark_unresolvables sigma =
+let mark_resolvability b sigma =
   Evd.fold_undefined (fun ev evi evs ->
-    Evd.add evs ev (mark_unresolvable_undef evi))
+    Evd.add evs ev (mark_resolvability_undef b evi))
     sigma (Evd.defined_evars sigma)
 
+let mark_unresolvables sigma = mark_resolvability false sigma
+
 let has_typeclasses evd =
   Evd.fold_undefined (fun ev evi has -> has ||
-    (is_class_evar evd evi && is_resolvable evi))
+    (is_resolvable evi && is_class_evar evd evi))
     evd false
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 
-let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
+type evar_filter = hole_kind -> bool
+
+let no_goals = function GoalEvar -> false | _ -> true
+let all_evars _ = true
+
+let resolve_typeclasses ?(filter=no_goals) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses evd) then evd
-  else !solve_instanciations_problem env evd onlyargs split fail
+  else !solve_instanciations_problem env evd filter split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 74ccaf83..4e6081e2 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -71,8 +71,6 @@ val instance_impl : instance -> global_reference
 val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
 
-val is_implicit_arg : hole_kind -> bool
-
 (** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 
@@ -83,10 +81,16 @@ val instance_constructor : typeclass -> constr list -> constr option * types
 
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
+val mark_resolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
-val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
+(** Filter which evars to consider for resolution. *)
+type evar_filter = hole_kind -> bool
+val no_goals : evar_filter
+val all_evars : evar_filter
+
+val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
@@ -101,7 +105,7 @@ val register_remove_instance_hint : (global_reference -> unit) -> unit
 val add_instance_hint : constr -> bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
 
-val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
+val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
 val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
 
 val declare_instance : int option -> bool -> global_reference -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e6fa6eec..eaa83146 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -966,7 +966,7 @@ let check_types env flags (sigma,_,_ as subst) m n =
 
 let try_resolve_typeclasses env evd flags m n =
   if flags.resolve_evars then
-    try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
+    try Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false
 	  ~fail:true env evd
     with e when Typeclasses_errors.unsatisfiable_exception e ->
       error_cannot_unify env evd (m, n)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index fad2e6f0..ac3df714 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -109,7 +109,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
     let typi = type_constructor mind mib cty params in
-    let decl,indapp = Term.decompose_prod typi in
+    let decl,indapp = decompose_prod_assum typi in
     let ind,cargs = find_rectype_a env indapp in
     let nparams = Array.length params in
     let carity = snd (rtbl.(i)) in
@@ -193,11 +193,8 @@ and nf_stk env c t stk  =
       let bsw = branch_of_switch (nb_rel env) sw in
       let mkbranch i (n,v) =
 	let decl,codom = btypes.(i) in
-	let env =
-	  List.fold_right
-	    (fun (name,t) env -> push_rel (name,None,t) env) decl env in
-	let b = nf_val env v codom in
-	compose_lam decl b
+	let b = nf_val (push_rel_context decl env) v codom in
+	it_mkLambda_or_LetIn b decl
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type dep p realargs c in