Added support for referring to subterms of the goal by pattern.

Tactics set/remember and destruct/induction take benefit of it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 315 insertions, 150 deletions

diff --git a/CHANGES b/CHANGES
index e6d510809..9320735c4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -48,6 +48,8 @@ Tactics
   from a context containing an arithmetical contradiction (wish #2236).
 - Using "auto with nocore" disables the use of the "core" database (wish #2188).
   This pseudo-database "nocore" can also be used with trivial and eauto.
+- Tactics "set", "destruct" and "induction" accepts incomplete terms and
+  use the goal to complete the pattern assuming it is no ambiguous.
 
 Vernacular commands
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 200919b8c..e027794f8 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -591,6 +591,11 @@ hypotheses of the current goal and adds the new definition {\ident
 {\tt :=} \term} to the local context. The default is to make this
 replacement only in the conclusion.
 
+If {\term} has holes (i.e. subexpressions of the form ``\_''), the
+tactic first checks that all subterms matching the pattern are
+compatible before doing the replacement using the leftmost subterm
+matching the pattern.
+
 \begin{Variants}
 
 \item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}}
@@ -626,7 +631,7 @@ Section~\ref{Occurrences clauses}.
   This is a more general form of {\tt remember} that remembers the
   occurrences of {\term} specified by an occurrences set.
 
-\item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
+\item {\tt pose ( {\ident} := {\term} )}
   
   This adds the local definition {\ident} := {\term} to the current
   context without performing any replacement in the goal or in the
@@ -1619,18 +1624,16 @@ Section~\ref{Cic-inductive-definitions}).
 \subsection{\tt induction \term
 \tacindex{induction}}
 
-This tactic applies to any goal. The type of the argument {\term} must
-be an inductive constant. Then, the tactic {\tt induction}
-generates subgoals, one for each possible form of {\term}, i.e. one
-for each constructor of the inductive type.
+This tactic applies to any goal. The argument {\term} must be of
+inductive type and the tactic {\tt induction} generates subgoals,
+one for each possible form of {\term}, i.e. one for each constructor
+of the inductive type.
 
-The tactic {\tt induction} automatically replaces every occurrences
-of {\term} in the conclusion and the hypotheses of the goal.  It
-automatically adds induction hypotheses (using names of the form {\tt
-  IHn1}) to the local context. If some hypothesis must not be taken
-into account in the induction hypothesis, then it needs to be removed
-first (you can also use the tactics {\tt elim} or {\tt simple induction},
-see below).
+If the argument is dependent in either the conclusion or some
+hypotheses of the goal, the argument is replaced by the appropriate
+constructor form in each of the resulting subgoals and induction
+hypotheses are added to the local context using names whose prefix is
+{\tt IH}.
 
 There are particular cases:
 
@@ -1642,10 +1645,13 @@ behaves as {\tt intros until {\ident}; induction {\ident}}.
 
 \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt induction} applied to the
-last introduced hypothesis.
+last introduced hypothesis. Remark: For simple induction on a numeral,
+use syntax {\tt induction ({\num})} (not very interesting anyway).
 
-\Rem For simple induction on a numeral, use syntax {\tt induction
-({\num})} (not very interesting anyway).
+\item The argument {\term} can also be a pattern of which holes are
+  denoted by ``\_''. In this case, the tactic checks that all subterms
+  matching the pattern in the conclusion and the hypotheses are
+  compatible and performs induction using this subterm.
 
 \end{itemize}
 
@@ -1833,10 +1839,19 @@ instantiate premises of the type of {\term$_2$}.
 \tacindex{destruct}}
 \label{destruct}
 
-The tactic {\tt destruct} is used to perform case analysis without
-recursion. Its behavior is similar to {\tt induction} except
-that no induction hypothesis is generated.  It applies to any goal and
-the type of {\term} must be inductively defined. There are particular cases:
+This tactic applies to any goal. The argument {\term} must be of
+inductive or coinductive type and the tactic generates subgoals, one
+for each possible form of {\term}, i.e. one for each constructor of
+the inductive or coinductive type. Unlike {\tt induction}, no
+induction hypothesis is generated by {\tt destruct}.
+
+If the argument is dependent in either the conclusion or some
+hypotheses of the goal, the argument is replaced by the appropriate
+constructor form in each of the resulting subgoals, thus performing
+case analysis. If non dependent, the tactic simply exposes the
+inductive or coinductive structure of the argument.
+
+There are special cases:
 
 \begin{itemize}
 
@@ -1846,10 +1861,13 @@ behaves as {\tt intros until {\ident}; destruct {\ident}}.
 
 \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt destruct} applied to the
-last introduced hypothesis.
+last introduced hypothesis. Remark: For destruction of a numeral, use
+syntax {\tt destruct ({\num})} (not very interesting anyway).
 
-\Rem For destruction of a numeral, use syntax {\tt destruct
-({\num})} (not very interesting anyway).
+\item The argument {\term} can also be a pattern of which holes are
+  denoted by ``\_''. In this case, the tactic checks that all subterms
+  matching the pattern in the conclusion and the hypotheses are
+  compatible and performs case analysis using this subterm.
 
 \end{itemize}
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 85c362b76..1ce6564c1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -75,7 +75,7 @@ let functional_induction with_clean c princl pat =
 	if princ_infos.Tactics.farg_in_concl
 	then [c] else []
       in
-      List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list)
+      List.map (fun c -> Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list)
     in
     let princ' = Some (princ,bindings) in
     let princ_vars =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9e8d22a87..452b395dd 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -661,6 +661,11 @@ 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 *)
 
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
 type occurrences = bool * int list
 let all_occurrences = (false,[])
 let no_occurrences_in_set = (true,[])
@@ -671,17 +676,24 @@ let error_invalid_occurrence l =
     (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
      prlist_with_sep spc int l ++ str ".")
 
-let error_cannot_unify_occurrences pos (nowhere_except_in,locs) =
-(*
-  let l = List.filter ((>) !pos) locs in
-  let l =
-    if nowhere_except_in then list_subtract (interval 1 (!pos-1)) l else l in
-  errorlabstrm "" (str "Cannot unify occurrence at position " ++ int pos ++
-    plural n " with occurrence" ++ plural n " at position" ++
-    spc() ++ pr_enum l ++ str".")
-*)
-  errorlabstrm "" (str "Cannot unify occurrence at position " ++ int pos ++
-    strbrk " in a way compatible with the other unifications found for the given term.")
+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) (nowhere_except_in,locs) =
+  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 ".")
 
 let is_selected pos (nowhere_except_in,locs) =
   nowhere_except_in && List.mem pos locs ||
@@ -689,25 +701,43 @@ let is_selected pos (nowhere_except_in,locs) =
 
 exception NotUnifiable
 
-let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) 
-    match_fun merge_fun substs occ t =
+type 'a testing_function = {
+  match_fun : constr -> 'a;
+  merge_fun : 'a -> 'a -> 'a;
+  mutable testing_state : 'a;
+  mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
+}
+
+let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl occ t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
-  let substs = ref substs in
-  let add_subst subst =
-    try substs := merge_fun subst !substs
-    with NotUnifiable -> error_cannot_unify_occurrences !pos plocs in
+  let nested = ref false in
+  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 ->
+      let lastpos = Option.get test.last_found in
+      error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos plocs in
   let rec substrec k t =
     if nowhere_except_in & !pos > maxocc then t else
     try
-      let subst = match_fun t in
-      let r = if is_selected !pos plocs then (add_subst subst; mkRel k) else t
-      in incr pos; r
-    with _ ->
-      map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
+      let subst = test.match_fun t in
+      if is_selected !pos plocs then
+        (add_subst t subst; incr pos;
+         (* Check nested matching subterms *)
+         nested := true; ignore (subst_below k t); nested := false;
+         (* Do the effective substitution *)
+         mkRel k)
+      else
+        (incr pos; 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 1 t in
-  (!substs,!pos, t')
+  (!pos, t')
 
 let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = [] 
 
@@ -724,22 +754,26 @@ let proceed_with_occurrences f plocs x =
     x
   end
 
+let make_eq_test c = {
+  match_fun = (fun c' -> if eq_constr c c' then () else raise NotUnifiable);
+  merge_fun = (fun () () -> ());
+  testing_state = ();
+  last_found = None
+} 
+
 let subst_closed_term_occ_gen plocs pos c t =
-  let (_,pos,t) = subst_closed_term_occ_gen_modulo plocs 
-    (fun c' -> if eq_constr c c' then () else raise Exit)
-    (fun () () -> ()) () pos t in
-  (pos,t)
+  subst_closed_term_occ_gen_modulo plocs (make_eq_test c) None pos t
 
 let subst_closed_term_occ plocs c t =
   proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c)
     plocs t
 
-type hyp_location_flag = (* To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
+let subst_closed_term_occ_modulo plocs test cl t =
+  proceed_with_occurrences
+    (subst_closed_term_occ_gen_modulo plocs test cl) plocs t
 
 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.")
@@ -755,19 +789,13 @@ let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
 let subst_closed_term_occ_decl (plocs,hyploc) c d =
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d
+       (fun _ occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d
 
-let subst_closed_term_occ_decl_modulo (plocs,hyploc)
-    match_fun merge_fun substs d =
-  let subst = ref substs in
+let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d =
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-        (fun occ t ->
-          let (substs,occ,t) =
-            subst_closed_term_occ_gen_modulo plocs
-              match_fun merge_fun !subst occ t
-          in subst := substs; (occ,t))
-        hyploc)
+       (subst_closed_term_occ_gen_modulo plocs test)
+       hyploc)
     plocs d
 
 let vars_of_env env =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 2e202bf07..2028e5aca 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -153,17 +153,31 @@ val no_occurrences_in_set : occurrences
 val subst_closed_term_occ_gen :
   occurrences -> int -> constr -> types -> int * types
 
-(** [subst_closed_term_occ_gen_modulo] looks for subterm modulo a
+(** [subst_closed_term_occ_modulo] looks for subterm modulo a
     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 *)
 
+type hyp_location_flag = (** To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
+type 'a testing_function = {
+  match_fun : constr -> 'a;
+  merge_fun : 'a -> 'a -> 'a;
+  mutable testing_state : 'a;
+  mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
+}
+
+val make_eq_test : constr -> unit testing_function
+
 exception NotUnifiable
 
-val subst_closed_term_occ_gen_modulo :
-  occurrences -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a ->
-  int -> constr -> 'a * int * types
+val subst_closed_term_occ_modulo :
+  occurrences -> 'a testing_function -> (identifier * hyp_location_flag) option
+  -> constr -> types
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at
    positions [occl] by [Rel 1] in [d] (see also Note OCC) *)
@@ -172,17 +186,12 @@ val subst_closed_term_occ : occurrences -> constr -> constr -> constr
 (** [subst_closed_term_occ_decl occl c decl] replaces occurrences of closed [c]
    at positions [occl] by [Rel 1] in [decl] *)
 
-type hyp_location_flag = (** To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
-
 val subst_closed_term_occ_decl :
   occurrences * hyp_location_flag -> constr -> named_declaration ->
       named_declaration
 
 val subst_closed_term_occ_decl_modulo :
-  occurrences * hyp_location_flag -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a ->
+  occurrences * hyp_location_flag -> 'a testing_function ->
   named_declaration -> named_declaration
 
 val error_invalid_occurrence : int list -> 'a
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index a92330f17..c5a2f87b6 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -64,6 +64,10 @@ let h_generalize_dep c =
 let h_let_tac b na c cl =
   let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl)
+let h_let_pat_tac b na c cl =
+  let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
+  abstract_tactic (TacLetTac (na,snd c,cl,b))
+    (letin_pat_tac with_eq na c None cl)
 
 (* Derived basic tactics *)
 let h_simple_induction_destruct isrec h =
@@ -72,10 +76,17 @@ let h_simple_induction_destruct isrec h =
 let h_simple_induction = h_simple_induction_destruct true
 let h_simple_destruct = h_simple_induction_destruct false
 
+let out_indarg = function
+  | ElimOnConstr (_,c) -> ElimOnConstr c
+  | ElimOnIdent id -> ElimOnIdent id
+  | ElimOnAnonHyp n -> ElimOnAnonHyp n
+
 let h_induction_destruct isrec ev lcl =
-  abstract_tactic (TacInductionDestruct (isrec,ev,lcl))
+  let lcl' = on_fst (List.map (fun (a,b,c) ->(List.map out_indarg a,b,c))) lcl in
+  abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
     (induction_destruct isrec ev lcl)
-let h_new_induction ev c e idl cl = h_induction_destruct true ev ([c,e,idl],cl)
+let h_new_induction ev c e idl cl =
+  h_induction_destruct true ev ([c,e,idl],cl)
 let h_new_destruct ev c e idl cl = h_induction_destruct false ev ([c,e,idl],cl)
 
 let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 8c0092980..96e7e3f03 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -57,6 +57,8 @@ val h_generalize_gen  : (constr with_occurrences * name) list -> tactic
 val h_generalize_dep  : constr -> tactic
 val h_let_tac         : letin_flag -> name -> constr ->
                         Tacticals.clause -> tactic
+val h_let_pat_tac     : letin_flag -> name -> evar_map * constr ->
+                        Tacticals.clause -> tactic
 
 (** Derived basic tactics *)
 
@@ -64,15 +66,18 @@ val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic
 val h_new_induction   : evars_flag ->
-  constr with_bindings induction_arg list -> constr with_bindings option ->
+  (evar_map * constr with_bindings) induction_arg list ->
+  constr with_bindings option ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
   Tacticals.clause option -> tactic
 val h_new_destruct    : evars_flag ->
-  constr with_bindings induction_arg list -> constr with_bindings option ->
+  (evar_map * constr with_bindings) induction_arg list ->
+  constr with_bindings option ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
   Tacticals.clause option -> tactic
 val h_induction_destruct : rec_flag -> evars_flag ->
-  (constr with_bindings induction_arg list * constr with_bindings option *
+  ((evar_map * constr with_bindings) induction_arg list *
+   constr with_bindings option *
    (intro_pattern_expr located option * intro_pattern_expr located option)) list
     * Tacticals.clause option -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 98a44c613..d0fcad21a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1264,6 +1264,9 @@ let interp_open_constr_gen kind ist =
 let interp_open_constr ccl =
   interp_open_constr_gen (OfType ccl)
 
+let interp_pure_open_constr ist =
+  interp_gen (OfType None) ist false false false false
+
 let interp_typed_pattern ist env sigma (c,_) =
   let sigma, c =
     interp_gen (OfType None) ist true false false false env sigma c in
@@ -1515,16 +1518,14 @@ let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
   let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
   sigma, (loc,cb)
 
-let interp_induction_arg ist gl sigma arg =
-  let env = pf_env gl in
+let interp_induction_arg ist gl arg =
+  let env = pf_env gl and sigma = project gl in
   match arg with
   | ElimOnConstr c ->
-      let sigma, c = interp_constr_with_bindings ist env sigma c in
-      sigma, ElimOnConstr c
-  | ElimOnAnonHyp n as x -> sigma, x
+      ElimOnConstr (interp_constr_with_bindings ist env sigma c)
+  | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (loc,id) ->
       try
-	sigma,
         match List.assoc id ist.lfun with
 	| VInteger n ->
 	    ElimOnAnonHyp n
@@ -1532,23 +1533,23 @@ let interp_induction_arg ist gl sigma arg =
 	    if Tactics.is_quantified_hypothesis id' gl
 	    then ElimOnIdent (loc,id')
 	    else
-	      (try ElimOnConstr (constr_of_id env id',NoBindings)
+	      (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
 	       with Not_found ->
 		user_err_loc (loc,"",
 		pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
 	| VConstr ([],c) ->
-	    ElimOnConstr (c,NoBindings)
+	    ElimOnConstr (sigma,(c,NoBindings))
 	| _ -> user_err_loc (loc,"",
 	      strbrk "Cannot coerce " ++ pr_id id ++
 	      strbrk " neither to a quantified hypothesis nor to a term.")
       with Not_found ->
 	(* We were in non strict (interactive) mode *)
 	if Tactics.is_quantified_hypothesis id gl then
-          sigma, ElimOnIdent (loc,id)
+          ElimOnIdent (loc,id)
 	else
           let c = (GVar (loc,id),Some (CRef (Ident (loc,id)))) in
           let c = interp_constr ist env sigma c in
-          sigma, ElimOnConstr (c,NoBindings)
+          ElimOnConstr (sigma,(c,NoBindings))
 
 (* Associates variables with values and gives the remaining variables and
    values *)
@@ -2242,7 +2243,14 @@ and interp_atomic ist gl tac =
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (na,c,clp,b) ->
       let clp = interp_clause ist gl clp in
-      h_let_tac b (interp_fresh_name ist env na) (pf_interp_constr ist gl c) clp
+      if clp = nowhere then
+        (* We try to fully-typechect the term *)
+        h_let_tac b (interp_fresh_name ist env na)
+          (pf_interp_constr ist gl c) clp
+      else
+        (* We try to keep the pattern structure as much as possible *)
+        h_let_pat_tac b (interp_fresh_name ist env na)
+          (interp_pure_open_constr ist env sigma c) clp
 
   (* Automation tactics *)
   | TacTrivial (lems,l) ->
@@ -2267,8 +2275,7 @@ and interp_atomic ist gl tac =
   | TacInductionDestruct (isrec,ev,(l,cls)) ->
       let sigma, l =
         list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) ->
-          let sigma,lc =
-            list_fold_map (interp_induction_arg ist gl) sigma lc in
+          let lc = List.map (interp_induction_arg ist gl) lc in
 	  let sigma,cbo =
             Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
           (sigma,(lc,cbo,
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 96c6da91f..85fcb7e56 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -168,4 +168,3 @@ val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> iden
 val interp_int : interp_sign -> identifier located -> int
 
 val error_ltac_variable : loc -> identifier -> Environ.env option -> value -> string -> 'a
-
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e4abb726..957d2c476 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,6 +59,8 @@ let inj_with_occurrences e = (all_occurrences_expr,e)
 
 let dloc = dummy_loc
 
+let typ_of = Retyping.get_type_of
+
 (* Option for 8.2 compatibility *)
 open Goptions
 let dependent_propositions_elimination = ref true
@@ -75,6 +77,10 @@ let _ =
       optread  = (fun () -> !dependent_propositions_elimination) ;
       optwrite = (fun b -> dependent_propositions_elimination := b) }
 
+let finish_evar_resolution env initial_sigma c =
+  snd (Pretyping.solve_remaining_evars true true solve_by_implicit_tactic
+         env initial_sigma c)
+
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -571,6 +577,19 @@ let dependent_in_decl a (_,c,t) =
 (* Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
+let onOpenInductionArg tac = function
+  | ElimOnConstr cbl ->
+      tac cbl
+  | ElimOnAnonHyp n ->
+      tclTHEN
+        (intros_until_n n)
+        (onLastHyp (fun c -> tac (Evd.empty,(c,NoBindings))))
+  | ElimOnIdent (_,id) ->
+      (* A quantified hypothesis *)
+      tclTHEN
+        (try_intros_until_id_check id)
+        (tac (Evd.empty,(mkVar id,NoBindings)))
+
 let onInductionArg tac = function
   | ElimOnConstr cbl ->
       tac cbl
@@ -580,6 +599,11 @@ let onInductionArg tac = function
       (* A quantified hypothesis *)
       tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings))
 
+let map_induction_arg f = function
+  | ElimOnConstr (sigma,(c,bl)) -> ElimOnConstr (f (sigma,c),bl)
+  | ElimOnAnonHyp n -> ElimOnAnonHyp n
+  | ElimOnIdent id -> ElimOnIdent id
+
 (**************************)
 (*  Refinement tactics    *)
 (**************************)
@@ -1660,13 +1684,46 @@ let letin_tac with_eq name c occs gl =
 (* Implementation without generalisation: abbrev will be lost in hyps in *)
 (* in the extracted proof *)
 
-let letin_abstract id c (occs,check_occs) gl =
+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 = empty_transparent_state;
+  resolve_evars = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = false;
+  frozen_evars =
+    fold_undefined (fun evk _ evars -> ExistentialSet.add evk evars)
+      sigma ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = false;
+  modulo_eta = false;
+  allow_K_in_toplevel_higher_order_unification = false
+}
+
+let make_pattern_test env sigma0 (sigma,c) =
+  let flags = default_matching_flags sigma0 in
+  let matching_fun t =
+    try ignore (w_unify env Reduction.CONV ~flags c t sigma); Some t
+    with _ -> raise NotUnifiable in
+  let merge_fun c1 c2 =
+    match c1, c2 with
+    | Some c1, Some c2 when not (is_fconv Reduction.CONV env sigma0 c1 c2) ->
+        raise NotUnifiable
+    | _ -> c1 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 env sigma0 (sigma,c)
+   | Some c -> c)
+
+let letin_abstract id c (test,out) (occs,check_occs) gl =
   let env = pf_env gl in
   let compute_dependency _ (hyp,_,_ as d) depdecls =
     match occurrences_of_hyp hyp occs with
       | None -> depdecls
       | Some occ ->
-          let newdecl = subst_closed_term_occ_decl occ c d in
+          let newdecl = subst_closed_term_occ_decl_modulo occ test d in
           if occ = (all_occurrences,InHyp) & eq_named_declaration d newdecl then
 	    if check_occs & not (in_every_hyp occs)
 	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
@@ -1676,20 +1733,21 @@ let letin_abstract id c (occs,check_occs) gl =
   let depdecls = fold_named_context compute_dependency env ~init:[] in
   let ccl = match occurrences_of_goal occs with
     | None -> pf_concl gl
-    | Some occ -> subst1 (mkVar id) (subst_closed_term_occ occ c (pf_concl gl))
-  in
+    | Some occ ->
+        subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in
   let lastlhyp =
     if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in
-  (depdecls,lastlhyp,ccl)
+  (depdecls,lastlhyp,ccl,out test)
 
-let letin_tac_gen with_eq name c ty occs gl =
+let letin_tac_gen with_eq name (sigmac,c) test ty occs gl =
   let id =
-    let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
+    let t = match ty with Some t -> t | None -> typ_of (pf_env gl) sigmac c in
+    let x = id_of_name_using_hdchar (Global.env()) t name in
     if name = Anonymous then fresh_id [] x gl else
       if not (mem_named_context x (pf_hyps gl)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared.") in
-  let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in
-  let t = match ty with Some t -> t | None -> pf_type_of gl c in
+  let (depdecls,lastlhyp,ccl,c) = letin_abstract id c test occs gl in
+  let t = match ty with Some t -> t | None -> pf_apply typ_of gl c in
   let newcl,eq_tac = match with_eq with
     | Some (lr,(loc,ido)) ->
       let heq = match ido with
@@ -1713,8 +1771,15 @@ let letin_tac_gen with_eq name c ty occs gl =
       eq_tac;
       tclMAP convert_hyp_no_check depdecls ] gl
 
-let letin_tac with_eq name c ty occs =
-  letin_tac_gen with_eq name c ty (occs,true)
+let make_eq_test c = (make_eq_test c,fun _ -> c)
+
+let letin_tac with_eq name c ty occs gl =
+  letin_tac_gen with_eq name (project gl,c) (make_eq_test c) ty (occs,true) gl
+
+let letin_pat_tac with_eq name c ty occs gl =
+  letin_tac_gen with_eq name c
+    (make_pattern_test (pf_env gl) (project gl) c)
+    ty (occs,true) gl
 
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c gl =
@@ -2393,7 +2458,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	    hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
 	else []
       in
-      let body, c' = if defined then Some c', Retyping.get_type_of ctxenv Evd.empty c' else None, c' in
+      let body, c' = if defined then Some c', typ_of ctxenv Evd.empty c' else None, c' in
 	Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls,
 	     dep, succ (List.length ctx), vars)
     else None
@@ -3002,7 +3067,7 @@ let clear_unselected_context id inhyps cls gl =
 	  thin ids gl
       | None -> tclIDTAC gl
 
-let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
+let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls gl =
   let inhyps = match cls with
   | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
   | _ -> [] in
@@ -3015,14 +3080,17 @@ let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
 	  (induction_with_atomization_of_ind_arg
 	    isrec with_evars elim names (id,lbind) inhyps) gl
     | _        ->
-	let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
+	let x = id_of_name_using_hdchar (Global.env()) (typ_of (pf_env gl) sigma c)
 		  Anonymous in
 	let id = fresh_id [] x gl in
 	(* We need the equality name now *)
 	let with_eq = Option.map (fun eq -> (false,eq)) eqname in
 	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
 	tclTHEN
-	  (letin_tac_gen with_eq (Name id) c None (Option.default allHypsAndConcl cls,false))
+          (* Warning: letin is buggy when c is not of inductive type *)
+	  (letin_tac_gen with_eq (Name id) (sigma,c)
+             (make_pattern_test (pf_env gl) (project gl) (sigma,c))
+             None (Option.default allHypsAndConcl cls,false))
 	  (induction_with_atomization_of_ind_arg
 	     isrec with_evars elim names (id,lbind) inhyps) gl
 
@@ -3079,7 +3147,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
   if List.length lc = 1 && not (is_functional_induction elim gl) then
     (* standard induction *)
-    onInductionArg
+    onOpenInductionArg
       (fun c -> new_induct_gen isrec with_evars elim names c cls)
       (List.hd lc) gl
   else begin
@@ -3091,6 +3159,8 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
       str "Example: induction x1 x2 x3 using my_scheme.");
     if cls <> None then
       error "'in' clause not supported here.";
+    let lc = List.map
+      (map_induction_arg (pf_apply finish_evar_resolution gl)) lc in
     if List.length lc = 1 then
       (* Hook to recover standard induction on non-standard induction schemes *)
       (* will be removable when is_functional_induction will be more clever *)
@@ -3098,8 +3168,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
 	(fun (c,lbind) ->
 	  if lbind <> NoBindings then
 	    error "'with' clause not supported here.";
-	  new_induct_gen_l isrec with_evars elim names [c])
-	(List.hd lc) gl
+	  new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc) gl
     else
       let newlc =
 	List.map (fun x ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a83e494f5..f8f32b792 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -271,7 +271,8 @@ val elim :
 
 val simple_induct : quantified_hypothesis -> tactic
 
-val new_induct : evars_flag -> constr with_bindings induction_arg list ->
+val new_induct : evars_flag -> 
+  (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
     intro_pattern_expr located option * intro_pattern_expr located option ->
       clause option -> tactic
@@ -282,7 +283,8 @@ val general_case_analysis : evars_flag -> constr with_bindings ->  tactic
 val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
-val new_destruct : evars_flag -> constr with_bindings induction_arg list ->
+val new_destruct : evars_flag ->
+  (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
     intro_pattern_expr located option * intro_pattern_expr located option ->
       clause option -> tactic
@@ -290,7 +292,7 @@ val new_destruct : evars_flag -> constr with_bindings induction_arg list ->
 (** {6 Generic case analysis / induction tactics. } *)
 
 val induction_destruct : rec_flag -> evars_flag ->
-  (constr with_bindings induction_arg list *
+  ((evar_map * constr with_bindings) induction_arg list *
   constr with_bindings option *
   (intro_pattern_expr located option * intro_pattern_expr located option))
   list *
@@ -360,6 +362,8 @@ val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic
 val forward   : tactic option -> intro_pattern_expr located option -> constr -> tactic
 val letin_tac : (bool * intro_pattern_expr located) option -> name ->
   constr -> types option -> clause -> tactic
+val letin_pat_tac : (bool * intro_pattern_expr located) option -> name ->
+  evar_map * constr -> types option -> clause -> tactic
 val assert_tac : name -> types -> tactic
 val assert_by  : name -> types -> tactic -> tactic
 val pose_proof : name -> constr -> tactic
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index d796cf748..b24ed2f1b 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -41,3 +41,26 @@ Proof.
   auto.
   auto.
 Qed.
+
+(* Check selection of occurrences by pattern *)
+
+Goal forall x, S x = S (S x).   
+intros.
+induction (S _) in |- * at -2.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1 3.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1.
+now_show (0=S (S x)).
+Undo 2.
+induction (S _) in |- * at 2.
+now_show (S x=0).
+Undo 2.
+induction (S _) in |- * at 3.
+now_show (S x=1).
+Undo 2.
+Fail induction (S _) in |- * at 4.
+Abort.
+
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0a866d3b7..83b63067e 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -77,6 +77,25 @@ let sumbool = Coqlib.build_coq_sumbool
 
 let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
 
+let induct_on c =
+  new_induct false
+    [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+    None (None,None) None
+
+let destruct_on_using c id =
+  new_destruct false
+    [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+    None
+    (None,Some (dl,Genarg.IntroOrAndPattern [
+                                    [dl,Genarg.IntroAnonymous];
+                                    [dl,Genarg.IntroIdentifier id]]))
+    None
+
+let destruct_on c =
+  new_destruct false
+    [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+    None (None,None) None
+
 (* reconstruct the inductive with the correct deBruijn indexes *)
 let mkFullInd ind n =
   let mib = Global.lookup_mind (fst ind) in
@@ -511,17 +530,9 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
       avoid := freshz::(!avoid);
       tclTHENSEQ [ intros_using fresh_first_intros;
                      intro_using freshn ;
-                     new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
-                                        Glob_term.NoBindings))]
-                                None
-                                (None,None)
-		                None;
+                     induct_on (mkVar freshn);
                      intro_using freshm;
-                     new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm),
-                                    Glob_term.NoBindings))]
-                                None
-                                (None,None)
-		                None;
+                     destruct_on (mkVar freshm);
                      intro_using freshz;
                      intros;
                      tclTRY (
@@ -539,7 +550,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                            in
                             avoid := fresht::(!avoid);
                             (new_destruct false [Tacexpr.ElimOnConstr
-                                      ((mkVar freshz,Glob_term.NoBindings))]
+                                      (Evd.empty,((mkVar freshz,Glob_term.NoBindings)))]
                                   None
                                   (None, Some (dl,Genarg.IntroOrAndPattern [[
                                     dl,Genarg.IntroIdentifier fresht;
@@ -649,17 +660,9 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
       avoid := freshz::(!avoid);
       tclTHENSEQ [ intros_using fresh_first_intros;
                      intro_using freshn ;
-                     new_induct false [Tacexpr.ElimOnConstr
-                                    ((mkVar freshn),Glob_term.NoBindings)]
-                                None
-                                (None,None)
-		                None;
+                     induct_on (mkVar freshn);
                      intro_using freshm;
-                     new_destruct false [Tacexpr.ElimOnConstr
-                                    ((mkVar freshm),Glob_term.NoBindings)]
-                                None
-                                (None,None)
-		                None;
+                     destruct_on (mkVar freshm);
                      intro_using freshz;
                      intros;
                      tclTRY (
@@ -808,24 +811,11 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
         assert_by (Name freshH) (
           mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
 	)
-	  (tclTHEN
-	    (new_destruct false [Tacexpr.ElimOnConstr
-              (eqbnm,Glob_term.NoBindings)]
-              None
-              (None,None)
-	      None)
-	    Auto.default_auto);
+	  (tclTHEN (destruct_on eqbnm) Auto.default_auto);
         (fun gsig ->
 	  let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in
           avoid := freshH2::(!avoid);
-	  tclTHENS (
-	    new_destruct false [Tacexpr.ElimOnConstr
-                                    ((mkVar freshH),Glob_term.NoBindings)]
-                                None
-                                (None,Some (dl,Genarg.IntroOrAndPattern [
-                                    [dl,Genarg.IntroAnonymous];
-                                    [dl,Genarg.IntroIdentifier freshH2]])) None
-	  ) [
+	  tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
 	    (* left *)
 	    tclTHENSEQ [
 	      simplest_left;