diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.mli | 11 |
2 files changed, 0 insertions, 15 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 33b070e765..5bc3161b93 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -23,10 +23,6 @@ let project x = x.sigma let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -let abstract_tactic_expr tacfun = tacfun -let abstract_tactic tacfun = tacfun -let abstract_extended_tactic tacfun = tacfun - let refiner pr goal_sigma = let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in {it=sgl; sigma = sigma'} diff --git a/proofs/refiner.mli b/proofs/refiner.mli index bc47a73c9f..d353a566fa 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -26,17 +26,6 @@ val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list -(** {6 Hiding the implementation of tactics. } *) - -(** [abstract_tactic tac] hides the (partial) proof produced by [tac] under - a single proof node. The boolean tells if the default tactic is used. *) -(* spiwack: currently here for compatibility, the tactic expression - is discarded and we simply return the tactic. *) - -val abstract_tactic : tactic -> tactic -val abstract_tactic_expr : tactic -> tactic -val abstract_extended_tactic : tactic -> tactic - val refiner : rule -> tactic (** {6 Tacticals. } *) |