Exporting a generic argument induction_arg. As a consequence,

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

4 files changed, 35 insertions, 54 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 6d4ec83f87..60ce59ed92 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 79240d2e78..2bbb3b309b 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 a418a624f9..12119e5184 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 8cb07e1c22..cce4382c2c 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;
   ()