diff options
| -rw-r--r-- | plugins/xml/dumptree.ml4 | 3 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 11 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 19 | ||||
| -rw-r--r-- | proofs/refiner.ml | 12 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 26 |
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 *) |