Revising r16550 about providing intro patterns for applying injection:

- Introduction of a specific notation for injection intropatterns: [= pats]
- Use of this specific pattern also to apply discriminate on the fly

Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).

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

14 files changed, 144 insertions, 102 deletions

diff --git a/CHANGES b/CHANGES
index 8cea62915b..0cb2b7bdf0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -49,8 +49,10 @@ Tactics
 - Now "appcontext" and "context" behave the same. The old buggy behaviour of
   "context" can be retrieved at parse time by setting the
   "Tactic Compat Context" flag. (possible source of incompatibilities).
-- Introduction patterns of the form [x1 .. xn] or (x1,..,xn) now apply
-  "injection" when used on an equality statement ("ssreflect" style).
+- New introduction pattern [= x1 .. xn] applies "injection as [x1 .. xn]"
+  on the fly if next hypothesis to introduce is an injectible equality
+  (idea borrowed from Georges Gonthier). Introduction pattern [=] applies
+  "discriminate" if a discriminable equality.
 - Tactic "injection c as ipats" now clears c if c refers to an
   hypothesis and moves the resulting equations in the hypotheses
   independently of the number of ipats, which has itself to be less
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2382175601..9aa53eb2be 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -776,11 +776,12 @@ either:
   \item the pattern \texttt{?\ident}
   \item an identifier
   \end{itemize}
-\item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
+\item a {\em composite introduction pattern}, i.e. either one of:
   \begin{itemize}
   \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
   \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)}
+  \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
   \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)}
    for sequence of right-associative binary constructs
   \end{itemize}
@@ -822,14 +823,17 @@ introduction pattern~$p$:
   of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
   $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
   $p_n$]});
-\item as a special case, if the product is over an equality type, then
-  a pattern of the form {\tt [$p_{1}$ \dots\ $p_n$]} or of the form
-  {\tt ($p_1$, \ldots, $p_n$)} applies {\tt injection} instead of {\tt
-    destruct} on the hypothesis and use the patterns $p_1$, \ldots,
-  $p_n$ on the hypotheses generated by {\tt injection} (see
-  Section~\ref{injection}); if the number of patterns is smaller than
-  the number of hypotheses generated, the pattern \texttt{?} is used
-  to complete the list;
+\item if the product is over an equality type, then a pattern of the
+  form {\tt [=$p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
+  (see Section~\ref{injection}) or {\tt discriminate} (see
+  Section~\ref{discriminate}) instead of {\tt destruct}; if {\tt
+    injection} is applicable, the patterns $p_1$, \ldots, $p_n$ are
+  used on the hypotheses generated by {\tt injection}; if the number
+  of patterns is smaller than the number of hypotheses generated, the
+  pattern \texttt{?} is used to complete the list;
+  %TODO!
+  %if {\tt discriminate} is applicable, the list of patterns $p_{1}$
+  %\dots\ $p_n$ is supposed to be empty;
 \item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)}
   is a shortcut for introduction via
   {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 4b4f225455..b1150d6c04 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -65,7 +65,8 @@ let mlexpr_of_intro_pattern = function
   | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
   | Misctypes.IntroIdentifier id ->
       <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
-  | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ ->
+  | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _
+  | Misctypes.IntroInjection _ ->
       failwith "mlexpr_of_intro_pattern: TODO"
 
 let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 164fd60c9e..7d9599032b 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -18,6 +18,7 @@ type patvar = Id.t
 
 type intro_pattern_expr =
   | IntroOrAndPattern of or_and_intro_pattern_expr
+  | IntroInjection of (Loc.t * intro_pattern_expr) list
   | IntroWildcard
   | IntroRewrite of bool
   | IntroIdentifier of Id.t
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5c0996c944..13e422b54f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -285,7 +285,9 @@ GEXTEND Gram
 	  let rec pairify = function
 	    | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
 	    | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]]
-	  in !@loc,pairify (si::tc) ] ]
+	  in !@loc,pairify (si::tc)
+      | "[="; tc = intropatterns; "]" -> !@loc,IntroInjection tc
+ ] ]
   ;
   naming_intropattern:
     [ [ prefix = pattern_ident -> !@loc, IntroFresh prefix
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 264deeb051..2639e2e720 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -29,6 +29,8 @@ let smartmap_cast_type f c =
 
 let rec pr_intro_pattern (_,pat) = match pat with
   | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
+  | IntroInjection pl ->
+      str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
   | IntroWildcard -> str "_"
   | IntroRewrite true -> str "->"
   | IntroRewrite false -> str "<-"
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 842ce67a0d..20e7f2b2ce 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1134,7 +1134,38 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
 
-let injEq_then tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
+  (* fetch the informations of the  pair *)
+  let ceq = constr_of_global Coqlib.glob_eq in
+  let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
+  let eqTypeDest = fst (destApp t) in
+  let _,ar1 = destApp t1 and
+      _,ar2 = destApp t2 in
+  let ind = destInd ar1.(0) in
+  (* check whether the equality deals with dep pairs or not *)
+  (* if yes, check if the user has declared the dec principle *)
+  (* and compare the fst arguments of the dep pair *)
+  let new_eq_args = [|type_of env sigma ar1.(3);ar1.(3);ar2.(3)|] in
+  if (eq_constr eqTypeDest (sigTconstr())) &&
+    (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind) &&
+    (is_conv env sigma ar1.(2) ar2.(2))
+  then begin
+    Library.require_library [Loc.ghost,eqdep_dec] (Some false);
+    let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
+      ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+      (* cut with the good equality and prove the requested goal *)
+    tclTHENS (cut (mkApp (ceq,new_eq_args)))
+      [tclIDTAC; tclTHEN (apply (
+        mkApp(inj2,
+              [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
+                ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
+       )) (Auto.trivial [] [])
+      ]
+  (* not a dep eq or no decidable type found *)
+  end
+  else raise Not_dep_pair
+
+let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
@@ -1147,64 +1178,32 @@ let injEq_then tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
     | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
         errorlabstrm "Equality.inj" (str"Nothing to inject.")
     | Inr posns ->
-(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
-	let t1 = try_delta_expand env sigma t1 in
-	let t2 = try_delta_expand env sigma t2 in
-*)
-      try
-(* fetch the informations of the  pair *)
-        let ceq = constr_of_global Coqlib.glob_eq in
-        let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
-        let eqTypeDest = fst (destApp t) in
-        let _,ar1 = destApp t1 and
-            _,ar2 = destApp t2 in
-        let ind = destInd ar1.(0) in
-(* check whether the equality deals with dep pairs or not *)
-(* if yes, check if the user has declared the dec principle *)
-(* and compare the fst arguments of the dep pair *)
-        let new_eq_args = [|type_of env sigma ar1.(3);ar1.(3);ar2.(3)|] in
-        if (eq_constr eqTypeDest (sigTconstr())) &&
-           (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind) &&
-           (is_conv env sigma ar1.(2) ar2.(2))
-        then begin
-          Library.require_library [Loc.ghost,eqdep_dec] (Some false);
-          let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
-            ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
-          (* cut with the good equality and prove the requested goal *)
-          tclTHENS (cut (mkApp (ceq,new_eq_args)) )
-            [tclIDTAC; tclTHEN (apply (
-              mkApp(inj2,
-                    [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
-                      ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
-             )) (Auto.trivial [] [])
-            ]
-        (* not a dep eq or no decidable type found *)
-        end
-        else raise Not_dep_pair
-      with e when Errors.noncritical e ->
-	inject_at_positions env sigma l2r u eq_clause posns
+        try inject_if_homogenous_dependent_pair env sigma u
+        with e when (Errors.noncritical e || e = Not_dep_pair) ->
+        inject_at_positions env sigma l2r u eq_clause posns
           (tac (clenv_value eq_clause))
 
+let postInjEqTac ipats c n =
+  match ipats with
+  | Some ipats ->
+      let clear_tac =
+        if use_injection_pattern_l2r_order () && isVar c
+        then tclTRY (clear [destVar c])
+        else tclIDTAC in
+      let ipats =
+        if use_injection_pattern_l2r_order ()
+        then adjust_intro_patterns n ipats
+        else ipats in
+      tclTHEN
+        (clear_tac)
+        (intros_pattern MoveLast ipats)
+  | None -> tclIDTAC
+
 let injEq ipats =
   let l2r =
     if use_injection_pattern_l2r_order () & ipats <> None then true else false
   in
-  injEq_then
-    (fun c n -> match ipats with
-      | Some ipats ->
-          let clear_tac =
-            if use_injection_pattern_l2r_order () && isVar c
-            then tclTRY (clear [destVar c])
-            else tclIDTAC in
-          let ipats =
-            if use_injection_pattern_l2r_order ()
-            then adjust_intro_patterns n ipats
-            else ipats in
-          tclTHEN
-            (clear_tac)
-            (intros_pattern MoveLast ipats)
-      | None -> tclIDTAC)
-    l2r
+  injEqThen (postInjEqTac ipats) l2r
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
@@ -1215,25 +1214,26 @@ let injClause ipats with_evars = function
 let injConcl gls  = injClause None false None gls
 let injHyp id gls = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) gls
 
-let _ = declare_injector (fun tac -> injEq_then (fun _ -> tac) true)
-
-let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
+let decompEqThen ntac l2r (lbeq,_,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in
-  let sigma =  clause.evd in
+  let sigma = 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 clause cpath dirn sort gls
     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-        ntac 0 gls
+        ntac (clenv_value clause) 0 gls
     | Inr posns ->
-	inject_at_positions env sigma false u clause (List.rev posns) ntac gls
+	inject_at_positions env sigma l2r u clause (List.rev posns)
+          (ntac (clenv_value clause)) gls
 
 let dEqThen with_evars ntac = function
-  | None -> onNegatedEquality with_evars (decompEqThen ntac)
-  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
+  | None -> onNegatedEquality with_evars (decompEqThen ntac false)
+  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac false)) c
+
+let dEq with_evars = dEqThen with_evars (fun c x -> tclIDTAC)
 
-let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
+let _ = declare_intro_decomp_eq (fun tac -> decompEqThen (fun _ -> tac) true)
 
 let swap_equality_args = function
   | MonomorphicLeibnizEq (e1,e2) -> [e2;e1]
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 1413c1b70f..70480d26e7 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -99,7 +99,7 @@ val injHyp       : Id.t -> tactic
 val injConcl     : tactic
 
 val dEq : evars_flag -> constr with_bindings induction_arg option -> tactic
-val dEqThen : evars_flag -> (int -> tactic) -> constr with_bindings induction_arg option -> tactic
+val dEqThen : evars_flag -> (constr -> int -> tactic) -> constr with_bindings induction_arg option -> tactic
 
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b508fb83b6..ed22ab0e18 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -308,7 +308,7 @@ let projectAndApply thin id eqname names depids gls =
     | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 gls
     | _ -> tac id gls
   in
-  let deq_trailer id neqns =
+  let deq_trailer id _ neqns =
     tclTHENSEQ
       [(if not (List.is_empty names) then clear [id] else tclIDTAC);
        (tclMAP_i neqns (fun idopt ->
@@ -387,6 +387,8 @@ let rec get_names allow_conj (loc,pat) = match pat with
         (Some n, n :: List.map get_name l)
       end else
 	error"Nested conjunctive patterns not allowed for inversion equations."
+  | IntroInjection l ->
+      error "Injection patterns not allowed for inversion equations."
   | IntroOrAndPattern l ->
       error "Disjunctive patterns not allowed for inversion equations."
   | IntroIdentifier id ->
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index dbe8b8dd73..503888c380 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -278,6 +278,8 @@ let intern_message ist = List.map (intern_message_token ist)
 let rec intern_intro_pattern lf ist = function
   | loc, IntroOrAndPattern l ->
       loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
+  | loc, IntroInjection l ->
+      loc, IntroInjection (List.map (intern_intro_pattern lf ist) l)
   | loc, IntroIdentifier id ->
       loc, IntroIdentifier (intern_ident lf ist id)
   | loc, IntroFresh id ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a7cfc08e98..08b165b872 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -431,6 +431,8 @@ let rec intropattern_ids (loc,pat) = match pat with
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll ->
       List.flatten (List.map intropattern_ids (List.flatten ll))
+  | IntroInjection l ->
+      List.flatten (List.map intropattern_ids l)
   | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _
   | IntroForthcoming _ -> []
 
@@ -717,6 +719,8 @@ let interp_message ist gl l =
 let rec interp_intro_pattern ist gl = function
   | loc, IntroOrAndPattern l ->
       loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l)
+  | loc, IntroInjection l ->
+      loc, IntroInjection (interp_intro_pattern_list_as_list ist gl l)
   | loc, IntroIdentifier id ->
       loc, interp_intro_pattern_var loc ist (pf_env gl) id
   | loc, IntroFresh id ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cee98b7c54..f357da8178 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1323,9 +1323,9 @@ let adjust_intro_patterns nb ipats =
   | ip :: l -> ip :: aux (n-1) l in
   aux nb ipats
 
-let inj_function = ref (fun _ -> failwith "Not implemented")
+let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented")
 
-let declare_injector f = inj_function := f
+let declare_intro_decomp_eq f = intro_decomp_eq_function := f
 
 let my_find_eq_data_decompose gl t =
   try find_eq_data_decompose gl t
@@ -1334,31 +1334,28 @@ let my_find_eq_data_decompose gl t =
        known equalities will be dynamically registered *)
       -> raise Matching.PatternMatchingFailure
 
+let intro_decomp_eq loc b l l' thin tac id gl =
+  let c = mkVar id in
+  let _,t = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+  let eq,eq_args = my_find_eq_data_decompose gl t in
+  let eq_clause = make_clenv_binding gl (c,t) NoBindings in
+  !intro_decomp_eq_function
+    (fun n -> tac ((dloc,id)::thin) (adjust_intro_patterns n l @ l'))
+    (eq,t,eq_args) eq_clause gl
+
 let intro_or_and_pattern loc b ll l' thin tac id gl =
   let c = mkVar id in
   let ind,t = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  try
-    (* Use injection if an equality type *)
-    let eq,eq_args = my_find_eq_data_decompose gl t in
-    match fix_empty_or_and_pattern 1 ll with
-    | [l] ->
-        let eq_clause = make_clenv_binding gl (c,t) NoBindings in
-        !inj_function
-          (fun n -> tac ((dloc,id)::thin) (adjust_intro_patterns n l @ l'))
-          (eq,t,eq_args) eq_clause gl
-    | ll -> check_or_and_pattern_size loc ll 1; assert false
-  with Matching.PatternMatchingFailure ->
-    (* Use "destruct" otherwise *)
-    let nv = mis_constr_nargs ind in
-    let bracketed = b || not (List.is_empty l') in
-    let adjust n l = if bracketed then adjust_intro_patterns n l else l in
-    let ll = fix_empty_or_and_pattern (Array.length nv) ll in
-    check_or_and_pattern_size loc ll (Array.length nv);
-    tclTHENLASTn
-      (tclTHEN (simplest_case c) (clear [id]))
-      (Array.map2 (fun n l -> tac thin ((adjust n l)@l'))
-	nv (Array.of_list ll))
-      gl
+  let nv = mis_constr_nargs ind in
+  let bracketed = b || not (List.is_empty l') in
+  let adjust n l = if bracketed then adjust_intro_patterns n l else l in
+  let ll = fix_empty_or_and_pattern (Array.length nv) ll in
+  check_or_and_pattern_size loc ll (Array.length nv);
+  tclTHENLASTn
+    (tclTHEN (simplest_case c) (clear [id]))
+    (Array.map2 (fun n l -> tac thin ((adjust n l)@l'))
+       nv (Array.of_list ll))
+    gl
 
 let rewrite_hyp l2r id gl =
   let rew_on l2r =
@@ -1393,6 +1390,8 @@ let rec explicit_intro_names = function
       | IntroRewrite _ | IntroForthcoming _)) :: l -> explicit_intro_names l
 | (_, IntroOrAndPattern ll) :: l' ->
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
+| (_, IntroInjection l) :: l' ->
+    explicit_intro_names (l@l')
 | [] ->
     []
 
@@ -1441,6 +1440,10 @@ let rec intros_patterns b avoid ids thin destopt tac = function
       intro_then_force
 	(intro_or_and_pattern loc b ll l' thin
 	   (fun thin -> intros_patterns b avoid ids thin destopt tac))
+  | (loc, IntroInjection l) :: l' ->
+      intro_then_force
+	(intro_decomp_eq loc b l l' thin
+	   (fun thin -> intros_patterns b avoid ids thin destopt tac))
   | (loc, IntroRewrite l2r) :: l ->
       intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l))
 	MoveLast true false
@@ -1480,6 +1483,10 @@ let prepare_intros s ipat gl = match ipat with
       onLastHypId
 	(intro_or_and_pattern loc true ll [] []
 	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards)))
+  | IntroInjection l -> make_id s gl,
+      onLastHypId
+	(intro_decomp_eq loc true l [] []
+	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards)))
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected")
 
@@ -1520,6 +1527,10 @@ let as_tac id ipat = match ipat with
       intro_or_and_pattern loc true ll [] []
         (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards))
         id
+  | Some (loc,IntroInjection l) ->
+      intro_decomp_eq loc true l [] []
+        (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards))
+        id
   | Some (loc,
       (IntroIdentifier _ | IntroAnonymous | IntroFresh _ |
        IntroWildcard | IntroForthcoming _)) ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 99d41a4873..cdc8eb3757 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -398,7 +398,7 @@ val general_multi_rewrite :
 val subst_one :
   (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t
 
-val declare_injector :
+val declare_intro_decomp_eq :
   ((int -> tactic) -> Coqlib.coq_eq_data * types *
    (types * constr * constr) ->
    clausenv -> tactic) -> unit
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 9847e09872..f1ee8a05f7 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -73,6 +73,17 @@ intros * (H1,H2).
 exact H1.
 Qed.
 
+(* Test injection using K, knowing that an equality is decidable *)
+(* Basic case, using sigT *)
+
+Scheme Equality for nat.
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  existT P n H1 = existT P n H2 -> H1 = H2.
+intros.
+injection H.
+intro H0. exact H0.
+Abort.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.