diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:24 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:24 +0000 |
| commit | 8e10368c387570df13904531bfba05130335ed0e (patch) | |
| tree | 50d7a35c9a45e0c9496da4a4ad22ead531be829d /proofs/refiner.ml | |
| parent | 2e3cf396ba869987c4e41f46bc9b4b2fe31ab4d2 (diff) | |
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box
Nested was never constructed, while the notion of abstract_tactic_box
is obsolete (cf. Refiner.abstract_tactic).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 4f75ffa52..87ba77dc5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -23,18 +23,9 @@ 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_operation syntax semantics = - semantics - -let abstract_tactic_expr ?(dflt=false) te tacfun gls = - abstract_operation (Tactic(te,dflt)) tacfun gls - -let abstract_tactic ?(dflt=false) te = - !abstract_tactic_box := Some te; - abstract_tactic_expr ~dflt (Tacexpr.TacAtom (Loc.ghost,te)) - -let abstract_extended_tactic ?(dflt=false) s args = - abstract_tactic ~dflt (Tacexpr.TacExtend (Loc.ghost, s, args)) +let abstract_tactic_expr ?(dflt=false) te tacfun = tacfun +let abstract_tactic ?(dflt=false) te tacfun = tacfun +let abstract_extended_tactic ?(dflt=false) s args tacfun = tacfun let refiner = function | Prim pr -> @@ -44,7 +35,7 @@ let refiner = function {it=sgl; sigma = sigma'}) - | Nested (_,_) | Decl_proof _ -> + | Decl_proof _ -> failwith "Refiner: should not occur" (* Daimon is a canonical unfinished proof *) |