diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 6 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 9 |
2 files changed, 11 insertions, 4 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7895bfac93..f3658ad4b6 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -31,10 +31,12 @@ open Safe_typing (* Mainly contributed by C. Murthy *) (*********************************************************************) +type lemma_possible_guards = int list list + type proof_topstate = { mutable top_end_tac : tactic option; top_init_tac : tactic option; - top_compute_guard : bool; + top_compute_guard : lemma_possible_guards; top_goal : goal; top_strength : Decl_kinds.goal_kind; top_hook : declaration_hook } @@ -252,7 +254,7 @@ let set_end_tac tac = (* Modifying the current prooftree *) (*********************************************************************) -let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook = +let start_proof na str sign concl ?init_tac ?(compute_guard=[]) hook = let top_goal = mk_goal sign concl None in let ts = { top_end_tac = None; diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 6acf1ff780..acb852471d 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -78,9 +78,12 @@ val get_undo : unit -> int option systematically apply at initialization time (e.g. to start the proof of mutually dependent theorems) *) +type lemma_possible_guards = int list list + val start_proof : identifier -> goal_kind -> named_context_val -> constr -> - ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit + ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> + declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning or fails if no proof is focused *) @@ -108,7 +111,9 @@ val suspend_proof : unit -> unit it also tells if the guardness condition has to be inferred. *) val cook_proof : (Refiner.pftreestate -> unit) -> - identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook) + identifier * + (Entries.definition_entry * lemma_possible_guards * goal_kind * + declaration_hook) (* To export completed proofs to xml *) val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit |