aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:24 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:24 +0000
commit8e10368c387570df13904531bfba05130335ed0e (patch)
tree50d7a35c9a45e0c9496da4a4ad22ead531be829d /proofs
parent2e3cf396ba869987c4e41f46bc9b4b2fe31ab4d2 (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')
-rw-r--r--proofs/proof_type.ml6
-rw-r--r--proofs/proof_type.mli7
-rw-r--r--proofs/refiner.ml17
-rw-r--r--proofs/refiner.mli6
4 files changed, 11 insertions, 25 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 1f5ef315b..4652bac2e 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -46,11 +46,10 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Nested of compound_rule * proof_tree
| Decl_proof of bool
| Daimon
-and compound_rule=
+type compound_rule=
| Tactic of tactic_expr * bool
and tactic_expr =
@@ -89,7 +88,7 @@ and tactic_arg =
type ltac_call_kind =
| LtacNotationCall of string
| LtacNameCall of ltac_constant
- | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
+ | LtacAtomCall of glob_atomic_tactic_expr
| LtacVarCall of identifier * glob_tactic_expr
| LtacConstrInterp of glob_constr *
(extended_patvar_map * (identifier * identifier option) list)
@@ -98,4 +97,3 @@ type ltac_trace = (int * Loc.t * ltac_call_kind) list
exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn
-let abstract_tactic_box = ref (ref None)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 4f7e87ea9..d6081e56c 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -79,11 +79,10 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Nested of compound_rule * proof_tree
| Decl_proof of bool
| Daimon
-and compound_rule=
+type compound_rule=
(** the boolean of Tactic tells if the default tactic is used *)
| Tactic of tactic_expr * bool
@@ -123,7 +122,7 @@ and tactic_arg =
type ltac_call_kind =
| LtacNotationCall of string
| LtacNameCall of ltac_constant
- | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
+ | LtacAtomCall of glob_atomic_tactic_expr
| LtacVarCall of identifier * glob_tactic_expr
| LtacConstrInterp of glob_constr *
(extended_patvar_map * (identifier * identifier option) list)
@@ -131,5 +130,3 @@ type ltac_call_kind =
type ltac_trace = (int * Loc.t * ltac_call_kind) list
exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn
-
-val abstract_tactic_box : atomic_tactic_expr option ref ref
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 *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index b5fc9ee66..6f11e7115 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -30,9 +30,9 @@ val apply_sig_tac :
(** [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, abstract_operation
- is a second projection *)
-val abstract_operation : compound_rule -> tactic -> tactic
+(* spiwack: currently here for compatibility, the tactic expression
+ is discarded and we simply return the tactic. *)
+
val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
val abstract_extended_tactic :