- Implantation de la suggestion 1873 sur discriminate. Au final,

  discriminate/injection/simplify_eq acceptent maintenant un terme
  comme argument. Les clauses "with" et les variantes "e" sont aussi
  acceptées. Aussi, discriminate sans argument essaie maintenant
  toutes les hyps quantifiées (au lieu de traiter seulement les buts
  t1<>t2).

--This line, and those below, will be ignored--

M    doc/refman/RefMan-tac.tex
M    CHANGES
M    pretyping/evd.ml
M    pretyping/termops.ml
M    pretyping/termops.mli
M    pretyping/clenv.ml
M    tactics/extratactics.ml4
M    tactics/inv.ml
M    tactics/equality.ml
M    tactics/tactics.mli
M    tactics/equality.mli
M    tactics/tacticals.ml
M    tactics/eqdecide.ml4
M    tactics/tacinterp.ml
M    tactics/tactics.ml
M    tactics/extratactics.mli
M    toplevel/auto_ind_decl.ml
M    contrib/funind/invfun.ml
M    test-suite/success/Discriminate.v
M    test-suite/success/Injection.v
M    proofs/clenvtac.mli
M    proofs/clenvtac.ml


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

22 files changed, 409 insertions, 176 deletions

diff --git a/CHANGES b/CHANGES
index 4304fce18..675db3f18 100644
--- a/CHANGES
+++ b/CHANGES
@@ -202,6 +202,9 @@ Tactics
 - Slight improvement of the hnf and simpl tactics when applied on
   expressions with explicit occurrences of match or fix.
 - New tactics "eapply in", "erewrite", "erewrite in".
+- New tactics "ediscriminate", "einjection", "esimplify_eq".
+- Tactics "discriminate", "injection", "simplify_eq" now support any
+  term as argument. Clause "with" is also supported.
 - Unfoldable references can be given by notation's string rather than by name 
   in unfold.
 - The "with" arguments are now typed using informations from the current goal:
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 0160c290f..63d44916b 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -573,9 +573,9 @@ let rec reflexivity_with_destruct_cases g =
 	       match kind_of_term  (pf_type_of g (mkVar id)) with 
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> 
 		     if Equality.discriminable (pf_env g) (project g) t1 t2 
-		     then Equality.discr id g
+		     then Equality.discrHyp id g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite]  g
+		     then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f71d66319..8539136a0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -993,7 +993,7 @@ The proof of {\tt False} is searched in the hypothesis named \ident.
 \tacindex{contradict}
 
 This tactic allows to manipulate negated hypothesis and goals. The
-name \ident\ should correspond to an hypothesis. With 
+name \ident\ should correspond to a hypothesis. With 
 {\tt contradict H}, the current goal and context is transformed in
 the following way: 
 \begin{itemize}
@@ -2395,17 +2395,20 @@ of an inductive datatype. If $G$ is the current goal, it leaves the sub-goals
 of \term$_1$ and \term$_2$ must satisfy the same restrictions as in the tactic
 \texttt{decide equality}.
 
-\subsection{\tt discriminate {\ident}
+\subsection{\tt discriminate {\term}
 \label{discriminate}
-\tacindex{discriminate}}
+\tacindex{discriminate}
+\tacindex{ediscriminate}}
 
-This tactic proves any goal from an absurd hypothesis stating that two
+This tactic proves any goal from an assumption stating that two
 structurally different terms of an inductive set are equal. For
-example, from the hypothesis {\tt (S (S O))=(S O)} we can derive by
-absurdity any proposition.  Let {\ident} be a hypothesis of type
-{\tt{\term$_1$} = {\term$_2$}} in the local context, {\term$_1$} and
+example, from {\tt (S (S O))=(S O)} we can derive by absurdity any
+proposition.
+
+The argument {\term} is assumed to be a proof of a statement
+of conclusion {\tt{\term$_1$} = {\term$_2$}} with {\term$_1$} and
 {\term$_2$} being elements of an inductive set.  To build the proof,
-the tactic traverses the normal forms\footnote{Recall: opaque
+the tactic traverses the normal forms\footnote{Reminder: opaque
   constants will not be expanded by $\delta$ reductions} of
 {\term$_1$} and {\term$_2$} looking for a couple of subterms {\tt u}
 and {\tt w} ({\tt u} subterm of the normal form of {\term$_1$} and
@@ -2414,26 +2417,39 @@ positions and whose head symbols are two different constructors. If
 such a couple of subterms exists, then the proof of the current goal
 is completed, otherwise the tactic fails.
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem The syntax {\tt discriminate {\ident}} can be used to refer to a
+hypothesis quantified in the goal. In this case, the quantified
+hypothesis whose name is {\ident} is first introduced in the local
+context using \texttt{intros until \ident}.
 
 \begin{ErrMsgs}
-\item {\ident} \errindex{Not a discriminable equality} \\
-  occurs when the type of the specified hypothesis is not an equation.
+\item \errindex{No primitive equality found}
+\item \errindex{Not a discriminable equality}
 \end{ErrMsgs}  
 
 \begin{Variants}
-\item \texttt{discriminate} \num\\
-  This does the same thing as \texttt{intros until \num} then
-\texttt{discriminate \ident} where {\ident} is the identifier for the last
-introduced hypothesis.
-\item {\tt discriminate}\\
-  It applies to a goal of the form {\tt
-    \verb=~={\term$_1$}={\term$_2$}} and it is equivalent to: 
-  {\tt unfold not; intro {\ident}}; {\tt discriminate
-    {\ident}}.
+\item \texttt{discriminate} \num
+
+  This does the same thing as \texttt{intros until \num} followed by
+  \texttt{discriminate \ident} where {\ident} is the identifier for
+  the last introduced hypothesis.
+
+\item \texttt{discriminate} {\term} {\tt with} {\bindinglist}
+
+  This does the same thing as \texttt{discriminate {\term}} but using
+the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{ediscriminate} \num\\
+      \texttt{ediscriminate} {\term} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt discriminate} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
+\item \texttt{discriminate}
+
+  This looks for a quantified or not quantified hypothesis {\ident} on
+  which {\tt discriminate {\ident}} is applicable.
 
   \begin{ErrMsgs}
   \item \errindex{No discriminable equalities} \\
@@ -2441,9 +2457,10 @@ introduced hypothesis.
   \end{ErrMsgs}
 \end{Variants}
 
-\subsection{\tt injection {\ident}
+\subsection{\tt injection {\term}
 \label{injection}
-\tacindex{injection}}
+\tacindex{injection}
+\tacindex{einjection}}
 
 The {\tt injection} tactic is based on the fact that constructors of
 inductive sets are injections. That means that if $c$ is a constructor
@@ -2451,10 +2468,11 @@ of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
 terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal
 too.
 
-If {\ident} is an hypothesis of type {\tt {\term$_1$} = {\term$_2$}},
-then {\tt injection} behaves as applying injection as deep as possible to
+If {\term} is a proof of a statement of conclusion
+ {\tt {\term$_1$} = {\term$_2$}},
+then {\tt injection} applies injectivity as deep as possible to
 derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
-placed in the same positions. For example, from the hypothesis {\tt (S
+placed in the same positions. For example, from {\tt (S
   (S n))=(S (S (S m))} we may derive {\tt n=(S m)}.  To use this
 tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
 set and they should be neither explicitly equal, nor structurally
@@ -2462,7 +2480,7 @@ different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
 their respective normal forms, then:
 \begin{itemize}
 \item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal,
-\item there must not exist any couple of subterms {\tt u} and {\tt w},
+\item there must not exist any pair of subterms {\tt u} and {\tt w},
   {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} ,
   placed in the same positions and having different constructors as
   head symbols.
@@ -2501,59 +2519,70 @@ the projection on the second one, and so {\tt injection} will work fine.
 To define such an equality, you have to use the {\tt Scheme} command 
 (see \ref{Scheme}).
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt injection {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
 
 \begin{ErrMsgs}
-\item {\ident} \errindex{is not a projectable equality} 
-  occurs when the type of
-  the hypothesis $id$ does not verify the preconditions.
-\item \errindex{Not an equation} occurs when the type of the
-  hypothesis $id$ is not an equation.
+\item \errindex{Not a projectable equality but a discriminable one}
+\item \errindex{Nothing to do, it is an equality between convertible terms}
+\item \errindex{Not a primitive equality}
 \end{ErrMsgs}
 
 \begin{Variants}
 \item \texttt{injection} \num{}
 
-  This does the same thing as \texttt{intros until \num} then
+  This does the same thing as \texttt{intros until \num} followed by
 \texttt{injection \ident} where {\ident} is the identifier for the last
 introduced hypothesis.
 
-\item{\tt injection}\tacindex{injection} 
+\item \texttt{injection} \term{} {\tt with} {\bindinglist}
+
+  This does the same as \texttt{injection {\term}} but using
+  the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{einjection} \num\\
+      \texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt injection} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
+\item{\tt injection}
   
   If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
-  the tactic computes the head normal form of the goal and then
-  behaves as the sequence: {\tt unfold not; intro {\ident}; injection
-  {\ident}}.
+  this behaves as {\tt intro {\ident}; injection {\ident}}.
   
   \ErrMsg \errindex{goal does not satisfy the expected preconditions}
 
-\item \texttt{injection} \ident{} \texttt{as} \nelist{\intropattern}{}\\
+\item \texttt{injection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
 \texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
 \texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
+\texttt{einjection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
 \tacindex{injection \ldots{} as}
  
-These variants apply \texttt{intros} \nelist{\intropattern}{} after the call to \texttt{injection}.
+These variants apply \texttt{intros} \nelist{\intropattern}{} after
+the call to \texttt{injection} or \texttt{einjection}.
 
 \end{Variants}
 
-\subsection{\tt simplify\_eq {\ident}
+\subsection{\tt simplify\_eq {\term}
 \tacindex{simplify\_eq}
+\tacindex{esimplify\_eq}
 \label{simplify-eq}}
 
-Let {\ident} be the name of an hypothesis of type {\tt
-  {\term$_1$}={\term$_2$}} in the local context. If {\term$_1$} and
+Let {\term} be the proof of a statement of conclusion {\tt
+  {\term$_1$}={\term$_2$}}. If {\term$_1$} and
 {\term$_2$} are structurally different (in the sense described for the
 tactic {\tt discriminate}), then the tactic {\tt simplify\_eq} behaves as {\tt
-  discriminate {\ident}} otherwise it behaves as {\tt injection
-  {\ident}}.
+  discriminate {\term}}, otherwise it behaves as {\tt injection
+  {\term}}.
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt simplify\_eq {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
 
 \begin{Variants}
 \item \texttt{simplify\_eq} \num
@@ -2561,9 +2590,23 @@ latter is first introduced in the local context using
   This does the same thing as \texttt{intros until \num} then
 \texttt{simplify\_eq \ident} where {\ident} is the identifier for the last
 introduced hypothesis.
+
+\item \texttt{simplify\_eq} \term{} {\tt with} {\bindinglist}
+
+  This does the same as \texttt{simplify\_eq {\term}} but using
+  the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{esimplify\_eq} \num\\
+      \texttt{esimplify\_eq} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt simplify\_eq} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
 \item{\tt simplify\_eq}
-If the current goal has form $\verb=~=t_1=t_2$, then this tactic does 
-\texttt{hnf; intro {\ident}; simplify\_eq {\ident}}.
+
+If the current goal has form $t_1\verb=<>=t_2$, it behaves as
+\texttt{intro {\ident}; simplify\_eq {\ident}}.
 \end{Variants}
 
 \subsection{\tt dependent rewrite -> {\ident}
@@ -2599,8 +2642,8 @@ constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary
 conditions that should hold for the instance $(I~\vec{t})$ to be
 proved by $c_i$.
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
+\Rem If {\ident} does not denote a hypothesis in the local context
+but refers to a hypothesis quantified in the goal, then the
 latter is first introduced in the local context using
 \texttt{intros until \ident}.
 
@@ -3242,7 +3285,7 @@ equalities with uninterpreted symbols. It also include the constructor theory
 (see \ref{injection} and \ref{discriminate}).
 If the goal is a non-quantified equality, {\tt congruence} tries to
 prove it with non-quantified equalities in the context. Otherwise it
-tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis.
+tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.
 
 {\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. 
 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 074dd0901..c91580044 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -222,13 +222,24 @@ let dependent_metas clenv mvs conclmetas =
        Metaset.union deps (clenv_metavars clenv.evd mv))
     mvs conclmetas
 
+let duplicated_metas c = 
+  let rec collrec (one,more as acc) c =
+    match kind_of_term c with
+    | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more)
+    | _       -> fold_constr collrec acc c
+  in
+  snd (collrec ([],[]) c)
+
 let clenv_dependent hyps_only clenv =
   let mvs = undefined_metas clenv.evd in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = dependent_metas clenv mvs ctyp_mvs in
+  let nonlinear = duplicated_metas (clenv_value clenv) in
+  (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
-    (fun mv -> Metaset.mem mv deps &&
-               not (hyps_only && Metaset.mem mv ctyp_mvs))
+    (fun mv -> (Metaset.mem mv deps &&
+                not (hyps_only && Metaset.mem mv ctyp_mvs))
+               or List.mem mv nonlinear) 
     mvs
 
 let clenv_missing ce = clenv_dependent true ce
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 660547b5c..166114ab6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -643,6 +643,20 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (**********************************************************)
 (* Pretty-printing *)
 
+let pr_instance_status (sc,typ) =
+  begin match sc with
+  | IsSubType -> str " [or a subtype of it]"
+  | IsSuperType -> str " [or a supertype of it]"
+  | ConvUpToEta 0 -> mt ()
+  | UserGiven -> mt ()
+  | ConvUpToEta n -> str" [or an eta-expansion up to " ++ int n ++ str" of it]"
+  end ++
+  begin match typ with
+  | CoerceToType -> str " [up to coercion]"
+  | TypeNotProcessed -> mt ()
+  | TypeProcessed -> str " [type is checked]"
+  end
+
 let pr_meta_map mmap =
   let pr_name = function
       Name id -> str"[" ++ pr_id id ++ str"]"
@@ -652,10 +666,10 @@ let pr_meta_map mmap =
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
            print_constr b.rebus ++ fnl ())
-    | (mv,Clval(na,(b,_),_)) ->
+    | (mv,Clval(na,(b,s),_)) ->
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
-           print_constr b.rebus ++ fnl ())
+           print_constr b.rebus ++ spc () ++ pr_instance_status s ++ fnl ())
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 73c03097a..4246f0daa 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -275,6 +275,11 @@ let rec strip_head_cast c = match kind_of_term c with
   | Cast (c,_,_) -> strip_head_cast c
   | _ -> c
 
+(* Get the last arg of an application *)
+let last_arg c = match kind_of_term c with
+  | App (f,cl) -> array_last cl
+  | _ -> anomaly "last_arg"
+
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
    subterms of [c]; it carries an extra data [l] (typically a name
    list) which is processed by [g na] (which typically cons [na] to
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f80deab10..539951d5c 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -185,6 +185,9 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
 val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
 val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
 
+(* Get the last arg of a constr intended to be nn application *)
+val last_arg : constr -> constr
+
 (* name contexts *)
 type names_context = name list
 val add_name : name -> names_context -> names_context
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 22dcca289..624b671d3 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -60,6 +60,9 @@ let clenv_cast_meta clenv =
   in 
   crec
 
+let clenv_value_cast_meta clenv =
+    clenv_cast_meta clenv (clenv_value clenv)
+
 let clenv_pose_dependent_evars with_evars clenv =
   let dep_mvs = clenv_dependent false clenv in
   if dep_mvs <> [] & not with_evars then
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 0cf0a5545..4dd59fcf6 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -27,6 +27,7 @@ val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_value_cast_meta : clausenv -> constr
 
 (* Compatibility, use res_pf ?with_evars:true instead *)
 val e_res_pf : clausenv -> tactic
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 8aef9c50b..61100f0a5 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -75,7 +75,7 @@ let mkBranches c1 c2 =
 let solveNoteqBranch side = 
   tclTHEN (choose_noteq side)
     (tclTHEN (intro_force true)
-      (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id))))
+      (onLastHyp (fun id -> Extratactics.h_discrHyp id)))
 
 let h_solveNoteqBranch side =
   Refiner.abstract_extended_tactic "solveNoteqBranch" [] 
@@ -115,7 +115,7 @@ let diseqCase eqonleft =
   (tclTHEN  red_in_concl
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (h_simplest_apply (mkVar diseq))
-  (tclTHEN  (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
+  (tclTHEN  (Extratactics.h_injHyp absurd)
             (full_trivial [])))))))
 
 let solveArg eqonleft op a1 a2 tac g = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f907b1fd7..3bfc719e2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,6 +40,9 @@ open Vernacexpr
 open Setoid_replace
 open Declarations
 open Indrec
+open Printer
+open Clenv
+open Clenvtac
 
 (* Rewriting tactics *)
 
@@ -550,66 +553,84 @@ exception NotDiscriminable
 
 let eq_baseid = id_of_string "e"
 
-let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort =
+let apply_on_clause (f,t) clause =
+  let sigma = Evd.evars_of clause.evd in
+  let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
+  let argmv = 
+    (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
+     | Meta mv -> mv
+     | _  -> errorlabstrm "" (str "Ill-formed clause applicator")) in
+  clenv_fchain argmv f_clause clause
+
+let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
+  let eqn = mkApp(lbeq.eq,[|t;t1;t2|]) in
   let discriminator =
     build_discriminator sigma e_env dirn (mkVar e) sort cpath in
   let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
-  tclCOMPLETE 
-    ((tclTHENS (cut_intro absurd_term)
-      [onLastHyp gen_absurdity; 
-       refine (mkApp (pf,[|mkVar id|]))]))
+  let pf_ty = mkArrow eqn absurd_term in
+  let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
+  tclTHENS (cut_intro absurd_term)
+    [onLastHyp gen_absurdity; res_pf absurd_clause]
 
-let discrEq (lbeq,(t,t1,t2) as u) id gls =
-  let sigma = project gls in
+let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
+  let sigma = Evd.evars_of eq_clause.evd in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inr _ ->
-	errorlabstrm "discr" (str" Not a discriminable equality")
+	errorlabstrm "discr" (str"Not a discriminable equality")
     | Inl (cpath, (_,dirn), _) ->
 	let sort = pf_apply get_type_of gls (pf_concl gls) in 
-	discr_positions env sigma u id cpath dirn sort gls
-
-let onEquality tac id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+	discr_positions env sigma u eq_clause cpath dirn sort gls
+
+let onEquality with_evars tac (c,lbindc) gls =
+  let t = pf_type_of gls c in
+  let t' = try snd (pf_reduce_to_quantified_ind gls t) with UserError _ -> t in
+  let eq_clause = make_clenv_binding gls (c,t') lbindc in
+  let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
+  let eqn = clenv_type eq_clause' in
   let eq =
     try find_eq_data_decompose eqn
     with PatternMatchingFailure ->
-      errorlabstrm "" (pr_id id ++ str": not a primitive equality") 
-  in tac eq id gls
+      errorlabstrm "" (str"No primitive equality found") in
+  tclTHEN
+    (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) 
+    (tac eq eq_clause') gls
 
-let onNegatedEquality tac gls =
+let onNegatedEquality with_evars tac gls =
   let ccl = pf_concl gls in
-  let eq =
-    try match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
-      | Prod (_,t,u) when is_empty_type u ->
-          find_eq_data_decompose (pf_whd_betadeltaiota gls t)
-      | _ -> raise PatternMatchingFailure
-    with PatternMatchingFailure ->
+  match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
+  | Prod (_,t,u) when is_empty_type u ->
+      tclTHEN introf
+        (onLastHyp (fun id -> 
+          onEquality with_evars tac (mkVar id,NoBindings))) gls
+  | _ -> 
       errorlabstrm "" (str "Not a negated primitive equality")
-  in tclTHEN introf (onLastHyp (tac eq)) gls
 
-let discrSimpleClause = function
-  | None -> onNegatedEquality discrEq
-  | Some ((_,id),_) -> onEquality discrEq id
+let discrSimpleClause with_evars = function
+  | None -> onNegatedEquality with_evars discrEq
+  | Some ((_,id),_) -> onEquality with_evars discrEq (mkVar id,NoBindings)
 
-let discr = onEquality discrEq
+let discr with_evars = onEquality with_evars discrEq
 
-let discrClause = onClauses discrSimpleClause
+let discrClause with_evars = onClauses (discrSimpleClause with_evars)
 
-let discrEverywhere = 
+let discrEverywhere with_evars = 
   tclORELSE
-    (Tacticals.tryAllClauses discrSimpleClause)
+    (tclTHEN
+      (tclREPEAT introf) 
+      (Tacticals.tryAllHyps
+        (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
     (fun gls -> 
        errorlabstrm "DiscrEverywhere" (str"No discriminable equalities"))
 
-let discr_tac = function
-  | None -> discrEverywhere
-  | Some id -> try_intros_until discr id
+let discr_tac with_evars = function
+  | None -> discrEverywhere with_evars
+  | Some c -> onInductionArg (discr with_evars) c
 
-let discrConcl gls  = discrClause onConcl gls
-let discrHyp id gls = discrClause (onHyp id) gls
+let discrConcl gls  = discrClause false onConcl gls
+let discrHyp id gls = discrClause false (onHyp id) gls
 
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
@@ -828,7 +849,7 @@ let simplify_args env sigma t =
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
     | _ -> t
 
-let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
+let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
   let injectors =
@@ -837,9 +858,12 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
         (* arbitrarily take t1' as the injector default value *)
 	let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
 	let injfun = mkNamedLambda e t injbody in
-	let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in
-	let ty = simplify_args env sigma (get_type_of env sigma pf) in
-	  (pf,ty))
+	let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in
+	let pf_typ = get_type_of env sigma pf in
+	let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
+        let pf = clenv_value_cast_meta inj_clause in
+	let ty = simplify_args env sigma (clenv_type inj_clause) in
+	(pf,ty))
       posns in
   if injectors = [] then
     errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
@@ -850,14 +874,13 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
 exception Not_dep_pair
 
 
-let injEq ipats (eq,(t,t1,t2)) id gls =
-  let sigma = project gls in
-  let env = pf_env gls in
+let injEq ipats (eq,(t,t1,t2)) eq_clause =
+  let sigma = Evd.evars_of eq_clause.evd in
+  let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
     | Inl _ ->
 	errorlabstrm "Inj"
-	  (str (string_of_id id) ++
-	    str" is not a projectable equality but a discriminable one")
+	  (str"Not a projectable equality but a discriminable one")
     | Inr [] ->
 	errorlabstrm "Equality.inj" 
 	   (str"Nothing to do, it is an equality between convertible terms")
@@ -895,45 +918,44 @@ let injEq ipats (eq,(t,t1,t2)) id gls =
                         [|ar1.(0);Ind_tables.find_eq_dec_proof ind;
                           ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
                   )) (Auto.trivial [] [])
-                ] gls
+                ]
 (* not a dep eq or no decidable type found *)
             ) else (raise Not_dep_pair) 
-        ) with _ -> (
-	tclTHEN 
-	  (inject_at_positions env sigma (eq,(t,t1,t2)) id posns)
+        ) with _ ->
+	tclTHEN
+	  (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns)
 	  (intros_pattern None ipats)
-	  gls
-        )
 
-let inj ipats = onEquality (injEq ipats)
+let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
-let injClause ipats = function
-  | None -> onNegatedEquality (injEq ipats)
-  | Some id -> try_intros_until (inj ipats) id
+let injClause ipats with_evars = function
+  | None -> onNegatedEquality with_evars (injEq ipats)
+  | Some c -> onInductionArg (inj ipats with_evars) c
 
-let injConcl gls  = injClause [] None gls
-let injHyp id gls = injClause [] (Some id) gls
+let injConcl gls  = injClause [] false None gls
+let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
 
-let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls =
+let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in 
-  let sigma = project gls in
+  let sigma = Evd.evars_of clause.evd in
   let env = pf_env gls in 
   match find_positions env sigma t1 t2 with
     | Inl (cpath, (_,dirn), _) ->
-	discr_positions env sigma u id cpath dirn sort gls
+	discr_positions env sigma u clause cpath dirn sort gls
     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
         ntac 0 gls
     | Inr posns ->
 	tclTHEN
-	  (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns))
+	  (inject_at_positions env sigma (lbeq,(t,t1,t2)) clause
+	    (List.rev posns))
 	  (ntac (List.length posns))
 	  gls
 
-let dEqThen ntac = function
-  | None -> onNegatedEquality (decompEqThen ntac)
-  | Some id -> try_intros_until (onEquality (decompEqThen ntac)) id
+let dEqThen with_evars ntac = function
+  | None -> onNegatedEquality with_evars (decompEqThen ntac)
+  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
 
-let dEq = dEqThen (fun x -> tclIDTAC)
+let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
 
 let rewrite_msg = function 
   | None -> str "passed term is not a primitive equality" 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index acbaca235..3c7f9c6b0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -67,18 +67,22 @@ val replace_in : identifier -> constr -> constr -> tactic
 val replace_by : constr -> constr -> tactic -> tactic
 val replace_in_by : identifier -> constr -> constr -> tactic -> tactic
 
-val discr        : identifier -> tactic
+val discr        : evars_flag -> constr with_ebindings -> tactic
 val discrConcl   : tactic
-val discrClause  : clause -> tactic
+val discrClause  : evars_flag -> clause -> tactic
 val discrHyp     : identifier -> tactic
-val discrEverywhere     : tactic
-val discr_tac    : quantified_hypothesis option -> tactic
-val inj          : intro_pattern_expr list -> identifier -> tactic
-val injClause    : intro_pattern_expr list -> quantified_hypothesis option ->
-                   tactic
-
-val dEq : quantified_hypothesis option -> tactic
-val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic
+val discrEverywhere : evars_flag -> tactic
+val discr_tac    : evars_flag -> 
+  constr with_ebindings induction_arg option -> tactic
+val inj          : intro_pattern_expr list -> evars_flag ->
+  constr with_ebindings -> tactic
+val injClause    : intro_pattern_expr list -> evars_flag -> 
+  constr with_ebindings induction_arg option -> tactic
+val injHyp       : identifier -> tactic
+val injConcl     : tactic
+
+val dEq : evars_flag -> constr with_ebindings induction_arg option -> tactic
+val dEqThen : evars_flag -> (int -> tactic) -> constr with_ebindings induction_arg option -> tactic
 
 val make_iterated_tuple : 
   env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index dd716024d..5d374215d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -16,6 +16,8 @@ open Genarg
 open Extraargs
 open Mod_subst
 open Names
+open Tacexpr
+open Rawterm
 
 (* Equality *)
 open Equality
@@ -41,25 +43,93 @@ TACTIC EXTEND replace_term
   -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ]
 END
 
+let induction_arg_of_quantified_hyp = function
+  | AnonHyp n -> ElimOnAnonHyp n
+  | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id)
+
+(* Versions *_main must come first!! so that "1" is interpreted as a
+   ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
+   ElimOnIdent and not as "constr" *)
+
+TACTIC EXTEND simplify_eq_main
+| [ "simplify_eq" constr_with_bindings(c) ] ->
+    [ dEq false (Some (ElimOnConstr c)) ]
+END
 TACTIC EXTEND simplify_eq
-  [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
+  [ "simplify_eq" ] -> [ dEq false None ]
+| [ "simplify_eq" quantified_hypothesis(h) ] ->
+    [ dEq false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND esimplify_eq_main
+| [ "esimplify_eq" constr_with_bindings(c) ] ->
+    [ dEq true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND esimplify_eq
+| [ "esimplify_eq" ] -> [ dEq true None ]
+| [ "esimplify_eq" quantified_hypothesis(h) ] ->
+    [ dEq true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
+TACTIC EXTEND discriminate_main
+| [ "discriminate" constr_with_bindings(c) ] ->
+    [ discr_tac false (Some (ElimOnConstr c)) ]
+END
 TACTIC EXTEND discriminate
-  [ "discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ]
+| [ "discriminate" ] -> [ discr_tac false None ]
+| [ "discriminate" quantified_hypothesis(h) ] ->
+    [ discr_tac false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND ediscriminate_main
+| [ "ediscriminate" constr_with_bindings(c) ] ->
+    [ discr_tac true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND ediscriminate
+| [ "ediscriminate" ] -> [ discr_tac true None ]
+| [ "ediscriminate" quantified_hypothesis(h) ] ->
+    [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-let h_discrHyp id = h_discriminate (Some id)
+let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings)
 
+TACTIC EXTEND injection_main
+| [ "injection" constr_with_bindings(c) ] ->
+    [ injClause [] false (Some (ElimOnConstr c)) ]
+END 
 TACTIC EXTEND injection
-  [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause [] h ]
+| [ "injection" ] -> [ injClause [] false None ]
+| [ "injection" quantified_hypothesis(h) ] -> 
+    [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND einjection_main
+| [ "einjection" constr_with_bindings(c) ] ->
+    [ injClause [] true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND einjection
+| [ "einjection" ] -> [ injClause [] true None ]
+| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ]
+END 
+TACTIC EXTEND injection_as_main
+| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat false (Some (ElimOnConstr c)) ]
 END 
 TACTIC EXTEND injection_as
-  [ "injection" quantified_hypothesis_opt(h) 
-    "as" simple_intropattern_list(ipat)] -> [ injClause ipat h ]
+| [ "injection" "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat false None ]
+| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+    [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ]
+END 
+TACTIC EXTEND einjection_as_main
+| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat true (Some (ElimOnConstr c)) ]
+END 
+TACTIC EXTEND einjection_as
+| [ "einjection" "as" simple_intropattern_list(ipat)] ->
+    [ injClause ipat true None ]
+| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+    [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-let h_injHyp id = h_injection (Some id)
+let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
 
 TACTIC EXTEND conditional_rewrite
 | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 341716c01..7a5314c36 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -9,10 +9,9 @@
 (*i $Id$ i*)
 
 open Proof_type
-open Rawterm
 
-val h_discrHyp : quantified_hypothesis -> tactic
-val h_injHyp : quantified_hypothesis -> tactic
+val h_discrHyp : Names.identifier -> tactic
+val h_injHyp : Names.identifier -> tactic
 
 val refine_tac : Evd.open_constr -> tactic
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a77a97906..a25fa285b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -331,7 +331,7 @@ let projectAndApply thin id eqname names depids gls =
   substHypIfVariable
     (* If no immediate variable in the equation, try to decompose it *)
     (* and apply a trailer which again try to substitute *)
-    (fun id -> dEqThen (deq_trailer id) (Some (NamedHyp id)))
+    (fun id -> dEqThen false (deq_trailer id) (Some (ElimOnIdent (dummy_loc,id))))
     id
     gls
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 876f13c33..897c8fd98 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1150,7 +1150,7 @@ let debugging_exception_step ist signal_anomaly e pp =
 let error_ltac_variable loc id env v s =
    user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ 
    str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ 
-   str "which cannot be coerced to " ++ str s)
+   strbrk "which cannot be coerced to " ++ str s)
 
 exception CannotCoerceTo of string
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 577ef0c6f..3d5fd753e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -325,10 +325,6 @@ let elimination_sort_of_hyp id gl =
 (* Find the right elimination suffix corresponding to the sort of the goal *)
 (* c should be of type A1->.. An->B with B an inductive definition *)
 
-let last_arg c = match kind_of_term c with
-  | App (f,cl) -> array_last cl
-  | _ -> anomaly "last_arg"
-
 let general_elim_then_using mk_elim 
   isrec allnames tac predicate (indbindings,elimbindings) 
   ind indclause gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25e920976..c8f92b60f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -469,6 +469,21 @@ let rec intros_rmove = function
  		    move_to_rhyp destopt;
 		    intros_rmove rest ]
 
+(* Apply a tactic on a quantified hypothesis, an hypothesis in context
+   or a term with bindings *)
+
+let onInductionArg tac = function
+  | ElimOnConstr (c,lbindc as cbl) -> 
+      if isVar c & lbindc = NoBindings then 
+	tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl)
+      else
+	tac cbl
+  | ElimOnAnonHyp n ->
+      tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> tac (c,NoBindings)))
+  | ElimOnIdent (_,id) ->
+      (*Identifier apart because id can be quantified in goal and not typable*)
+      tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings))
+
 (**************************)
 (*  Refinement tactics    *)
 (**************************)
@@ -2531,7 +2546,6 @@ let induct_destruct_l isrec with_evars lc elim names cls =
       "'in' clause not supported when several induction hypothesis are given";
   new_induct_gen_l isrec with_evars elim names newlc
 
-
 (* Induction either over a term, over a quantified premisse, or over
    several quantified premisses (like with functional induction
    principles). 
@@ -2540,19 +2554,10 @@ let induct_destruct_l isrec with_evars lc elim names cls =
 let induct_destruct isrec with_evars lc elim names cls =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
   if List.length lc = 1 then (* induction on one arg: use old mechanism *)
-    try 
-      let c = List.hd lc in
-      match c with
-	| ElimOnConstr c -> new_induct_gen isrec with_evars elim names c cls
-	| ElimOnAnonHyp n ->
-	    tclTHEN (intros_until_n n)
-	      (tclLAST_HYP (fun c -> 
-		new_induct_gen isrec with_evars elim names (c,NoBindings) cls))
-	      (* Identifier apart because id can be quantified in goal and not typable *)
-	| ElimOnIdent (_,id) ->
-	    tclTHEN (tclTRY (intros_until_id id))
-	      (new_induct_gen isrec with_evars elim names
-		(mkVar id,NoBindings) cls)
+    try
+      onInductionArg
+	(fun c -> new_induct_gen isrec with_evars elim names c cls)
+	(List.hd lc)
     with (* If this fails, try with new mechanism but if it fails too,
 	    then the exception is the first one. *)
       | x ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0492e296f..700c25f6e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -101,6 +101,13 @@ val intros_clearing      : bool list -> tactic
 val try_intros_until :
   (identifier -> tactic) -> quantified_hypothesis -> tactic
 
+(* Apply a tactic on a quantified hypothesis, an hypothesis in context
+   or a term with bindings *)
+
+val onInductionArg : 
+  (constr with_ebindings -> tactic) ->
+    constr with_ebindings induction_arg -> tactic
+
 (*s Introduction tactics with eliminations. *)
 
 val intro_pattern     : identifier option -> intro_pattern_expr      -> tactic
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index f28c83deb..b57c54781 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -9,3 +9,26 @@ Qed.
 Lemma l2 : forall H : 0 = 1, H = H.   
  discriminate H.
 Qed.
+
+(* Check the variants of discriminate *)
+
+Goal O = S O -> True.
+discriminate 1.
+Undo.
+intros.
+discriminate H.
+Undo.
+Ltac g x := discriminate x.
+g H.
+Abort.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+try discriminate (H O) || exact I.
+Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+ediscriminate (H O).
+instantiate (1:=O).
+Abort.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 606e884ae..867d73746 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -43,6 +43,29 @@ intros; injection H as Hyt Hxz.
 exact Hxz.
 Qed.
 
+(* Check the variants of injection *)
+
+Goal forall x y, S x = S y -> True.
+injection 1 as H'.
+Undo.
+intros.
+injection H as H'.
+Undo.
+Ltac f x := injection x.
+f H.
+Abort.
+
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+try injection (H O) || exact I.
+Qed.
+
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+einjection (H O).
+instantiate (1:=O).
+Abort.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
@@ -53,7 +76,7 @@ Abort.
 
 *)
 
-(* Accept does not project on discriminable positions... allow it?
+(* Injection does not project on discriminable positions... allow it?
 
 Goal 1=2 -> 1=0.
 intro H.
@@ -61,4 +84,4 @@ injection H.
 intro; assumption.
 Qed.
 
- *)
+*)
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0ef835689..9192db722 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -525,7 +525,7 @@ let compute_bl_tact ind lnamesparrec nparrec  =
                      intro_using freshz;
                      intros;
                      tclTRY ( 
-                      tclORELSE reflexivity (Equality.discr_tac None)
+                      tclORELSE reflexivity (Equality.discr_tac false None)
                      );
                      simpl_in_hyp
 		       ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
@@ -643,9 +643,10 @@ let compute_lb_tact ind lnamesparrec nparrec =
                      intro_using freshz;
                      intros;
                      tclTRY ( 
-                      tclORELSE reflexivity (Equality.discr_tac None)
+                      tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Equality.inj [] freshz; intros; simpl_in_concl;
+                     Equality.inj [] false (mkVar freshz,Rawterm.NoBindings);
+		     intros; simpl_in_concl;
                      Auto.default_auto;
                      tclREPEAT (
                       tclTHENSEQ [apply (andb_true_intro());
@@ -806,6 +807,6 @@ let compute_dec_tact ind lnamesparrec nparrec =
                                 Rawterm.NoBindings
                               )
                               true);
-        Pfedit.by (Equality.discr_tac None)
+        Pfedit.by (Equality.discr_tac false None)