Exporting a generic argument induction_arg. As a consequence,

simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.

16 files changed, 104 insertions, 99 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 011b31d9a..ca828102b 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -61,6 +61,9 @@ let wit_red_expr = make0 "redexpr"
 let wit_clause_dft_concl  =
   make0 "clause_dft_concl"
 
+let wit_destruction_arg =
+  make0 "destruction_arg"
+
 (** Aliases *)
 
 let wit_reference = wit_ref
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 70c9c0de2..6ccd944d4 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -69,6 +69,11 @@ val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
 
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
 
+val wit_destruction_arg :
+  (constr_expr with_bindings destruction_arg,
+   glob_constr_and_expr with_bindings destruction_arg,
+   delayed_open_constr_with_bindings destruction_arg) genarg_type
+
 (** Aliases for compatibility *)
 
 val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 35e6a2e31..5b5957bef 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -40,13 +40,13 @@ type goal_selector =
   | SelectId of Id.t
   | SelectAll
 
-type 'a core_induction_arg =
+type 'a core_destruction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of Id.t located
   | ElimOnAnonHyp of int
 
-type 'a induction_arg =
-  clear_flag * 'a core_induction_arg
+type 'a destruction_arg =
+  clear_flag * 'a core_destruction_arg
 
 type inversion_kind =
   | SimpleInversion
@@ -68,7 +68,7 @@ type 'id message_token =
   | MsgIdent of 'id
 
 type ('dconstr,'id) induction_clause =
-    'dconstr with_bindings induction_arg *
+    'dconstr with_bindings destruction_arg *
     (intro_pattern_naming_expr located option (* eqn:... *)
     * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 6d4ec83f8..60ce59ed9 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -27,6 +27,7 @@ open Equality
 open Misctypes
 open Sigma.Notations
 open Proofview.Notations
+open Constrarg
 
 DECLARE PLUGIN "extratactics"
 
@@ -82,48 +83,38 @@ let induction_arg_of_quantified_hyp = function
    ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
    ElimOnIdent and not as "constr" *)
 
+let mytclWithHoles tac with_evars c =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Tacmach.New.pf_env gl in
+    let sigma = Tacmach.New.project gl in
+    let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in
+    Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma'
+  end }
+
 let elimOnConstrWithHoles tac with_evars c =
   Tacticals.New.tclDELAYEDWITHHOLES with_evars c
     (fun c -> tac with_evars (Some (None,ElimOnConstr c)))
 
-TACTIC EXTEND simplify_eq_main
-| [ "simplify_eq" constr_with_bindings(c) ] ->
-    [ elimOnConstrWithHoles dEq false c ]
-END
 TACTIC EXTEND simplify_eq
   [ "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) ] ->
-    [ elimOnConstrWithHoles dEq true c ]
+| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false 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)) ]
+| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ]
 END
 
 let discr_main c = elimOnConstrWithHoles discr_tac false c
 
-TACTIC EXTEND discriminate_main
-| [ "discriminate" constr_with_bindings(c) ] ->
-    [ discr_main c ]
-END
 TACTIC EXTEND discriminate
 | [ "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) ] ->
-    [ elimOnConstrWithHoles discr_tac true c ]
+| [ "discriminate" destruction_arg(c) ] ->
+    [ mytclWithHoles discr_tac false c ]
 END
 TACTIC EXTEND ediscriminate
 | [ "ediscriminate" ] -> [ discr_tac true None ]
-| [ "ediscriminate" quantified_hypothesis(h) ] ->
-    [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
+| [ "ediscriminate" destruction_arg(c) ] ->
+    [ mytclWithHoles discr_tac true c ]
 END
 
 let discrHyp id =
@@ -133,42 +124,25 @@ let discrHyp id =
 let injection_main with_evars c =
  elimOnConstrWithHoles (injClause None) with_evars c
 
-TACTIC EXTEND injection_main
-| [ "injection" constr_with_bindings(c) ] ->
-    [ injection_main false c ]
-END
 TACTIC EXTEND injection
 | [ "injection" ] -> [ injClause None false None ]
-| [ "injection" quantified_hypothesis(h) ] ->
-    [ injClause None false (Some (induction_arg_of_quantified_hyp h)) ]
-END
-TACTIC EXTEND einjection_main
-| [ "einjection" constr_with_bindings(c) ] ->
-    [ injection_main true c ]
+| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ]
 END
 TACTIC EXTEND einjection
 | [ "einjection" ] -> [ injClause None true None ]
-| [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ]
-END
-TACTIC EXTEND injection_as_main
-| [ "injection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
-    [ elimOnConstrWithHoles (injClause (Some ipat)) false c ]
+| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ]
 END
 TACTIC EXTEND injection_as
 | [ "injection" "as" intropattern_list(ipat)] ->
     [ injClause (Some ipat) false None ]
-| [ "injection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
-    [ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ]
-END
-TACTIC EXTEND einjection_as_main
-| [ "einjection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
-    [ elimOnConstrWithHoles (injClause (Some ipat)) true c ]
+| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
+    [ mytclWithHoles (injClause (Some ipat)) false c ]
 END
 TACTIC EXTEND einjection_as
 | [ "einjection" "as" intropattern_list(ipat)] ->
     [ injClause (Some ipat) true None ]
-| [ "einjection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
-    [ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ]
+| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
+    [ mytclWithHoles (injClause (Some ipat)) true c ]
 END
 
 let injHyp id =
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 79240d2e7..2bbb3b309 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -269,7 +269,7 @@ let intern_intro_pattern_naming_loc lf ist (loc,pat) =
   (loc,intern_intro_pattern_naming lf ist pat)
 
   (* TODO: catch ltac vars *)
-let intern_induction_arg ist = function
+let intern_destruction_arg ist = function
   | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c)
   | clear,ElimOnAnonHyp n as x -> x
   | clear,ElimOnIdent (loc,id) ->
@@ -511,7 +511,7 @@ let rec intern_atomic lf ist x =
   (* Derived basic tactics *)
   | TacInductionDestruct (ev,isrec,(l,el)) ->
       TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats),cls) ->
-	      (intern_induction_arg ist c,
+	      (intern_destruction_arg ist c,
                (Option.map (intern_intro_pattern_naming_loc lf ist) ipato,
                Option.map (intern_or_and_intro_pattern_loc lf ist) ipats),
                Option.map (clause_app (intern_hyp_location ist)) cls)) l,
@@ -792,6 +792,7 @@ let () =
   Genintern.register_intern0 wit_red_expr (lift intern_red_expr);
   Genintern.register_intern0 wit_bindings (lift intern_bindings);
   Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
+  Genintern.register_intern0 wit_destruction_arg (lift intern_destruction_arg);
   ()
 
 (***************************************************************************)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index a418a624f..12119e518 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1031,7 +1031,7 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
   } in
     (loc,f)
 
-let interp_induction_arg ist gl arg =
+let interp_destruction_arg ist gl arg =
   match arg with
   | keep,ElimOnConstr c ->
       keep,ElimOnConstr { delayed = fun env sigma ->
@@ -1052,7 +1052,7 @@ let interp_induction_arg ist gl arg =
           (keep, ElimOnConstr { delayed = begin fun env sigma ->
           try Sigma.here (constr_of_id env id', NoBindings) sigma
           with Not_found ->
-            user_err_loc (loc, "interp_induction_arg",
+            user_err_loc (loc, "interp_destruction_arg",
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
           end })
       in
@@ -1799,7 +1799,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             (* TODO: move sigma as a side-effect *)
              (* spiwack: the [*p] variants are for printing *)
             let cp = c in
-            let c = interp_induction_arg ist gl c in
+            let c = interp_destruction_arg ist gl c in
             let ipato = interp_intro_pattern_naming_option ist env sigma ipato in
             let ipatsp = ipats in
             let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in
@@ -2056,6 +2056,10 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
   Sigma.Unsafe.of_pair (c, sigma)
   }
 
+let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl ->
+  Ftactic.return (interp_destruction_arg ist gl c)
+end }
+
 let () =
   register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
   register_interp0 wit_ref (lift interp_reference);
@@ -2070,6 +2074,7 @@ let () =
   register_interp0 wit_open_constr (lifts interp_open_constr);
   register_interp0 wit_bindings interp_bindings';
   register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
+  register_interp0 wit_destruction_arg interp_destruction_arg';
   ()
 
 let () =
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 8cb07e1c2..cce4382c2 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -63,7 +63,7 @@ and subst_intro_or_and_pattern subst = function
   | IntroOrPattern ll ->
       IntroOrPattern (List.map (List.map (subst_intro_pattern subst)) ll)
 
-let subst_induction_arg subst = function
+let subst_destruction_arg subst = function
   | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c)
   | clear,ElimOnAnonHyp n as x -> x
   | clear,ElimOnIdent id as x -> x
@@ -158,7 +158,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Derived basic tactics *)
   | TacInductionDestruct (isrec,ev,(l,el)) ->
       let l' = List.map (fun (c,ids,cls) ->
-        subst_induction_arg subst c, ids, cls) l in
+        subst_destruction_arg subst c, ids, cls) l in
       let el' = Option.map (subst_glob_with_bindings subst) el in
       TacInductionDestruct (isrec,ev,(l',el'))
 
@@ -303,4 +303,5 @@ let () =
   Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
   Genintern.register_subst0 wit_bindings subst_bindings;
   Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
+  Genintern.register_subst0 wit_destruction_arg subst_destruction_arg;
   ()
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a8a88d33f..d0bca9ee3 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -141,7 +141,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
   (id,CProdN(loc,bl,ty))
 
 (* Functions overloaded by quotifier *)
-let induction_arg_of_constr (c,lbind as clbind) = match lbind with
+let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
   | NoBindings ->
     begin
       try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
@@ -216,7 +216,7 @@ let merge_occurrences loc cl = function
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
   bindings red_expr int_or_var open_constr uconstr
-  simple_intropattern clause_dft_concl hypident;
+  simple_intropattern clause_dft_concl hypident destruction_arg;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
@@ -236,11 +236,11 @@ GEXTEND Gram
   uconstr:
     [ [ c = constr -> c ] ]
   ;
-  induction_arg:
+  destruction_arg:
     [ [ n = natural -> (None,ElimOnAnonHyp n)
       | test_lpar_id_rpar; c = constr_with_bindings ->
-        (Some false,induction_arg_of_constr c)
-      | c = constr_with_bindings_arg -> on_snd induction_arg_of_constr c
+        (Some false,destruction_arg_of_constr c)
+      | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c
     ] ]
   ;
   constr_with_bindings_arg:
@@ -499,8 +499,8 @@ GEXTEND Gram
     [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
   ;
   induction_clause:
-    [ [ c = induction_arg; pat = as_or_and_ipat; eq = eqn_ipat; cl = opt_clause
-        -> (c,(eq,pat),cl) ] ]
+    [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
+        cl = opt_clause -> (c,(eq,pat),cl) ] ]
   ;
   induction_clause_list:
     [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator;
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index efb89cd6e..7d1c63ee0 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -345,6 +345,7 @@ module Tactic =
       make_gen_entry utactic "uconstr"
     let quantified_hypothesis =
       make_gen_entry utactic "quantified_hypothesis"
+    let destruction_arg = make_gen_entry utactic "destruction_arg"
     let int_or_var = make_gen_entry utactic "int_or_var"
     let red_expr = make_gen_entry utactic "red_expr"
     let simple_intropattern =
@@ -520,4 +521,5 @@ let () =
   Grammar.register0 wit_tactic (Tactic.tactic);
   Grammar.register0 wit_ltac (Tactic.tactic);
   Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl);
+  Grammar.register0 wit_destruction_arg (Tactic.destruction_arg);
   ()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 319ca256e..008374e09 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -188,6 +188,7 @@ module Tactic :
     val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
     val uconstr : constr_expr Gram.entry
     val quantified_hypothesis : quantified_hypothesis Gram.entry
+    val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
     val int_or_var : int or_var Gram.entry
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_tactic_expr Gram.entry
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index bc39c9304..b6e4c8011 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -620,11 +620,14 @@ module Make
     | RepeatStar -> str "?"
     | RepeatPlus -> str "!"
 
-  let pr_induction_arg prc prlc = function
+  let pr_core_destruction_arg prc prlc = function
     | ElimOnConstr c -> pr_with_bindings prc prlc c
     | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
     | ElimOnAnonHyp n -> int n
 
+  let pr_destruction_arg prc prlc (clear_flag,h) =
+    pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
+                               
   let pr_inversion_kind = function
     | SimpleInversion -> primitive "simple inversion"
     | FullInversion -> primitive "inversion"
@@ -924,8 +927,8 @@ module Make
           hov 1 (
             primitive (with_evars ev (if isrec then "induction" else "destruct"))
             ++ spc ()
-            ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
-              pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
+            ++ prlist_with_sep pr_comma (fun (h,ids,cl) ->
+              pr_destruction_arg pr.pr_dconstr pr.pr_dconstr h ++
                 pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++
                 pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
@@ -1357,6 +1360,11 @@ end)
 let run_delayed c =
   Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
 
+let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
+  | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g))
+  | clear_flag,ElimOnAnonHyp n as x -> x
+  | clear_flag,ElimOnIdent id as x -> x
+
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
@@ -1411,6 +1419,10 @@ let () =
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
+  Genprint.register_print0 Constrarg.wit_destruction_arg
+    (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
+    (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it));
   Genprint.register_print0 Stdarg.wit_int int int int;
   Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
   Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 458d8f372..1122615c3 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -72,16 +72,16 @@ val discrConcl   : unit Proofview.tactic
 val discrHyp     : Id.t -> unit Proofview.tactic
 val discrEverywhere : evars_flag -> unit Proofview.tactic
 val discr_tac    : evars_flag ->
-  constr with_bindings induction_arg option -> unit Proofview.tactic
+  constr with_bindings destruction_arg option -> unit Proofview.tactic
 val inj          : intro_patterns option -> evars_flag ->
   clear_flag -> constr with_bindings -> unit Proofview.tactic
 val injClause    : intro_patterns option -> evars_flag ->
-  constr with_bindings induction_arg option -> unit Proofview.tactic
+  constr with_bindings destruction_arg option -> unit Proofview.tactic
 val injHyp       : clear_flag -> Id.t -> unit Proofview.tactic
 val injConcl     : unit Proofview.tactic
 
-val dEq : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic
-val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic
+val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
 
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5286e2678..23aadf393 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1121,6 +1121,14 @@ let run_delayed env sigma c =
 (* Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
+let tactic_infer_flags with_evar = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.use_unif_heuristics = true;
+  Pretyping.use_hook = Some solve_by_implicit_tactic;
+  Pretyping.fail_evar = not with_evar;
+  Pretyping.expand_evars = true }
+
+
 let onOpenInductionArg env sigma tac = function
   | clear_flag,ElimOnConstr f ->
       let (cbl, sigma') = run_delayed env sigma f in
@@ -1161,24 +1169,25 @@ let onInductionArg tac = function
         (try_intros_until_id_check id)
         (tac clear_flag (mkVar id,NoBindings))
 
-let map_induction_arg f = function
-  | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (f g)
-  | clear_flag,ElimOnAnonHyp n as x -> x
-  | clear_flag,ElimOnIdent id as x -> x
+let map_destruction_arg f sigma = function
+  | clear_flag,ElimOnConstr g -> let sigma,x = f sigma g in (sigma, (clear_flag,ElimOnConstr x))
+  | clear_flag,ElimOnAnonHyp n as x -> (sigma,x)
+  | clear_flag,ElimOnIdent id as x -> (sigma,x)
 
-let finish_delayed_evar_resolution env sigma f =
+let finish_delayed_evar_resolution with_evars env sigma f =
   let ((c, lbind), sigma') = run_delayed env sigma f in
   let pending = (sigma,sigma') in
   let sigma' = Sigma.Unsafe.of_evar_map sigma' in
-  let Sigma (c, _, _) = finish_evar_resolution env sigma' (pending,c) in
-  (c, lbind)
+  let flags = tactic_infer_flags with_evars in
+  let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in
+  (Sigma.to_evar_map sigma', (c, lbind))
 
 let with_no_bindings (c, lbind) =
   if lbind != NoBindings then error "'with' clause not supported here.";
   c
 
-let force_induction_arg env sigma c =
-  map_induction_arg (finish_delayed_evar_resolution env sigma) c
+let force_destruction_arg with_evars env sigma c =
+  map_destruction_arg (finish_delayed_evar_resolution with_evars env) sigma c
 
 (****************************************)
 (* tactic "cut" (actually modus ponens) *)
@@ -2551,13 +2560,6 @@ let apply_delayed_in simple with_evars id lemmas ipat =
 (* Implementation without generalisation: abbrev will be lost in hyps in *)
 (* in the extracted proof *)
 
-let tactic_infer_flags with_evar = {
-  Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
-  Pretyping.use_hook = Some solve_by_implicit_tactic;
-  Pretyping.fail_evar = not with_evar;
-  Pretyping.expand_evars = true }
-
 let decode_hyp = function
   | None -> MoveLast
   | Some id -> MoveAfter id
@@ -4417,7 +4419,7 @@ let induction_destruct isrec with_evars (lc,elim) =
       (* Standard induction on non-standard induction schemes *)
       (* will be removable when is_functional_induction will be more clever *)
       if not (Option.is_empty cls) then error "'in' clause not supported here.";
-      let c = force_induction_arg env sigma c in
+      let _,c = force_destruction_arg false env sigma c in
       onInductionArg
 	(fun _clear_flag c ->
 	  induction_gen_l isrec with_evars elim names
@@ -4452,7 +4454,7 @@ let induction_destruct isrec with_evars (lc,elim) =
           end }) l)
     | Some elim ->
       (* Several induction hyps with induction scheme *)
-      let lc = List.map (on_pi1 (force_induction_arg env sigma)) lc in
+      let lc = List.map (on_pi1 (fun c -> snd (force_destruction_arg false env sigma c))) lc in
       let newlc =
         List.map (fun (x,(eqn,names),cls) ->
           if cls != None then error "'in' clause not yet supported here.";
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 78a237395..012c75091 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -94,11 +94,11 @@ val try_intros_until :
 
 val onInductionArg :
   (clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
-    constr with_bindings induction_arg -> unit Proofview.tactic
+    constr with_bindings destruction_arg -> unit Proofview.tactic
 
-val force_induction_arg : env -> evar_map ->
-    delayed_open_constr_with_bindings induction_arg ->
-    constr with_bindings induction_arg
+val force_destruction_arg : evars_flag -> env -> evar_map ->
+    delayed_open_constr_with_bindings destruction_arg ->
+    evar_map * constr with_bindings destruction_arg
 
 (** Tell if a used hypothesis should be cleared by default or not *)
 
@@ -299,7 +299,7 @@ val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option
 (** Implements user-level "destruct" and "induction" *)
 
 val induction_destruct : rec_flag -> evars_flag ->
-  (delayed_open_constr_with_bindings induction_arg
+  (delayed_open_constr_with_bindings destruction_arg
    * (intro_pattern_naming option * or_and_intro_pattern option)
    * clause option) list *
   constr with_bindings option -> unit Proofview.tactic
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 21a8cf9ed..21554e9ff 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -16,9 +16,8 @@ The command has indeed failed with message:
 In nested Ltac calls to "f2", "f1" and "refine", last call failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-Ltac call to "h" failed.
-Error: Ltac variable x is bound to I which cannot be coerced to
-a declared or quantified hypothesis.
+In nested Ltac calls to "h" and "injection", last call failed.
+Error: No primitive equality found.
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection", last call failed.
 Error: No primitive equality found.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 56ed89ed8..c072cc641 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -124,7 +124,7 @@ intros * [= H].
 exact H.
 Abort.
 
-(* Injection does not projects at positions in Prop... allow it?
+(* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
 Goal forall p q : True\/True, c _ p = c _ q -> False.