From eef907ed0a200e912ab2eddc0fcea41b5f61c145 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Mon, 25 Nov 2013 19:55:57 +0100
Subject: Allow proofs to start with dependent goals.

I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
---
 proofs/proof.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'proofs/proof.ml')

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
-- 
cgit v1.2.3