aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 3d5eb2031..60522c54b 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;