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/refiner.ml | |
| 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/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 4 |
1 files changed, 0 insertions, 4 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'} |