Made the subterm finding function make_abstraction independent of the

proof engine. Moved it to unification.ml.

11 files changed, 255 insertions, 191 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index dcd3f0efb..f826984b4 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -137,9 +137,9 @@ Detyping
 Indrec
 Program
 Coercion
-Unification
 Cases
 Pretyping
+Unification
 Declaremods
 Library
 States
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 003665db5..d8f51054d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -46,6 +46,7 @@ type pretype_error =
   | UnexpectedType of constr * constr
   | NotProduct of constr
   | TypingError of type_error
+  | CannotUnifyOccurrences of Termops.subterm_unification_error
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index d9ee969e3..f8e39f316 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -47,6 +47,7 @@ type pretype_error =
   | UnexpectedType of constr * constr
   | NotProduct of constr
   | TypingError of type_error
+  | CannotUnifyOccurrences of Termops.subterm_unification_error
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index a4c72f482..f1a9d6915 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -26,8 +26,8 @@ Typeclasses
 Classops
 Program
 Coercion
-Unification
 Detyping
 Indrec
 Cases
 Pretyping
+Unification
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a32d54b5e..75f6f66fe 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -22,6 +22,7 @@ open Reductionops
 open Cbv
 open Patternops
 open Locus
+open Pretype_errors
 
 (* Errors *)
 
@@ -960,7 +961,7 @@ let e_contextually byhead (occs,c) f env sigma t =
   in
   let t' = traverse (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
-    !evd, t'
+  !evd, t'
 
 let contextually byhead occs f env sigma t =
   let f' subst env sigma t = sigma, f subst env sigma t in
@@ -1075,9 +1076,9 @@ let compute = cbv_betadeltaiota
 (* Pattern *)
 
 let make_eq_univs_test evd c =
-  { match_fun = (fun evd c' -> 
-    let b, cst = Universes.eq_constr_universes c c' in 
-      if b then 
+  { match_fun = (fun evd c' ->
+    let b, cst = Universes.eq_constr_universes c c' in
+      if b then
 	try Evd.add_universe_constraints evd cst
 	with Evd.UniversesDiffer -> raise NotUnifiable
       else raise NotUnifiable);
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d9cd58cea..67559e686 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -679,30 +679,33 @@ let replace_term = replace_term_gen eq_constr
    occurrence except the ones in l and b=false, means all occurrences
    except the ones in l *)
 
-let error_invalid_occurrence l =
+type occurrence_error =
+  | InvalidOccurrence of int list
+  | IncorrectInValueOccurrence of Id.t
+
+let explain_invalid_occurrence l =
   let l = List.sort_uniquize Int.compare l in
-  errorlabstrm ""
-    (str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") ++
-     prlist_with_sep spc int l ++ str ".")
-
-let pr_position (cl,pos) =
-  let clpos = match cl with
-    | None -> str " of the goal"
-    | Some (id,InHyp) -> str " of hypothesis " ++ pr_id id
-    | Some (id,InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id
-    | Some (id,InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
-  int pos ++ clpos
-
-let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) =
-  let s = if nested then "Found nested occurrences of the pattern"
-    else "Found incompatible occurrences of the pattern" in
-  errorlabstrm ""
-    (str s ++ str ":" ++
-     spc () ++ str "Matched term " ++ quote (print_constr t2) ++
-     strbrk " at position " ++ pr_position (cl2,pos2) ++ 
-     strbrk " is not compatible with matched term " ++
-     quote (print_constr t1) ++ strbrk " at position " ++ 
-     pr_position (cl1,pos1) ++ str ".")
+  str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
+  ++ prlist_with_sep spc int l ++ str "."
+
+let explain_incorrect_in_value_occurrence id =
+  pr_id id ++ str " has no value."
+
+let explain_occurrence_error = function
+  | InvalidOccurrence l -> explain_invalid_occurrence l
+  | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
+
+let error_occurrences_error e =
+  errorlabstrm "" (explain_occurrence_error e)
+
+let error_invalid_occurrence occ =
+  error_occurrences_error (InvalidOccurrence occ)
+
+type position =(Id.t * Locus.hyp_location_flag) option
+
+type subterm_unification_error = bool * (position * int * constr) * (position * int * constr)
+
+exception SubtermUnificationError of subterm_unification_error
 
 exception NotUnifiable
 
@@ -724,7 +727,7 @@ let subst_closed_term_occ_gen_modulo occs test cl occ t =
       test.last_found <- Some (cl,!pos,t)
     with NotUnifiable ->
       let lastpos = Option.get test.last_found in
-      error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos in
+     raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos)) in
   let rec substrec k t =
     if nowhere_except_in && !pos > maxocc then t else
     try
@@ -749,7 +752,7 @@ let check_used_occurrences nbocc (nowhere_except_in,locs) =
   let rest = List.filter (fun o -> o >= nbocc) locs in
   match rest with
   | [] -> ()
-  | _ -> error_invalid_occurrence rest
+  | _ -> error_occurrences_error (InvalidOccurrence rest)
 
 let proceed_with_occurrences f occs x =
   match occs with
@@ -785,7 +788,7 @@ let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
   let f = f (Some (id,hyploc)) in
   match bodyopt,hyploc with
   | None, InHypValueOnly ->
-      errorlabstrm "" (pr_id id ++ str " has no value.")
+      error_occurrences_error (IncorrectInValueOccurrence id)
   | None, _ | Some _, InHypTypeOnly ->
       let acc,typ = f acc typ in acc,(id,bodyopt,typ)
   | Some body, InHypValueOnly ->
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 8b4d02e04..72a115231 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -155,7 +155,16 @@ val subst_closed_term_occ_gen :
     testing function returning a substitution of type ['a] (or failing
     with NotUnifiable); a function for merging substitution (possibly
     failing with NotUnifiable) and an initial substitution are
-    required too *)
+    required too; [subst_closed_term_occ_modulo] itself turns a
+    NotUnifiable exception into a SubtermUnificationError *)
+
+exception NotUnifiable
+
+type position =(Id.t * Locus.hyp_location_flag) option
+
+type subterm_unification_error = bool * (position * int * constr) * (position * int * constr)
+
+exception SubtermUnificationError of subterm_unification_error
 
 type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
@@ -166,8 +175,6 @@ type 'a testing_function = {
 
 val make_eq_test : constr -> unit testing_function
 
-exception NotUnifiable
-
 val subst_closed_term_occ_modulo :
   occurrences -> 'a testing_function -> (Id.t * hyp_location_flag) option
   -> constr -> types
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 219d03b9e..dbdc0a4e4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -24,6 +24,7 @@ open Retyping
 open Coercion
 open Recordops
 open Locus
+open Locusops
 
 let occur_meta_or_undefined_evar evd c =
   let rec occrec c = match kind_of_term c with
@@ -1156,6 +1157,153 @@ let iter_fail f a =
       with ex when precatchable_exception ex -> ffail (i+1)
   in ffail 0
 
+(* make_abstraction: a variant of w_unify_to_subterm which works on
+   contexts, with evars, and possibly with occurrences *)
+
+let out_arg = function
+  | Misctypes.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
+  | Misctypes.ArgArg x -> x
+
+let occurrences_of_hyp id cls =
+  let rec hyp_occ = function
+      [] -> None
+    | ((occs,id'),hl)::_ when Id.equal id id' ->
+        Some (occurrences_map (List.map out_arg) occs, hl)
+    | _::l -> hyp_occ l in
+  match cls.onhyps with
+      None -> Some (AllOccurrences,InHyp)
+    | Some l -> hyp_occ l
+
+let occurrences_of_goal cls =
+  if cls.concl_occs == NoOccurrences then None
+  else Some (occurrences_map (List.map out_arg) cls.concl_occs)
+
+let in_every_hyp cls = Option.is_empty cls.onhyps
+
+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 default_matching_flags sigma = {
+  modulo_conv_on_closed_terms = Some empty_transparent_state;
+  use_metas_eagerly_in_conv_on_closed_terms = false;
+  modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = Some full_transparent_state;
+  check_applied_meta_types = true;
+  resolve_evars = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = false;
+  frozen_evars =
+    fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
+      sigma Evar.Set.empty;
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = false;
+  modulo_eta = false;
+  allow_K_in_toplevel_higher_order_unification = false
+}
+
+(* This supports search of occurrences of term from a pattern *)
+
+let make_pattern_test inf_flags env sigma0 (sigma,c) =
+  let flags = default_matching_flags sigma0 in
+  let matching_fun _ t =
+    try let sigma = w_typed_unify env sigma Reduction.CONV flags c t in
+	  Some(sigma, t)
+    with e when Errors.noncritical e -> raise NotUnifiable in
+  let merge_fun c1 c2 =
+    match c1, c2 with
+    | Some (evd,c1), Some (_,c2) ->
+      (try let evd = w_typed_unify env evd Reduction.CONV flags c1 c2 in
+	     Some (evd, c1)
+       with e when Errors.noncritical e -> raise NotUnifiable)
+    | Some _, None -> c1
+    | None, Some _ -> c2
+    | None, None -> None
+  in
+  { 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)
+  | Some (sigma,_) ->
+     let univs, subst = nf_univ_variables sigma in
+     Evd.evar_universe_context univs,
+     subst_univs_constr subst (nf_evar sigma c))
+
+let make_eq_test evd c =
+  let out cstr =
+    Evd.evar_universe_context cstr.testing_state, c
+  in
+    (Tacred.make_eq_univs_test evd c, out)
+
+let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl =
+  let id =
+    let t = match ty with Some t -> t | None -> get_type_of env sigmac 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
+    if mem_named_context x (named_context env) then
+      error ("The variable "^(Id.to_string x)^" is already declared.")
+    else
+      x
+  in
+  let compute_dependency _ (hyp,_,_ as d) depdecls =
+    match occurrences_of_hyp hyp occs with
+    | None -> depdecls
+    | Some ((AllOccurrences, InHyp) as occ) ->
+        let newdecl = subst_closed_term_occ_decl_modulo occ test d in
+        if Context.eq_named_declaration d newdecl then
+          if check_occs && not (in_every_hyp occs)
+          then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp)))
+          else depdecls
+        else
+          (subst1_named_decl (mkVar id) newdecl)::depdecls
+    | Some occ ->
+        let newdecl = subst_closed_term_occ_decl_modulo occ test d in
+        (subst1_named_decl (mkVar id) newdecl)::depdecls in
+  try
+    let depdecls = fold_named_context compute_dependency env ~init:[] in
+    let ccl = match occurrences_of_goal occs with
+      | None -> concl
+      | Some occ ->
+          subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None concl)
+    in
+    let lastlhyp =
+      if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in
+    (id,depdecls,lastlhyp,ccl,out test)
+  with
+    SubtermUnificationError e ->
+      raise (PretypeError (env,sigmac,CannotUnifyOccurrences e))
+
+(** [make_abstraction] is the main entry point to abstract over a term
+    or pattern at some occurrences; it returns:
+    - the id used for the abstraction
+    - the type of the abstraction
+    - the hypotheses from the context which depend on the term or pattern
+    - the most recent hyp before which there is no dependency in the term of pattern
+    - the abstracted conclusion
+    - an evar universe context effect to apply on the goal
+    - the term or pattern to abstract fully instantiated
+*)
+
+type abstraction_request =
+| AbstractPattern of Name.t * (evar_map * constr) * clause * bool * Pretyping.inference_flags
+| 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)
+
+let make_abstraction env evd ccl abs =
+  match abs with
+  | AbstractPattern (name,c,occs,check_occs,flags) ->
+      make_abstraction_core name
+        (make_pattern_test flags env evd c) c None occs check_occs env ccl
+  | AbstractExact (name,c,ty,occs,check_occs) ->
+      make_abstraction_core name
+        (make_eq_test evd c) (evd,c) ty occs check_occs env ccl
+
 (* Tries to find an instance of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] until it finds a match.
    Fails if no match is found *)
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 3f93d817d..de8eecc27 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -53,6 +53,22 @@ val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map
 val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
   evar_map * constr
 
+(* Looking for subterms in contexts at some occurrences, possibly with pattern*)
+
+type abstraction_request =
+| AbstractPattern of Names.Name.t * (evar_map * constr) * Locus.clause * bool * Pretyping.inference_flags
+| 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
+
+type abstraction_result =
+  Names.Id.t * Context.named_declaration list * Names.Id.t option *
+    constr * (Evd.evar_universe_context * constr)
+
+val make_abstraction : env -> Evd.evar_map -> constr ->
+  abstraction_request -> abstraction_result
+
 (*i This should be in another module i*)
 
 (** [abstract_list_all env evd t c l]
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8dfd1b14b..450b48d45 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -86,18 +86,6 @@ let _ =
       optread  = (fun () -> !Flags.tactic_context_compat) ;
       optwrite = (fun b -> Flags.tactic_context_compat := b) }
 
-let tactic_infer_flags = {
-  Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
-  Pretyping.use_hook = Some solve_by_implicit_tactic;
-  Pretyping.fail_evar = true;
-  Pretyping.expand_evars = true }
-
-let finish_evar_resolution env initial_sigma (sigma,c) =
-  let sigma =
-    Pretyping.solve_remaining_evars tactic_infer_flags env initial_sigma sigma
-  in Evd.evar_universe_context sigma, nf_evar sigma c
-
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -1740,141 +1728,19 @@ let apply_in simple with_evars id lemmas ipat =
 (* Tactics abstracting terms *)
 (*****************************)
 
-let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | ArgArg x -> x
-
-let occurrences_of_hyp id cls =
-  let rec hyp_occ = function
-      [] -> None
-    | ((occs,id'),hl)::_ when Id.equal id id' ->
-        Some (occurrences_map (List.map out_arg) occs, hl)
-    | _::l -> hyp_occ l in
-  match cls.onhyps with
-      None -> Some (AllOccurrences,InHyp)
-    | Some l -> hyp_occ l
-
-let occurrences_of_goal cls =
-  if cls.concl_occs == NoOccurrences then None
-  else Some (occurrences_map (List.map out_arg) cls.concl_occs)
-
-let in_every_hyp cls = Option.is_empty cls.onhyps
-
 (* Implementation without generalisation: abbrev will be lost in hyps in *)
 (* in the extracted proof *)
 
-let default_matching_flags sigma = {
-  modulo_conv_on_closed_terms = Some empty_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = false;
-  modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
-  modulo_delta_in_merge = Some full_transparent_state;
-  check_applied_meta_types = true;
-  resolve_evars = false;
-  use_pattern_unification = false;
-  use_meta_bound_pattern_unification = false;
-  frozen_evars =
-    fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
-      sigma Evar.Set.empty;
-  restrict_conv_on_strict_subterms = false;
-  modulo_betaiota = false;
-  modulo_eta = false;
-  allow_K_in_toplevel_higher_order_unification = false
-}
-
-(* This supports search of occurrences of term from a pattern *)
-
-let make_pattern_test env sigma0 (sigma,c) =
-  let flags = default_matching_flags sigma0 in
-  let matching_fun _ t =
-    try let sigma = w_unify env sigma Reduction.CONV ~flags c t in
-	  Some(sigma, t)
-    with e when Errors.noncritical e -> raise NotUnifiable in
-  let merge_fun c1 c2 =
-    match c1, c2 with
-    | Some (evd,c1), Some (_,c2) ->
-      (try let evd = w_unify env evd Reduction.CONV ~flags c1 c2 in
-	     Some (evd, c1)
-       with e when Errors.noncritical e -> raise NotUnifiable)
-    | Some _, None -> c1
-    | None, Some _ -> c2
-    | None, None -> None
-  in
-  { match_fun = matching_fun; merge_fun = merge_fun;
-    testing_state = None; last_found = None },
-  (fun test -> match test.testing_state with
-  | None ->
-    let ctx, c = finish_evar_resolution env sigma0 (sigma,c) in
-      Proofview.V82.tclEVARUNIVCONTEXT ctx, c
-  | Some (sigma,_) ->
-     let univs, subst = nf_univ_variables sigma in
-       Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context univs),
-       subst_univs_constr subst (nf_evar sigma c))
-
-let make_eq_test evd c =
-  let out cstr = 
-    let tac = Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context cstr.testing_state) in
-      tac, c
-  in
-    (Tacred.make_eq_univs_test evd c, out)
-
-let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs gl =
-  let env = Proofview.Goal.env gl in
-  let id =
-    let t = match ty with Some t -> t | None -> typ_of env sigmac c in
-    let x = id_of_name_using_hdchar (Global.env()) t name in
-    if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) gl else
-      let hyps = Proofview.Goal.hyps gl in
-      if not (mem_named_context x hyps) then x else
-	error ("The variable "^(Id.to_string x)^" is already declared.")
-  in
-  let compute_dependency _ (hyp,_,_ as d) depdecls =
-    match occurrences_of_hyp hyp occs with
-      | None -> depdecls
-      | Some ((AllOccurrences, InHyp) as occ) ->
-          let newdecl = subst_closed_term_occ_decl_modulo occ test d in
-          if eq_named_declaration d newdecl then
-            if check_occs && not (in_every_hyp occs)
-            then raise (RefinerError (DoesNotOccurIn (c,hyp)))
-            else depdecls
-          else
-            (subst1_named_decl (mkVar id) newdecl)::depdecls
-      | Some occ ->
-          let newdecl = subst_closed_term_occ_decl_modulo occ test d in
-	    (subst1_named_decl (mkVar id) newdecl)::depdecls in
-  let depdecls = fold_named_context compute_dependency env ~init:[] in
-  let concl = Proofview.Goal.concl gl in
-  let ccl = match occurrences_of_goal occs with
-    | None -> concl
-    | Some occ ->
-        subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None concl) in
-  let lastlhyp =
-    if List.is_empty depdecls then MoveLast else MoveAfter(pi1(List.last depdecls)) in
-  (id,depdecls,lastlhyp,ccl,out test)
-
-(** [make_abstraction] is the main entry point to abstract over a term
-    or pattern at some occurrences; it returns:
-    - the id used for the abstraction
-    - the type of the abstraction
-    - the hypotheses from the context which depend on the term or pattern
-    - the most recent hyp before which there is no dependency in the term of pattern
-    - the abstracted conclusion
-    - a tactic to apply to take evars effects into account
-    - the term or pattern to abstract fully instantiated
-*)
-
-type abstraction_request =
-| AbstractPattern of Name.t * (evar_map * constr) * clause * bool
-| AbstractExact of Name.t * constr * types option * clause * bool
+let tactic_infer_flags = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.use_unif_heuristics = true;
+  Pretyping.use_hook = Some solve_by_implicit_tactic;
+  Pretyping.fail_evar = true;
+  Pretyping.expand_evars = true }
 
-let make_abstraction abs gl =
-  let evd = Proofview.Goal.sigma gl in
-  let env = Proofview.Goal.env gl in
-  match abs with
-  | AbstractPattern (name,c,occs,check_occs) ->
-      make_abstraction_core name (make_pattern_test env evd c) c None occs check_occs gl
-  | AbstractExact (name,c,ty,occs,check_occs) ->
-      make_abstraction_core name (make_eq_test evd c) (evd,c) ty occs check_occs gl
+let decode_hyp = function
+  | None -> MoveLast
+  | Some id -> MoveAfter id
 
 (* [letin_tac b (... abstract over c ...) gl] transforms
    [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
@@ -1885,7 +1751,9 @@ let make_abstraction abs gl =
 let letin_tac_gen with_eq abs ty =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let (id,depdecls,lastlhyp,ccl,(tac,c)) = make_abstraction abs gl in
+    let evd = Proofview.Goal.sigma gl in
+    let ccl = Proofview.Goal.concl gl in
+    let (id,depdecls,lastlhyp,ccl,(ctx,c)) = make_abstraction env evd ccl abs in
     let t = match ty with Some t -> t | _ -> typ_of env (Proofview.Goal.sigma gl) c in
     let eq_tac gl = match with_eq with
       | Some (lr,(loc,ido)) ->
@@ -1904,26 +1772,26 @@ let letin_tac_gen with_eq abs ty =
 	  let sigma, _ = Typing.e_type_of env sigma term in
             sigma, term,
             Tacticals.New.tclTHEN
-	      (intro_gen loc (IntroMustBe heq) lastlhyp true false)
+	      (intro_gen loc (IntroMustBe heq) (decode_hyp lastlhyp) true false)
 	      (Proofview.V82.tactic (thin_body [heq;id]))
       | None ->
 	  (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
-    Proofview.tclBIND tac (fun () ->
-      Proofview.Goal.enter (fun gl -> 
-	let (sigma,newcl,eq_tac) = eq_tac gl in
-	  Tacticals.New.tclTHENLIST
-	    [ Proofview.V82.tclEVARS sigma; 
-	      Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
-              intro_gen dloc (IntroMustBe id) lastlhyp true false;
-              Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
-              eq_tac ]))
+    Proofview.Goal.enter (fun gl -> 
+      let (sigma,newcl,eq_tac) = eq_tac gl in
+      Tacticals.New.tclTHENLIST
+	[ Proofview.V82.tclEVARS sigma;
+          Proofview.V82.tclEVARUNIVCONTEXT ctx;
+	  Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
+          intro_gen dloc (IntroMustBe id) (decode_hyp lastlhyp) true false;
+          Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
+          eq_tac ])
   end
 
 let letin_tac with_eq name c ty occs =
   letin_tac_gen with_eq (AbstractExact (name,c,ty,occs,true)) ty
 
 let letin_pat_tac with_eq name c occs =
-  letin_tac_gen with_eq (AbstractPattern (name,c,occs,false)) None
+  letin_tac_gen with_eq (AbstractPattern (name,c,occs,false,tactic_infer_flags)) None
 
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c =
@@ -3437,7 +3305,7 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	    Tacticals.New.tclTHEN
             (* Warning: letin is buggy when c is not of inductive type *)
 	      (letin_tac_gen with_eq
-                 (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false)) None)
+                 (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false,tactic_infer_flags)) None)
 	      (induction_with_atomization_of_ind_arg
 	         isrec with_evars elim names (id,lbind) inhyps)
           end
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 90e358828..d251b571c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -637,6 +637,24 @@ let explain_type_error env sigma err =
   | UnsatisfiedConstraints cst ->
       explain_unsatisfied_constraints env cst
 
+let pr_position (cl,pos) =
+  let clpos = match cl with
+    | None -> str " of the goal"
+    | Some (id,Locus.InHyp) -> str " of hypothesis " ++ pr_id id
+    | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id
+    | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
+  int pos ++ clpos
+
+let explain_cannot_unify_occurrences env nested (cl2,pos2,t2) (cl1,pos1,t1) =
+  let s = if nested then "Found nested occurrences of the pattern"
+    else "Found incompatible occurrences of the pattern" in
+  str s ++ str ":" ++
+  spc () ++ str "Matched term " ++ pr_lconstr_env env t2 ++
+  strbrk " at position " ++ pr_position (cl2,pos2) ++
+  strbrk " is not compatible with matched term " ++
+  pr_lconstr_env env t1 ++ strbrk " at position " ++ 
+  pr_position (cl1,pos1) ++ str "."
+
 let explain_pretype_error env sigma err =
   let env = Evarutil.env_nf_betaiotaevar sigma env in
   let env = make_all_name_different env in
@@ -669,6 +687,7 @@ let explain_pretype_error env sigma err =
   | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
   | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
   | TypingError t -> explain_type_error env sigma t
+  | CannotUnifyOccurrences (b,c1,c2) -> explain_cannot_unify_occurrences env b c1 c2
 
 (* Module errors *)