Proof_global.start_dependent_proof: properly threads the sigma through the telescope.

Allows for a more refined notion of dependently generated initial goals.

1 files changed, 2 insertions, 2 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 3d5eb20312..60522c54b8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -237,8 +237,8 @@ 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 entry, proofview = Proofview.dependent_init sigma goals in
+let dependent_start goals =
+  let entry, proofview = Proofview.dependent_init goals in
   let pr = {
     proofview;
     entry;