diff options
| author | letouzey | 2012-10-06 10:08:45 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:45 +0000 |
| commit | e1bdb515ee2f701bfc56f1bcf4a8e404f759a38a (patch) | |
| tree | 52eb681313f840b3d46d633ed0440e3ad96ace9a /proofs | |
| parent | f975575187d0a19e7cc1afc43459a92eeb12b3f1 (diff) | |
remove Refiner.abstract_tactic and similar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
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. } *) |