diff options
| -rw-r--r-- | tactics/eqdecide.ml4 | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.mli | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/extratactics.mli | 3 |
5 files changed, 10 insertions, 9 deletions
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index b9c6bbef88..4752b8ed79 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -111,7 +111,7 @@ let diseqCase = (tclTHEN red_in_concl (tclTHEN (intro_using absurd) (tclTHEN (h_simplest_apply (mkVar diseq)) - (tclTHEN (Extratactics.h_injHyp absurd) + (tclTHEN (Extratactics.h_injHyp (Rawterm.NamedHyp absurd)) full_trivial)))))) let solveArg a1 a2 tac g = diff --git a/tactics/equality.ml b/tactics/equality.ml index 346b9dccbd..8bebda9a37 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -802,7 +802,7 @@ let inj id gls = let injClause = function | None -> onNegatedEquality inj - | Some id -> inj id + | Some id -> try_intros_until inj id let injConcl gls = injClause None gls let injHyp id gls = injClause (Some id) gls @@ -865,7 +865,7 @@ let decompEq = decompEqThen (fun x -> tclIDTAC) let dEqThen ntac = function | None -> onNegatedEquality (decompEqThen ntac) - | Some id -> decompEqThen ntac id + | Some id -> try_intros_until (decompEqThen ntac) id let dEq = dEqThen (fun x -> tclIDTAC) diff --git a/tactics/equality.mli b/tactics/equality.mli index 47ec783742..b9591189ac 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -71,10 +71,10 @@ val discrHyp : identifier -> tactic val discrEverywhere : tactic val discr_tac : identifier option -> tactic val inj : identifier -> tactic -val injClause : clause -> tactic +val injClause : quantified_hypothesis option -> tactic -val dEq : clause -> tactic -val dEqThen : (int -> tactic) -> clause -> tactic +val dEq : quantified_hypothesis option -> tactic +val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic val make_iterated_tuple : env -> evar_map -> (constr * constr) -> (constr * constr) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 8ff06745fd..0de8e29639 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -39,7 +39,7 @@ TACTIC EXTEND ReplaceIn END TACTIC EXTEND DEq - [ "Simplify_eq" ident_opt(h) ] -> [ dEq h ] + [ "Simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ] END TACTIC EXTEND Discriminate @@ -49,7 +49,7 @@ END let h_discrHyp id = h_discriminate (Some id) TACTIC EXTEND Injection - [ "Injection" ident_opt(h) ] -> [ injClause h ] + [ "Injection" quantified_hypothesis_opt(h) ] -> [ injClause h ] END let h_injHyp id = h_injection (Some id) diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 0e178b52b4..da842a4385 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -11,9 +11,10 @@ open Names open Term open Proof_type +open Rawterm val h_discrHyp : identifier -> tactic -val h_injHyp : identifier -> tactic +val h_injHyp : quantified_hypothesis -> tactic val h_rewriteLR : constr -> tactic val refine_tac : Genarg.open_constr -> tactic |