From 8e10368c387570df13904531bfba05130335ed0e Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 6 Oct 2012 10:08:24 +0000
Subject: 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
---
 proofs/proof_type.ml  |  6 ++----
 proofs/proof_type.mli |  7 ++-----
 proofs/refiner.ml     | 17 ++++-------------
 proofs/refiner.mli    |  6 +++---
 4 files changed, 11 insertions(+), 25 deletions(-)

(limited to 'proofs')

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 :
-- 
cgit v1.2.3