diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_type.ml | 9 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 16 | ||||
| -rw-r--r-- | proofs/refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
5 files changed, 2 insertions, 37 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 4652bac2e..d806d80b8 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -40,14 +40,7 @@ type prim_rule = | Rename of identifier * identifier | Change_evars -type proof_tree = { - goal : goal; - ref : (rule * proof_tree list) option } - -and rule = - | Prim of prim_rule - | Decl_proof of bool - | Daimon +type rule = Prim of prim_rule type compound_rule= | Tactic of tactic_expr * bool diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index d6081e56c..832377e31 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -66,21 +66,7 @@ type prim_rule = in the type of evar] \} \} \} v} *) -(** {6 ... } *) -(** Proof trees. - [ref] = [None] if the goal has still to be proved, - and [Some (r,l)] if the rule [r] was applied to the goal - and gave [l] as subproofs to be completed. - if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof - that the goal can be proven if the goals in [l] are solved. *) -type proof_tree = { - goal : goal; - ref : (rule * proof_tree list) option } - -and rule = - | Prim of prim_rule - | Decl_proof of bool - | Daimon +type rule = Prim of prim_rule type compound_rule= (** the boolean of Tactic tells if the default tactic is used *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 87ba77dc5..9b9b91337 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -35,16 +35,6 @@ let refiner = function {it=sgl; sigma = sigma'}) - | Decl_proof _ -> - failwith "Refiner: should not occur" - - (* Daimon is a canonical unfinished proof *) - - | Daimon -> - fun gls -> - {it=[];sigma=gls.sigma} - - let norm_evar_tac gl = refiner (Prim Change_evars) gl (*********************) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4524fe6a1..80a450bcd 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -109,8 +109,6 @@ let pf_matches = pf_apply Matching.matches_conv (* Tactics handling a list of goals *) (************************************) -type validation_list = proof_tree list -> proof_tree list - type tactic_list = Refiner.tactic_list let first_goal = first_goal diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e7ad5d000..da9aecde9 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -118,8 +118,6 @@ val rename_hyp : (identifier*identifier) list -> tactic (** {6 Tactics handling a list of goals. } *) -type validation_list = proof_tree list -> proof_tree list - type tactic_list = Refiner.tactic_list val first_goal : 'a list sigma -> 'a sigma |