diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-22 15:31:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-23 12:09:14 +0200 |
| commit | 74ddca99c649f2f8c203582a9b82bddf64fb6b52 (patch) | |
| tree | f23aa6340c2630619864666ef5eed257d3d765d9 /tactics/tacticals.ml | |
| parent | d23c7539887366202bc370d0f80c26a557486e1c (diff) | |
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f1b52ebc7..bd33e5146 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -63,13 +63,6 @@ let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST let tclTHENSEQ = tclTHENLIST -(* Experimental *) - -let rec tclFIRST_PROGRESS_ON tac = function - | [] -> tclFAIL 0 (str "No applicable tactic") - | [a] -> tac a (* so that returned failure is the one from last item *) - | a::tl -> tclORELSE (tac a) (tclFIRST_PROGRESS_ON tac tl) - (************************************************************************) (* Tacticals applying on hypotheses *) (************************************************************************) @@ -126,9 +119,6 @@ let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl) let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl -let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl -let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl - let onClause tac cl gls = let hyps () = pf_ids_of_hyps gls in tclMAP tac (Locusops.simple_clause_of hyps cl) gls |