From c70fe0c63238128a6bb98b9fa75445c4b71c7af5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 10 Oct 2016 10:53:51 +0200
Subject: Fix #4416: - Incorrect "Error: Incorrect number of goals"

In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.

See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
---
 proofs/proofview.ml  | 4 ++++
 proofs/proofview.mli | 4 ++++
 2 files changed, 8 insertions(+)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 483f82113d..ae7e2b79a8 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1016,6 +1016,10 @@ module Goal = struct
     in
     tclUNIT (CList.map_filter map step.comb)
 
+  let unsolved { self=self } =
+    tclEVARMAP >>= fun sigma ->
+    tclUNIT (not (Option.is_empty (advance sigma self)))
+
   (* compatibility *)
   let goal { self=self } = self
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 2157459f46..1a367f4eac 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -466,6 +466,10 @@ module Goal : sig
   (** Recover the list of current goals under focus, without evar-normalization *)
   val goals : [ `LZ ] t tactic list tactic
 
+  (** [unsolved g] is [true] if [g] is still unsolved in the current
+      proof state. *)
+  val unsolved : 'a t -> bool tactic
+
   (** Compatibility: avoid if possible *)
   val goal : [ `NF ] t -> Evar.t
 
-- 
cgit v1.2.3


From b247761476c4b36f0945c19c23c171ea57701178 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 18:02:25 +0200
Subject: Fix for bug #4863, update the Proofview's env with

side_effects. Partial solution to the handling of side effects
in proofview.
---
 proofs/proofview.ml | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ae7e2b79a8..91905be627 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1071,6 +1071,23 @@ struct
   let (pr_constrv,pr_constr) =
     Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
+  (* Get the side-effect's constant declarations to update the monad's
+   * environmnent *)
+  let add_if_undefined kn cb env =
+    try ignore(Environ.lookup_constant kn env); env
+    with Not_found -> Environ.add_constant kn cb env
+
+  (* Add the side effects to the monad's environment, if not already done. *)
+  let add_side_effect env = function
+    | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+      add_if_undefined kn cb env
+    | { Entries.eff = Entries.SEscheme (l,_) } ->
+      List.fold_left (fun env (_,kn,cb,eff_env) ->
+          add_if_undefined kn cb env) env l
+
+  let add_side_effects env effects =
+    List.fold_left (fun env eff -> add_side_effect env eff) env effects
+
   let refine ?(unsafe = true) f = Goal.enter begin fun gl ->
     let sigma = Goal.sigma gl in
     let env = Goal.env gl in
@@ -1083,6 +1100,10 @@ struct
     let (sigma, c) = f (Evd.reset_future_goals sigma) in
     let evs = Evd.future_goals sigma in
     let evkmain = Evd.principal_future_goal sigma in
+    (** Redo the effects in sigma in the monad's env *)
+    let privates_csts = Evd.eval_side_effects sigma in
+    let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
+    let env = add_side_effects env sideff in
     (** Check that the introduced evars are well-typed *)
     let fold accu ev = typecheck_evar ev env accu in
     let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
@@ -1109,8 +1130,11 @@ struct
     let comb = undefined sigma (CList.rev evs) in
     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"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
-    Pv.modify (fun ps -> { ps with solution = sigma; comb; })
+    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++
+                                                 Hook.get pr_constrv env sigma c)))) >>
+      (** We reset the logical environment extended with the effects. *)
+      Env.set (Environ.reset_context env) >>
+      Pv.modify (fun ps -> { ps with solution = sigma; comb; })
   end
 
   (** Useful definitions *)
-- 
cgit v1.2.3