diff options
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 9 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
3 files changed, 9 insertions, 7 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 621781187d..2f36d0c7ef 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -135,9 +135,9 @@ let abstract_replace clause c2 c1 unsafe gl = let e = (build_coq_eqT_data ()).eq in let sym = (build_coq_eqT_data ()).sym in let eq = applist (e, [t1;c1;c2]) in - tclTHENS (cut eq) - [tclTHEN intro (onLastHyp (fun id -> - tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id]))); + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id])); tclORELSE assumption (tclTRY (tclTHEN (apply sym) assumption))] gl else diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cebc6697e7..6444c1756b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -506,19 +506,20 @@ let cut_and_apply c gl = (* Cut tactics *) (**************************) -let true_cut na c gl = +let assert_tac first na c gl = match kind_of_term (hnf_type_of gl c) with | Sort s -> - let id = - match na with + let id = match na with | Anonymous -> let d = match s with Prop _ -> "H" | Type _ -> "X" in fresh_id [] (id_of_string d) gl | Name id -> id in - internal_cut id c gl + (if first then internal_cut else internal_cut_rev) id c gl | _ -> error "Not a proposition or a type" +let true_cut = assert_tac true + let cut c gl = match kind_of_term (hnf_type_of gl c) with | Sort _ -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 27a7d998ea..b33bc52f0e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -235,6 +235,7 @@ val cut_intro : constr -> tactic val cut_replacing : identifier -> constr -> tactic val cut_in_parallel : constr list -> tactic +val assert_tac : bool -> name -> constr -> tactic val true_cut : name -> constr -> tactic val letin_tac : bool -> name -> constr -> clause -> tactic val forward : bool -> name -> constr -> tactic |