aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:29 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:29 +0000
commita0057a6657f5615c3d3448fae10b26a968d30fe1 (patch)
tree0617fe67223c46d7fd1f17c83068ee6ca98d74ab
parent4a8188a2b460ab014379c508abac933690b48555 (diff)
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
-rw-r--r--plugins/xml/dumptree.ml43
-rw-r--r--proofs/proof_type.ml11
-rw-r--r--proofs/proof_type.mli19
-rw-r--r--proofs/refiner.ml12
-rw-r--r--proofs/tacmach.ml26
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 *)