Merge branch 'v8.5'

1 files changed, 28 insertions, 11 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f629539079..9ee7df14c8 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -33,7 +33,7 @@ type entry = (Term.constr * Term.types) list
 let proofview p =
   p.comb , p.solution
 
-let compact el { comb; solution } =
+let compact el ({ solution } as pv) =
   let nf = Evarutil.nf_evar solution in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
@@ -46,7 +46,7 @@ let compact el { comb; solution } =
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
-  new_el, { comb; solution = new_solution }
+  new_el, { pv with solution = new_solution; }
 
 
 (** {6 Starting and querying a proof view} *)
@@ -63,7 +63,7 @@ let dependent_init =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   (* Main routine *)
   let rec aux = function
-  | TNil sigma -> [], { solution = sigma; comb = []; }
+  | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
     let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
@@ -71,7 +71,7 @@ let dependent_init =
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
-    entry, { solution = sol; comb = gl :: comb; }
+    entry, { solution = sol; comb = gl :: comb; shelf = [] }
   in
   fun t ->
     let entry, v = aux t in
@@ -235,6 +235,9 @@ let apply env t sp =
   match ans with
   | Nil (e, info) -> iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
+    let (status, gaveup) = status in
+    let status = (status, state.shelf, gaveup) in
+    let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
 
@@ -581,7 +584,7 @@ let shelve =
   Comb.get >>= fun initial ->
   Comb.set [] >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
-  Shelf.put initial
+  Shelf.modify (fun gls -> gls @ initial)
 
 
 (** [contained_in_info e evi] checks whether the evar [e] appears in
@@ -620,7 +623,7 @@ let shelve_unifiable =
   let (u,n) = partition_unifiable initial.solution initial.comb in
   Comb.set n >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
-  Shelf.put u
+  Shelf.modify (fun gls -> gls @ u)
 
 (** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
@@ -642,6 +645,20 @@ let unshelve l p =
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
 
+let with_shelf tac =
+  let open Proof in
+  Pv.get >>= fun pv ->
+  let { shelf; solution } = pv in
+  Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >>
+  tac >>= fun ans ->
+  Pv.get >>= fun npv ->
+  let { shelf = gls; solution = sigma } = npv in
+  let gls' = Evd.future_goals sigma in
+  let fgoals = Evd.future_goals solution in
+  let pgoal = Evd.principal_future_goal solution in
+  let sigma = Evd.restore_future_goals sigma fgoals pgoal in
+  Pv.set { npv with shelf; solution = sigma } >>
+  tclUNIT (CList.rev_append gls' gls, ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
@@ -870,7 +887,7 @@ module Unsafe = struct
   let tclSETGOALS = Comb.set
 
   let tclEVARSADVANCE evd =
-    Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
+    Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
   let tclEVARUNIVCONTEXT ctx = 
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
@@ -1121,7 +1138,7 @@ struct
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
-    Pv.set { solution = sigma; comb; }
+    Pv.modify (fun ps -> { ps with solution = sigma; comb; })
   end }
 
   (** Useful definitions *)
@@ -1204,7 +1221,7 @@ module V82 = struct
       let sgs = CList.flatten goalss in
       let sgs = undefined evd sgs in
       InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
-      Pv.set { solution = evd; comb = sgs; }
+      Pv.set { ps with solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let (e, info) = Errors.push e in
       tclZERO ~info e
@@ -1216,7 +1233,7 @@ module V82 = struct
     Pv.modify begin fun ps ->
     let map g s = GoalV82.nf_evar s g in
     let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
-    { solution = evd; comb = goals; }
+    { ps with solution = evd; comb = goals; }
     end
       
   let has_unresolved_evar pv =
@@ -1261,7 +1278,7 @@ module V82 = struct
 
   let of_tactic t gls =
     try
-      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
+      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
       let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
     with Logic_monad.TacticFailure e as src ->