From 103210f0de563132c61fc33177be31adb8e0ab29 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Apr 2014 18:12:58 +0200 Subject: Simplifying interface of elimination tactics. They used dummy clausenvs, and that should be changed anyway. --- tactics/elim.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'tactics/elim.ml') diff --git a/tactics/elim.ml b/tactics/elim.ml index bbbe62eb5..5eb3dcfe6 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -63,7 +63,7 @@ Another example : *) let elimHypThen tac id = - Tacticals.New.elimination_then tac ([],[]) (mkVar id) + Tacticals.New.elimination_then tac (mkVar id) let rec general_decompose_on_hyp recognizer = Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) @@ -138,8 +138,8 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) -let simple_elimination c gls = - simple_elimination_then (fun _ -> tclIDTAC) c gls +let simple_elimination c = + Tacticals.New.elimination_then (fun _ -> Tacticals.New.tclIDTAC) c let induction_trailer abs_i abs_j bargs = Tacticals.New.tclTHEN @@ -163,7 +163,7 @@ let induction_trailer abs_i abs_j bargs = let ids = List.rev (ids_of_named_context hyps) in (tclTHENSEQ [Proofview.V82.of_tactic (bring_hyps hyps); tclTRY (clear ids); - simple_elimination (mkVar id)]) gls + Proofview.V82.of_tactic (simple_elimination (mkVar id))]) gls end )) @@ -180,8 +180,7 @@ let double_ind h1 h2 = (Tacticals.New.onLastHypId (fun id -> Tacticals.New.elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) - ([],[]) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) end let h_double_induction = double_ind -- cgit v1.2.3