Proof_type: rule now degenerates to prim_rule

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 34 insertions, 37 deletions

diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index b8a8c5137..c0c8ada95 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -45,9 +45,6 @@ let pr_proof_instr_xml instr =
   Ppdecl_proof.pr_proof_instr (Global.env()) instr
 ;;
 
-let pr_rule_xml pr = function
-  | Prim r -> str "<rule text=\"" ++ xmlstream (pr_prim_rule r) ++ str "\"/>"
-
 let pr_var_decl_xml env (id,c,typ) =
   let ptyp = print_constr_env env typ in
   match c with
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index d806d80b8..b84b6db48 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -21,6 +21,8 @@ open Misctypes
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by Proof_tree and Refiner *)
 
+(** Types of goals, tactics, rules ... *)
+
 type goal = Goal.goal
 
 type tactic = goal sigma -> goal list sigma 
@@ -40,12 +42,11 @@ type prim_rule =
   | Rename of identifier * identifier
   | Change_evars
 
-type rule = Prim of prim_rule
+(** Nowadays, the only rules we'll consider are the primitive rules *)
 
-type compound_rule=
-  | Tactic of tactic_expr * bool
+type rule = prim_rule
 
-and tactic_expr =
+type tactic_expr =
   (constr,
    constr_pattern,
    evaluable_global_reference,
@@ -78,6 +79,8 @@ and tactic_arg =
    tlevel)
      Tacexpr.gen_tactic_arg
 
+(** Ltac traces *)
+
 type ltac_call_kind =
   | LtacNotationCall of string
   | LtacNameCall of ltac_constant
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 832377e31..6688d6e62 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -22,10 +22,6 @@ open Misctypes
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
 
-type goal = Goal.goal
-
-type tactic = goal sigma -> goal list sigma
-
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
@@ -41,6 +37,10 @@ type prim_rule =
   | Rename of identifier * identifier
   | Change_evars
 
+(** Nowadays, the only rules we'll consider are the primitive rules *)
+
+type rule = prim_rule
+
 (** The type [goal sigma] is the type of subgoal. It has the following form
 {v   it    = \{ evar_concl = [the conclusion of the subgoal]
              evar_hyps = [the hypotheses of the subgoal]
@@ -66,13 +66,12 @@ type prim_rule =
                                               in the type of evar] \} \} \} v}
 *)
 
-type rule = Prim of prim_rule
+type goal = Goal.goal
 
-type compound_rule=
-  (** the boolean of Tactic tells if the default tactic is used *)
-  | Tactic of tactic_expr * bool
+type tactic = goal sigma -> goal list sigma
 
-and tactic_expr =
+
+type tactic_expr =
   (constr,
    constr_pattern,
    evaluable_global_reference,
@@ -105,6 +104,8 @@ and tactic_arg =
    tlevel)
      Tacexpr.gen_tactic_arg
 
+(** Ltac traces *)
+
 type ltac_call_kind =
   | LtacNotationCall of string
   | LtacNameCall of ltac_constant
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 9b9b91337..4b5bdcfe9 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -27,15 +27,11 @@ 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 ->
-      let prim_fun = prim_refiner pr in
-	(fun goal_sigma ->
-          let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
-	  {it=sgl; sigma = sigma'})
+let refiner pr goal_sigma =
+  let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
+  {it=sgl; sigma = sigma'}
 
-
-let norm_evar_tac gl = refiner (Prim Change_evars) gl
+let norm_evar_tac gl = refiner (Change_evars) gl
 
 (*********************)
 (*   Tacticals       *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 80a450bcd..0352d5624 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -128,48 +128,48 @@ let refiner = refiner
 
 (* This does not check that the variable name is not here *)
 let introduction_no_check id =
-  refiner (Prim (Intro id))
+  refiner (Intro id)
 
 let internal_cut_no_check replace id t gl =
-  refiner (Prim (Cut (true,replace,id,t))) gl
+  refiner (Cut (true,replace,id,t)) gl
 
 let internal_cut_rev_no_check replace id t gl =
-  refiner (Prim (Cut (false,replace,id,t))) gl
+  refiner (Cut (false,replace,id,t)) gl
 
 let refine_no_check c gl =
-  refiner (Prim (Refine c)) gl
+  refiner (Refine c) gl
 
 let convert_concl_no_check c sty gl =
-  refiner (Prim (Convert_concl (c,sty))) gl
+  refiner (Convert_concl (c,sty)) gl
 
 let convert_hyp_no_check d gl =
-  refiner (Prim (Convert_hyp d)) gl
+  refiner (Convert_hyp d) gl
 
 (* This does not check dependencies *)
 let thin_no_check ids gl =
-  if ids = [] then tclIDTAC gl else refiner (Prim (Thin ids)) gl
+  if ids = [] then tclIDTAC gl else refiner (Thin ids) gl
 
 (* This does not check dependencies *)
 let thin_body_no_check ids gl =
-  if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl
+  if ids = [] then tclIDTAC gl else refiner (ThinBody ids) gl
 
 let move_hyp_no_check with_dep id1 id2 gl =
-  refiner (Prim (Move (with_dep,id1,id2))) gl
+  refiner (Move (with_dep,id1,id2)) gl
 
 let order_hyps idl gl =
-  refiner (Prim (Order idl)) gl
+  refiner (Order idl) gl
 
 let rec rename_hyp_no_check l gl = match l with
   | [] -> tclIDTAC gl
   | (id1,id2)::l ->
-      tclTHEN (refiner (Prim (Rename (id1,id2))))
+      tclTHEN (refiner (Rename (id1,id2)))
 	(rename_hyp_no_check l) gl
 
 let mutual_fix f n others j gl =
-  with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
+  with_check (refiner (FixRule (f,n,others,j))) gl
 
 let mutual_cofix f others j gl =
-  with_check (refiner (Prim (Cofix (f,others,j)))) gl
+  with_check (refiner (Cofix (f,others,j))) gl
 
 (* Versions with consistency checks *)