diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 35166def0..9e6045661 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -233,6 +233,14 @@ let start sigma goals = shelf = [] ; given_up = [] } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr +let dependent_start sigma goals = + let pr = { + proofview = Proofview.dependent_init sigma goals ; + focus_stack = [] ; + shelf = [] ; + given_up = [] } in + let number_of_goals = List.length (Proofview.initial_goals pr.proofview) in + _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr exception UnfinishedProof exception HasShelvedGoals |