Merge remote-tracking branch 'forge/v8.5'

2 files changed, 25 insertions, 14 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 5eebd0d9d3..c766f3fab3 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -328,7 +328,7 @@ let check_exist =
 
 let standard_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted (id,k,pe) ->
+  | Admitted (id,k,pe,_) ->
       admit (id,k,pe) hook ();
       Pp.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
@@ -347,8 +347,8 @@ let standard_proof_terminator compute_guard hook =
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted (id,k,pe) ->
-      admit (id,k,pe) (hook None) ();
+  | Admitted (id,k,pe,ctx) ->
+      admit (id,k,pe) (hook (Some ctx)) ();
       Pp.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff, exports = match opaque with
@@ -480,14 +480,13 @@ let save_proof ?proof = function
               error "Admitted requires an explicit statement";
             let typ = Option.get const_entry_type in
             let ctx = Evd.evar_context_universe_context universes in
-            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None))
+            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
         | None ->
             let id, k, typ = Pfedit.current_proof_statement () in
-            let ctx =
-              let evd, _ = Pfedit.get_current_goal_context () in
-              Evd.universe_context evd in
             (* This will warn if the proof is complete *)
-            let pproofs,_ = Proof_global.return_proof ~allow_partial:true () in
+            let pproofs, universes =
+              Proof_global.return_proof ~allow_partial:true () in
+            let ctx = Evd.evar_context_universe_context universes in
             let sec_vars =
               match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
@@ -497,7 +496,7 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None))
+            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes)
       in
       Proof_global.get_terminator() pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/stm/stm.ml b/stm/stm.ml
index fa3ffc7c6e..373fd0ba39 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -671,11 +671,22 @@ end = struct (* {{{ *)
   let assign id what =
     if VCS.get_state id <> None then () else
     try match what with
-    | `Full s -> VCS.set_state id s
+    | `Full s ->
+         let s =
+           try
+            let prev = (VCS.visit id).next in
+            if is_cached prev
+            then { s with proof = 
+              Proof_global.copy_terminators
+                ~src:(get_cached prev).proof ~tgt:s.proof }
+            else s
+           with VCS.Expired -> s in
+         VCS.set_state id s
     | `Proof(ontop,(pstate,counters)) ->
          if is_cached ontop then
            let s = get_cached ontop in
-           let s = { s with proof = pstate } in
+           let s = { s with proof =
+             Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
                (Summary.surgery_summary
@@ -1119,7 +1130,7 @@ end = struct (* {{{ *)
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_warning (str "Sending back a fat state");
+          msg_warning (str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
@@ -2328,9 +2339,9 @@ let edit_at id =
     VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
       (Option.default brname bn)
       (no_edit brinfo.VCS.kind);
-      VCS.print ();
     VCS.delete_cluster_of id;
     VCS.gc ();
+    VCS.print ();
     Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
@@ -2368,7 +2379,8 @@ let edit_at id =
           end else begin
             anomaly(str"Cannot leave an `Edit branch open")
           end
-      | false, None, _ -> backto id None
+      | false, None, Some(_,bn) -> backto id (Some bn)
+      | false, None, None -> backto id None
     in
     VCS.print ();
     rc