Imported Upstream version 8.5~beta3+dfsg

1 files changed, 17 insertions, 4 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 828f9fa7..c7aa5bad 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -111,6 +111,8 @@ type proof = {
   shelf : Goal.goal list;
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
+  (* The initial universe context (for the statement) *)
+  initial_euctx : Evd.evar_universe_context
 }
 
 (*** General proof functions ***)
@@ -171,6 +173,12 @@ let is_done p =
 (* spiwack: for compatibility with <= 8.2 proof engine *)
 let has_unresolved_evar p =
   Proofview.V82.has_unresolved_evar p.proofview
+let has_shelved_goals p = not (CList.is_empty (p.shelf))
+let has_given_up_goals p = not (CList.is_empty (p.given_up))
+
+let is_complete p =
+  is_done p && not (has_unresolved_evar p) &&
+  not (has_shelved_goals p) && not (has_given_up_goals p)
 
 (* Returns the list of partial proofs to initial goals *)
 let partial_proof p = Proofview.partial_proof p.entry p.proofview
@@ -271,7 +279,9 @@ let start sigma goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 let dependent_start goals =
   let entry, proofview = Proofview.dependent_init goals in
@@ -280,7 +290,9 @@ let dependent_start goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
@@ -299,9 +311,9 @@ end
 let return p =
   if not (is_done p) then
     raise UnfinishedProof
-  else if not (CList.is_empty (p.shelf)) then
+  else if has_shelved_goals p then
     raise HasShelvedGoals
-  else if not (CList.is_empty (p.given_up)) then
+  else if has_given_up_goals p then
     raise HasGivenUpGoals
   else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
@@ -311,6 +323,7 @@ let return p =
     Proofview.return p.proofview
 
 let initial_goals p = Proofview.initial_goals p.entry
+let initial_euctx p = p.initial_euctx
 
 let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in