This commit introduces changes in induction and destruct.

The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
  the "at" is given, of whether the subterm is fully applied or not,
  and whether there are incompatible subterms matching the pattern. In
  particular, we have:
  "at" given
  | subterm fully applied
  | | incompatible subterms
  | | |
  Y Y - it works like in 8.4
  Y N - this was broken in 8.4 ("at" was ineffective and it was finding
        all subterms syntactically equal to the first one which matches)
  N Y Y it now finds all subterms like the first one which matches
        while in 8.4 it used to fail (I hope it is not a too risky in-draft
        for a semantics we would regret...) (e.g. "destruct (S _)" on
        goal "S x = S y + S x" now selects the two occurrences of "S x"
        while it was failing before)
  N Y N it works like in 8.4
  N N - it works like in 8.4, selecting all subterms like the
        first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
  select all subterms that syntactically match the first subterm to
  match the pattern (looking from left to right) is now internally called
  "like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
  for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
  finding the subterm: it could be easily replaced by an other
  matching algorithm.

In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".

Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
  time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
  holes in c, we need the sigma obtained from c to be an extension of
  the sigma of the tactics, while before, we just type-checked c
  independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
  pending conversion problems) is made slightly cleaner: it now takes
  three states: a term is evaluated in state sigma, leading to state
  sigma' >= sigma, with evars finally solved in state sigma'' >=
  sigma'; we solve evars in the diff of sigma' and sigma and report
  the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
  when "c" has unresolved holes, waiting instead for a decision on
  what to do in the case of a similar eapply (see mail to coqdev).

An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.

Incidentally, make_abstraction does not do evar resolution itself any longer.

13 files changed, 253 insertions, 106 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 93d47d6b1..9022db79f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1600,6 +1600,11 @@ let dependent_evar_ident ev evd =
   | _ -> anomaly (str "Not an evar resulting of a dependent binding")
 
 (*******************************************************************)
+
+type pending = (* before: *) evar_map * (* after: *) evar_map
+
+type pending_constr = pending * constr
+
 type open_constr = evar_map * constr
 
 (*******************************************************************)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cc64b3594..8acf81175 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -575,10 +575,16 @@ val eq_constr_univs_test : evar_map -> constr -> constr -> bool
 (** Syntactic equality up to universes, throwing away the (consistent) constraints
     in case of success. *)
 
-(********************************************************************
-   constr with holes *)
+(********************************************************************)
+(* constr with holes and pending resolution of classes, conversion  *)
+(* problems, candidates, etc.                                       *)
+
+type pending = (* before: *) evar_map * (* after: *) evar_map
+
+type pending_constr = pending * constr
+
+type open_constr = evar_map * constr (* Special case when before is empty *)
 
-type open_constr = evar_map * constr
 (** Partially constructed constrs. *)
 
 type unsolvability_explanation = SeveralInstancesFound of int
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index d8698a165..2ffbee4d0 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -50,8 +50,7 @@ let check_used_occurrences nbocc (nowhere_except_in,locs) =
 let proceed_with_occurrences f occs x =
   match occs with
   | NoOccurrences -> x
-  | _ ->
-    (* TODO FINISH ADAPTING WITH HUGO *)
+  | occs ->
     let plocs = Locusops.convert_occs occs in
     assert (List.for_all (fun x -> x >= 0) (snd plocs));
     let (nbocc,x) = f 1 x in
@@ -85,7 +84,7 @@ type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
-  mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option
+  mutable last_found : position_reporting option
 }
 
 (* Find subterms using a testing function, but only at a list of
@@ -93,7 +92,76 @@ type 'a testing_function = {
    (b,l), b=true means no occurrence except the ones in l and b=false,
    means all occurrences except the ones in l *)
 
-let replace_term_occ_gen_modulo occs test bywhat cl occ t =
+(*
+type 'a loc_state = {
+  hyp_location : (Id.t * hyp_location_flag) option;
+  maxocc : bool * int;
+  locs : occurrences;
+  current : int;
+  like_first : bool
+}
+
+let all_found pos =
+  let nowhere_except_in, maxocc = pos.maxocc in
+  nowhere_except_in && pos.current > maxocc
+
+let is_selected pos = Locusops.is_selected pos.current pos.locs
+
+let incr pos = pos := { !pos with current = (!pos).current + 1 }
+
+let make_current_pos cl pos = function
+  | AtOccs occs ->
+    let nowhere_except_in,locs = Locusops.convert_occs occs in
+    let maxocc = List.fold_right max locs 0 in
+    { hyp_location = cl;
+      maxocc = (nowhere_except_in,maxocc);
+      locs = occs;
+      current = pos;
+      like_first = false }
+  | LikeFirst ->
+    { hyp_location = None;
+      maxocc = (false,max_int);
+      locs = AllOccurrences;
+      current = pos;
+      like_first = true }
+
+let extract pos = (pos.hyp_location,pos.current)
+
+let like_first pos = pos.like_first
+
+let replace_term_occ_gen_modulo occs test bywhat cl pos t =
+  let nested = ref false in
+  let currentpos = ref (make_current_pos cl pos occs) in
+  let add_subst t subst =
+    try
+      test.testing_state <- test.merge_fun subst test.testing_state;
+      test.last_found <- Some (extract !currentpos,t)
+    with NotUnifiable e when not (like_first !currentpos) ->
+      let lastpos = Option.get test.last_found in
+     raise
+       (SubtermUnificationError (!nested,(extract !currentpos,t),lastpos,e)) in
+  let rec substrec k t =
+    if all_found !currentpos then (* shortcut *) t else
+    try
+      let subst = test.match_fun test.testing_state t in
+      if is_selected !currentpos then
+        (add_subst t subst; incr currentpos;
+         (* Check nested matching subterms *)
+         nested := true; ignore (subst_below k t); nested := false;
+         (* Do the effective substitution *)
+         Vars.lift k (bywhat ()))
+      else
+        (incr currentpos; subst_below k t)
+    with NotUnifiable _ ->
+      subst_below k t
+  and subst_below k t =
+    map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
+  in
+  let t' = substrec 0 t in
+  (!currentpos, t')
+*)
+
+let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
@@ -101,10 +169,10 @@ let replace_term_occ_gen_modulo occs test bywhat cl occ t =
   let add_subst t subst =
     try
       test.testing_state <- test.merge_fun subst test.testing_state;
-      test.last_found <- Some (cl,!pos,t)
-    with NotUnifiable e ->
+      test.last_found <- Some ((cl,!pos),t)
+    with NotUnifiable e when not like_first ->
       let lastpos = Option.get test.last_found in
-     raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos,e)) in
+     raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
   let rec substrec k t =
     if nowhere_except_in && !pos > maxocc then t else
     if not (Vars.closed0 t) then subst_below k t else
@@ -127,13 +195,17 @@ let replace_term_occ_gen_modulo occs test bywhat cl occ t =
   (!pos, t')
 
 let replace_term_occ_modulo occs test bywhat t =
+  let occs',like_first =
+    match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
   proceed_with_occurrences
-    (replace_term_occ_gen_modulo occs test bywhat None) occs t
+    (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t
 
-let replace_term_occ_decl_modulo (plocs,hyploc) test bywhat d =
+let replace_term_occ_decl_modulo occs test bywhat d =
+  let (plocs,hyploc),like_first =
+    match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (replace_term_occ_gen_modulo plocs test bywhat)
+       (replace_term_occ_gen_modulo plocs like_first test bywhat)
        hyploc)
     plocs d
 
@@ -157,11 +229,13 @@ let subst_closed_term_occ env evd occs c t =
   let t' = replace_term_occ_modulo occs test bywhat t in
     t', test.testing_state
 
-let subst_closed_term_occ_decl env evd (plocs,hyploc) c d =
+let subst_closed_term_occ_decl env evd occs c d =
   let test = make_eq_univs_test env evd c in
+  let (plocs,hyploc),like_first =
+    match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   let bywhat () = mkRel 1 in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun _ -> replace_term_occ_gen_modulo plocs test bywhat None)
+       (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None)
        hyploc) plocs d,
   test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index b24c95807..ea1ce6228 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -26,11 +26,12 @@ exception SubtermUnificationError of subterm_unification_error
     function to merge substitutions and an initial substitution;
     last_found is used for error messages and it has to be initialized
     with None. *)
+
 type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
-  mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option
+  mutable last_found : position_reporting option
 }
 
 (** This is the basic testing function, looking for exact matches of a
@@ -42,25 +43,26 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
     matching subterms at the indicated occurrences [occl] with [mk
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
-val replace_term_occ_modulo :
-  occurrences -> 'a testing_function -> (unit -> constr) -> constr -> constr
+val replace_term_occ_modulo : occurrences or_like_first ->
+  'a testing_function -> (unit -> constr) -> constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
-  occurrences * hyp_location_flag -> 'a testing_function -> (unit -> constr) ->
+  (occurrences * hyp_location_flag) or_like_first ->
+  'a testing_function -> (unit -> constr) ->
   named_declaration -> named_declaration
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
     unifying universes which results in a set of constraints. *)
-val subst_closed_term_occ : env -> evar_map -> occurrences -> constr -> 
-  constr -> constr * evar_map
+val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
+  constr -> constr -> constr * evar_map
 
 (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of 
     closed [c] at positions [occl] by [Rel 1] in [decl]. *)
 val subst_closed_term_occ_decl : env -> evar_map ->
-  occurrences * hyp_location_flag ->
+  (occurrences * hyp_location_flag) or_like_first ->
   constr -> named_declaration -> named_declaration * evar_map
 
 (** Miscellaneous *)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 5484c8095..21157d9d5 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -87,17 +87,22 @@ let out_arg = function
   | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable")
   | Misctypes.ArgArg x -> x
 
-let occurrences_of_hyp id cls =
+let occurrences_of_hyp id =function
+  | LikeFirst -> LikeFirst
+  | AtOccs cls ->
   let rec hyp_occ = function
       [] -> NoOccurrences, InHyp
     | ((occs,id'),hl)::_ when Names.Id.equal id id' ->
         occurrences_map (List.map out_arg) occs, hl
     | _::l -> hyp_occ l in
-  match cls.onhyps with
+  AtOccs (match cls.onhyps with
       None -> AllOccurrences,InHyp
-    | Some l -> hyp_occ l
+    | Some l -> hyp_occ l)
 
-let occurrences_of_goal cls =
-  occurrences_map (List.map out_arg) cls.concl_occs
+let occurrences_of_goal = function
+  | LikeFirst -> LikeFirst
+  | AtOccs cls -> AtOccs (occurrences_map (List.map out_arg) cls.concl_occs)
 
-let in_every_hyp cls = Option.is_empty cls.onhyps
+let in_every_hyp = function
+  | LikeFirst -> true
+  | AtOccs cls -> Option.is_empty cls.onhyps
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 73d13c0bc..f6d27a185 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -38,7 +38,7 @@ val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause
 
 (** Miscellaneous functions *)
 
-val occurrences_of_hyp : Id.t -> Id.t clause_expr ->
-  occurrences * hyp_location_flag
-val occurrences_of_goal : 'a clause_expr -> occurrences
-val in_every_hyp : 'a clause_expr -> bool
+val occurrences_of_hyp : Id.t -> clause or_like_first ->
+  (occurrences * hyp_location_flag) or_like_first
+val occurrences_of_goal : clause or_like_first -> occurrences or_like_first
+val in_every_hyp : clause or_like_first -> bool
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index e16d1206a..99b5a51f9 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -23,9 +23,11 @@ type unification_error =
   | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
 
-type position =(Id.t * Locus.hyp_location_flag) option
+type position = (Id.t * Locus.hyp_location_flag) option
 
-type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option
+type position_reporting = (position * int) * constr
+
+type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
 
 type pretype_error =
   (* Old Case *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index b74ca1936..5882d8b9c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,9 +24,11 @@ type unification_error =
   | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
 
-type position =(Id.t * Locus.hyp_location_flag) option
+type position = (Id.t * Locus.hyp_location_flag) option
 
-type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option
+type position_reporting = (position * int) * constr
+
+type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
 
 type pretype_error =
   (** Old Case *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5383101b4..6dbf7915b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -142,19 +142,27 @@ type inference_flags = {
   expand_evars : bool
 }
 
-let apply_typeclasses env evdref fail_evar =
+let fold_pending_holes f (sigma,sigma') =
+  Evd.fold_undefined
+    (fun evk _ acc -> if Evd.mem sigma evk then acc else f evk acc)
+    sigma'
+
+let is_pending_hole (sigma,sigma') evk =
+  Evd.is_undefined sigma' evk && not (Evd.mem sigma evk)
+
+let apply_typeclasses env evdref pending fail_evar =
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
-	      then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals)
+	      then (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals_or_obligations evk evi)
+              else (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals evk evi))
      ~split:true ~fail:fail_evar env !evdref;
   if Flags.is_program_mode () then (* Try optionally solving the obligations *)
     evdref := Typeclasses.resolve_typeclasses
-      ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref
+      ~filter:(fun evk evi -> is_pending_hole pending evk && Typeclasses.all_evars evk evi) ~split:true ~fail:false env !evdref
 
-let apply_inference_hook hook initial_sigma evdref =
-  evdref := fold_undefined (fun evk evi sigma ->
-    if not (Evd.mem initial_sigma evk) &&
-      is_undefined sigma evk (* i.e. not defined by side-effect *)
+let apply_inference_hook hook evdref pending =
+  evdref := fold_pending_holes (fun evk sigma ->
+    if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
       try
         let c = hook sigma evk in
@@ -162,7 +170,7 @@ let apply_inference_hook hook initial_sigma evdref =
       with Exit ->
         sigma
     else
-      sigma) !evdref !evdref
+      sigma) pending !evdref
 
 let apply_heuristics env evdref fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
@@ -171,39 +179,39 @@ let apply_heuristics env evdref fail_evar =
   with e when Errors.noncritical e ->
     let e = Errors.push e in if fail_evar then raise e
 
-let check_typeclasses_instances_are_solved env sigma =
+let check_typeclasses_instances_are_solved env current_sigma pending =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses env (ref sigma) true
+  apply_typeclasses env (ref current_sigma) pending true
 
-let check_extra_evars_are_solved env initial_sigma sigma =
-  Evd.fold_undefined
-    (fun evk evi () ->
-      if not (Evd.mem initial_sigma evk) then
-        let (loc,k) = evar_source evk sigma in
+let check_extra_evars_are_solved env current_sigma pending =
+  fold_pending_holes
+    (fun evk () ->
+      if not (Evd.is_defined current_sigma evk) then
+        let (loc,k) = evar_source evk current_sigma in
 	match k with
 	| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
 	| _ ->
-	    let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
-	    error_unsolvable_implicit loc env sigma evi k None) sigma ()
+	    let evi = nf_evar_info current_sigma (Evd.find_undefined current_sigma evk) in
+	    error_unsolvable_implicit loc env current_sigma evi k None) pending ()
 
-let check_evars_are_solved env initial_sigma sigma =
-  check_typeclasses_instances_are_solved env sigma;
-  check_problems_are_solved env sigma;
-  check_extra_evars_are_solved env initial_sigma sigma
+let check_evars_are_solved env current_sigma pending =
+  check_typeclasses_instances_are_solved env current_sigma pending;
+  check_problems_are_solved env current_sigma;
+  check_extra_evars_are_solved env current_sigma pending
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
-let solve_remaining_evars flags env initial_sigma sigma =
-  let evdref = ref sigma in
-  if flags.use_typeclasses then apply_typeclasses env evdref false;
+let solve_remaining_evars flags env current_sigma pending =
+  let evdref = ref current_sigma in
+  if flags.use_typeclasses then apply_typeclasses env evdref pending false;
   if Option.has_some flags.use_hook then
-    apply_inference_hook (Option.get flags.use_hook env) initial_sigma evdref;
+    apply_inference_hook (Option.get flags.use_hook env) evdref pending;
   if flags.use_unif_heuristics then apply_heuristics env evdref false;
-  if flags.fail_evar then check_evars_are_solved env initial_sigma !evdref;
+  if flags.fail_evar then check_evars_are_solved env !evdref pending;
   !evdref
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
-  let sigma = solve_remaining_evars flags env initial_sigma sigma in
+  let sigma = solve_remaining_evars flags env sigma (initial_sigma,sigma) in
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 5df4c8372..eb5626474 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -108,14 +108,17 @@ val understand_judgment_tcc : env -> evar_map ref ->
 
 (** Trying to solve remaining evars and remaining conversion problems
     with type classes, heuristics, and possibly an external solver *)
+(* For simplicity, it is assumed that current map has no other evars
+   with candidate and no other conversion problems that the one in
+   [pending], however, it can contain more evars than the pending ones. *)
 
 val solve_remaining_evars : inference_flags ->
-  env -> (* initial map *) evar_map -> (* map to solve *) evar_map -> evar_map
+  env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map
 
 (** Checking evars are all solved and reporting an appropriate error message *)
 
 val check_evars_are_solved :
-  env -> (* initial map: *) evar_map -> (* map to check: *) evar_map -> unit
+  env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
 
 (**/**)
 (** Internal of Pretyping... *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b2938cb99..d86da79d6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1131,7 +1131,7 @@ let abstract_scheme env (locc,a) (c, sigma) =
   if occur_meta a then
     mkLambda (na,ta,c), sigma
   else
-    let c', sigma' = subst_closed_term_occ env sigma locc a c in
+    let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
       mkLambda (na,ta,c'), sigma'
 
 let pattern_occs loccs_trm env sigma c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 527199e3b..2f1c230b7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -90,7 +90,7 @@ let abstract_scheme env evd c l lname_typ =
 
 let abstract_list_all env evd typ c l =
   let ctxt,_ = splay_prod_n env evd (List.length l) typ in
-  let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in
+  let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
   let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
   let evd,typp =
     try Typing.e_type_of env evd p
@@ -1362,9 +1362,10 @@ let indirectly_dependent c d decls =
 let indirect_dependency d decls =
   pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls))
 
-let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) =
-  let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
-  in Evd.evar_universe_context sigma, nf_evar sigma c
+let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
+  let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
+  let sigma, subst = nf_univ_variables sigma in
+  sigma, subst_univs_constr subst (nf_evar sigma c)
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1394,7 +1395,7 @@ let default_matching_merge_flags sigma =
     use_pattern_unification = true;
 }
 
-let default_matching_flags sigma =
+let default_matching_flags (sigma,_) =
   let flags = default_matching_core_flags sigma in {
   core_unify_flags = flags;
   merge_unify_flags = default_matching_merge_flags sigma;
@@ -1404,12 +1405,35 @@ let default_matching_flags sigma =
 }
 
 (* This supports search of occurrences of term from a pattern *)
+(* from_prefix is useful e.g. for subterms in an inductive type: we can say *)
+(* "destruct t" and it finds "t u" *)
 
-let make_pattern_test inf_flags env sigma0 (sigma,c) =
-  let flags = default_matching_flags sigma0 in
+exception PatternNotFound
+
+let make_pattern_test from_prefix_of_ind env sigma (pending,c) =
+  let flags = default_matching_flags pending in
+  let n = List.length (snd (decompose_app c)) in
   let matching_fun _ t =
-    try let sigma = w_typed_unify env sigma Reduction.CONV flags c t in
-	  Some(sigma, t)
+    try
+      let t' =
+        if from_prefix_of_ind then
+          (* We check for fully applied subterms of the form "u u1 .. un" *)
+          (* of inductive type knowning only a prefix "u u1 .. ui" *)
+          let t,l = decompose_app t in
+          let l1,l2 =
+            try List.chop n l with Failure _ -> raise (NotUnifiable None) in
+          if not (List.for_all closed0 l2) then raise (NotUnifiable None)
+          else
+            applist (t,l1)
+        else t in
+      let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in
+      let _ =
+        if from_prefix_of_ind then
+          (* We check that the subterm we found from prefix is applied *)
+          (* enough to be of inductive type *)
+          try ignore (Inductiveops.find_mrectype env sigma (Retyping.get_type_of env sigma t))
+          with UserError _ -> raise (NotUnifiable None) in
+      Some(sigma, t)
     with
     | PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
         raise (NotUnifiable (Some (c1,c2,e)))
@@ -1425,22 +1449,25 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) =
   { match_fun = matching_fun; merge_fun = merge_fun;
     testing_state = None; last_found = None },
   (fun test -> match test.testing_state with
-  | None ->
-      finish_evar_resolution ~flags:inf_flags env sigma0 (sigma,c)
+  | None -> None
+(*
+     let sigma, c = finish_evar_resolution ~flags:inf_flags env sigma (pending,c) in
+     sigma,c
+*)
   | Some (sigma,_) ->
+     let c = nf_evar sigma (local_strong whd_meta sigma c) in
      let univs, subst = nf_univ_variables sigma in
-     Evd.evar_universe_context univs,
-     subst_univs_constr subst (nf_evar sigma c))
+     Some (sigma,subst_univs_constr subst c))
 
 let make_eq_test env evd c =
   let out cstr =
-    Evd.evar_universe_context cstr.testing_state, c
+    match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, c)
   in
-    (make_eq_univs_test env evd c, out)
+  (make_eq_univs_test env evd c, out)
 
-let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl =
+let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
-    let t = match ty with Some t -> t | None -> get_type_of env sigmac c in
+    let t = match ty with Some t -> t | None -> get_type_of env sigma c in
     let x = id_of_name_using_hdchar (Global.env()) t name in
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
@@ -1450,9 +1477,9 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
       x
   in
   let mkvarid () = mkVar id in
-  let compute_dependency _ (hyp,_,_ as d) depdecls =
+  let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) =
     match occurrences_of_hyp hyp occs with
-    | NoOccurrences, InHyp ->
+    | AtOccs (NoOccurrences, InHyp) ->
         if indirectly_dependent c d depdecls then
           (* Told explicitly not to abstract over [d], but it is dependent *)
           let id' = indirect_dependency d depdecls in
@@ -1460,31 +1487,34 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
             ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
             ++ str ".")
         else
-          depdecls
-    | (AllOccurrences, InHyp) as occ ->
+          (push_named_context_val d sign,depdecls)
+    | (AtOccs (AllOccurrences, InHyp) | LikeFirst) as occ ->
         let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
         if Context.eq_named_declaration d newdecl
            && not (indirectly_dependent c d depdecls)
         then
           if check_occs && not (in_every_hyp occs)
-          then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp)))
-          else depdecls
+          then raise (PretypeError (env,sigma,NoOccurrenceFound (c,Some hyp)))
+          else (push_named_context_val d sign, depdecls)
         else
-          newdecl :: depdecls
+          (push_named_context_val newdecl sign, newdecl :: depdecls)
     | occ ->
-        replace_term_occ_decl_modulo occ test mkvarid d :: depdecls in
+        let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
+        (push_named_context_val newdecl sign, newdecl :: depdecls) in
   try
-    let depdecls = fold_named_context compute_dependency env ~init:[] in
+    let sign,depdecls =
+      fold_named_context compute_dependency env
+        ~init:(empty_named_context_val,[]) in
     let ccl = match occurrences_of_goal occs with
-      | NoOccurrences -> concl
+      | AtOccs NoOccurrences -> concl
       | occ -> replace_term_occ_modulo occ test mkvarid concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in
-    (id,depdecls,lastlhyp,ccl,out test)
+      (id,sign,depdecls,lastlhyp,ccl,out test)
   with
     SubtermUnificationError e ->
-      raise (PretypeError (env,sigmac,CannotUnifyOccurrences e))
+      raise (PretypeError (env,sigma,CannotUnifyOccurrences e))
 
 (** [make_abstraction] is the main entry point to abstract over a term
     or pattern at some occurrences; it returns:
@@ -1497,22 +1527,27 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
     - the term or pattern to abstract fully instantiated
 *)
 
+type prefix_of_inductive_support_flag = bool
+
 type abstraction_request =
-| AbstractPattern of Name.t * (evar_map * constr) * clause * bool * Pretyping.inference_flags
+| AbstractPattern of prefix_of_inductive_support_flag * Name.t * pending_constr * clause or_like_first * bool
 | AbstractExact of Name.t * constr * types option * clause * bool
 
 type abstraction_result =
-  Names.Id.t * Context.named_declaration list * Names.Id.t option *
-    constr * (Evd.evar_universe_context * constr)
+  Names.Id.t * named_context_val *
+    Context.named_declaration list * Names.Id.t option *
+    types * (Evd.evar_map * constr) option
 
 let make_abstraction env evd ccl abs =
   match abs with
-  | AbstractPattern (name,c,occs,check_occs,flags) ->
+  | AbstractPattern (from_prefix,name,c,occs,check_occs) ->
       make_abstraction_core name
-        (make_pattern_test flags env evd c) c None occs check_occs env ccl
+        (make_pattern_test from_prefix env evd c)
+        env evd (snd c) None occs check_occs ccl
   | AbstractExact (name,c,ty,occs,check_occs) ->
       make_abstraction_core name
-        (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl
+        (make_eq_test env evd c)
+        env evd c ty (AtOccs occs) check_occs ccl
 
 let keyed_unify env evd kop = 
   if not !keyed_unification then fun cl -> true
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index bedd6bf16..3b4998129 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -45,7 +45,7 @@ val elim_no_delta_flags : unit -> unify_flags
 val w_unify :
   env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map
 
-(** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
+(** [w_unify_to_subterm env m (c,t)] performs unification of [c] with a
    subterm of [t]. Constraints are added to [m] and the matched
    subterm of [t] is also returned. *)
 val w_unify_to_subterm :
@@ -63,20 +63,25 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
 
 (* Looking for subterms in contexts at some occurrences, possibly with pattern*)
 
+exception PatternNotFound
+
 type abstraction_request =
-| AbstractPattern of Names.Name.t * (evar_map * constr) * Locus.clause * bool * Pretyping.inference_flags
+| AbstractPattern of bool * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool
 | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
 
 val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
-  env -> Evd.evar_map -> open_constr -> Evd.evar_universe_context * constr
+  env -> Evd.evar_map -> pending_constr -> Evd.evar_map * constr
 
 type abstraction_result =
-  Names.Id.t * Context.named_declaration list * Names.Id.t option *
-    constr * (Evd.evar_universe_context * constr)
+  Names.Id.t * named_context_val *
+    Context.named_declaration list * Names.Id.t option *
+    types * (Evd.evar_map * constr) option
 
 val make_abstraction : env -> Evd.evar_map -> constr ->
   abstraction_request -> abstraction_result
 
+val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr
+
 (*i This should be in another module i*)
 
 (** [abstract_list_all env evd t c l]