Allow proofs to start with dependent goals.

I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.

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