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

9 files changed, 18 insertions, 121 deletions

diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 623d7c804..c29e4a3b3 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -47,13 +47,6 @@ let pr_proof_instr_xml instr =
 
 let pr_rule_xml pr = function
   | Prim r -> str "<rule text=\"" ++ xmlstream (pr_prim_rule r) ++ str "\"/>"
-  | Nested(cmpd, subtree) ->
-      hov 2 (str "<cmpdrule>" ++ fnl () ++
-        begin match cmpd with
-          Tactic (texp, _) -> pr_tactic_xml texp
-        end ++ fnl ()
-        ++ pr subtree
-      ) ++ fnl () ++ str "</cmpdrule>"
   | Daimon -> str "<daimon/>"
   | Decl_proof _ -> str "<proof/>"
 ;;
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 033e83410..3831ee9fa 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -113,57 +113,6 @@ Pp.msg_warning (Pp.(++) (Pp.str
             (List.fold_left
               (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
-     | {PT.goal=goal;
-        PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} ->
-         (* [hidden_proof] is the proof of the tactic;                     *)
-         (* [nodes] are the proof of the subgoals generated by the tactic; *)
-         (* [flat_proof] if the proof-tree obtained substituting [nodes]   *)
-         (*  for the holes in [hidden_proof]                               *)
-        let flat_proof =
-         Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
-        in begin
-        match tactic_expr with
-        | Tacexpr.TacArg (_,Tacexpr.Tacexp _) ->
-            (* We don't need to keep the level of abstraction introduced at *)
-            (* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
-            aux flat_proof old_hyps
-        | _ ->
-         (****** la tactique employee *)
-	 let prtac = Pptactic.pr_tactic (Global.env()) in
-         let tac = Pp.string_of_ppcmds (prtac tactic_expr) in
-         let tacname= first_word tac in
-         let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
-
-         (****** le but *)
-
-	 let concl = Goal.V82.concl sigma goal in
-	 let hyps = Goal.V82.hyps sigma goal in
-
-         let env = Global.env_of_context hyps in
-	   
-
-         let xgoal =
-          X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
-
-         let rec build_hyps =
-          function
-           | [] -> xgoal
-           | (id,c,tid)::hyps1 ->
-              let id' = Names.string_of_id id in
-               [< build_hyps hyps1;
-                  (X.xml_nempty "Hypothesis"
-                    ["id",idref_of_id id' ; "name",id']
-                    (constr_to_xml tid sigma env))
-               >] in
-         let old_names = List.map (fun (id,c,tid)->id) old_hyps in
-	 let nhyps = Environ.named_context_of_val hyps in
-         let new_hyps =
-          List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in
-
-         X.xml_nempty "Tactic" of_attribute
-          [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
-        end
-
      | {PT.ref=Some(PT.Daimon,_)} ->
          X.xml_empty "Hidden_open_goal" of_attribute
 
diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml
index 87bb89e8d..49d7c21f6 100644
--- a/printing/tactic_printer.ml
+++ b/printing/tactic_printer.ml
@@ -23,31 +23,16 @@ let pr_tactic = function
 
 let pr_rule = function
   | Prim r -> hov 0 (pr_prim_rule r)
-  | Nested(cmpd,_) ->
-      begin
-	match cmpd with
-	  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
-      end
   | Daimon -> str "<Daimon>"
   | Decl_proof _ -> str "proof"
 
-let uses_default_tac = function
-  | Nested(Tactic(_,dflt),_) -> dflt
-  | _ -> false
-
 (* Does not print change of evars *)
 let pr_rule_dot = function
   | Prim Change_evars ->str "PC: ch_evars" ++  mt ()
       (* PC: this might be redundant *)
-  | r ->
-      pr_rule r ++ if uses_default_tac r then str "..." else str"."
+  | r -> pr_rule r ++ str"."
 
 let pr_rule_dot_fnl = function
-  | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
-                              | TacMutualCofix (true,_,_))),_),_) ->
-      (* Very big hack to not display hidden tactics in "Theorem with" *)
-      (* (would not scale!) *)
-      mt ()
    | Prim Change_evars -> mt ()
    | r -> pr_rule_dot r ++ fnl ()
 
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 :
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0c7d6e0ca..12c970d68 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -227,11 +227,7 @@ let lookup_tactic s =
   with Not_found ->
     errorlabstrm "Refiner.lookup_tactic"
       (str"The tactic " ++ str s ++ str" is not installed.")
-(*
-let vernac_tactic (s,args) =
-  let tacfun = lookup_tactic s args in
-  abstract_extended_tactic s args tacfun
-*)
+
 (* Interpretation of extra generic arguments *)
 type glob_sign = {
   ltacvars : identifier list * identifier list;
@@ -1783,8 +1779,7 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
 and eval_tactic ist = function
   | TacAtom (loc,t) ->
       fun gl ->
-	let box = ref None in abstract_tactic_box := box;
-	let call = LtacAtomCall (t,box) in
+	let call = LtacAtomCall t in
 	let tac = (* catch error in the interpretation *)
 	  catch_error (push_trace(dloc,call)ist.trace)
 	    (interp_atomic ist gl) t	in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 141acb3db..c0027ef03 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -996,11 +996,7 @@ let explain_reduction_tactic_error = function
 
 let explain_ltac_call_trace (nrep,last,trace,loc) =
   let calls =
-    (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in
-  let tacexpr_differ te te' =
-    (* NB: The following comparison may raise an exception
-       since a tacexpr may embed a functional part via a TacExtend *)
-    try te <> te' with Invalid_argument _ -> false
+    (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace)
   in
   let pr_call (n,ck) =
     (match ck with
@@ -1009,16 +1005,9 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
        | Proof_type.LtacVarCall (id,t) ->
 	   quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
 	     Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
-       | Proof_type.LtacAtomCall (te,otac) -> quote
-	   (Pptactic.pr_glob_tactic (Global.env())
-	      (Tacexpr.TacAtom (Loc.ghost,te)))
-	   ++ (match !otac with
-		 | Some te' when tacexpr_differ (Obj.magic te') te ->
-		   strbrk " (expanded to " ++ quote
-		     (Pptactic.pr_tactic (Global.env())
-			(Tacexpr.TacAtom (Loc.ghost,te')))
-		   ++ str ")"
-		 | _ -> mt ())
+       | Proof_type.LtacAtomCall te ->
+	   quote (Pptactic.pr_glob_tactic (Global.env())
+		    (Tacexpr.TacAtom (Loc.ghost,te)))
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
 	   let filter =
 	     function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in