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).
---
 lib/monad.ml         | 11 +++++++++++
 lib/monad.mli        |  3 +++
 proofs/proofview.ml  |  4 ++++
 proofs/proofview.mli |  4 ++++
 tactics/ftactic.ml   | 23 +++++++++++++++++++----
 5 files changed, 41 insertions(+), 4 deletions(-)

diff --git a/lib/monad.ml b/lib/monad.ml
index a1714a41b3..2e55e9698c 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -64,6 +64,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
@@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
       | a::b::l -> f a >> f b >> iter f l
 
 
+    let rec map_filter f = function
+      | [] -> return []
+      | a::l ->
+        f a >>= function
+        | None -> map_filter f l
+        | Some b ->
+          map_filter f l >>= fun filtered ->
+          return (b::filtered)
 
     let rec fold_left2 r f x l1 l2 =
       match l1,l2 with
diff --git a/lib/monad.mli b/lib/monad.mli
index c8655efa04..f7de71f53a 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -66,6 +66,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
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
 
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index 8e42dcba74..418dacb48b 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
   | Uniform x ->
     (** We dispatch the uniform result on each goal under focus, as we know
         that the [m] argument was actually dependent. *)
-    Proofview.Goal.goals >>= fun l ->
-    let ans = List.map (fun _ -> x) l in
+    Proofview.Goal.goals >>= fun goals ->
+    let ans = List.map (fun g -> (g,x)) goals in
     Proofview.tclUNIT ans
-  | Depends l -> Proofview.tclUNIT l
+  | Depends l ->
+    Proofview.Goal.goals >>= fun goals ->
+    Proofview.tclUNIT (List.combine goals l)
+  in
+  (* After the tactic has run, some goals which were previously
+     produced may have been solved by side effects. The values
+     attached to such goals must be discarded, otherwise the list of
+     result would not have the same length as the list of focused
+     goals, which is an invariant of the [Ftactic] module. It is the
+     reason why a goal is attached to each result above. *)
+  let filter (g,x) =
+    g >>= fun g ->
+    Proofview.Goal.unsolved g >>= function
+    | true -> Proofview.tclUNIT (Some x)
+    | false -> Proofview.tclUNIT None
   in
   Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
-  Proofview.tclUNIT (Depends (List.concat l))
+  Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered ->
+  Proofview.tclUNIT (Depends filtered)
 
 let nf_enter f =
   bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
-- 
cgit v1.2.3


From 009718d9d0130a967261ae5d2484985522fc2f7c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 10 Oct 2016 10:58:09 +0200
Subject: Add test file for #4416.

---
 test-suite/bugs/closed/4416.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4416.v

diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
new file mode 100644
index 0000000000..b97a8ce640
--- /dev/null
+++ b/test-suite/bugs/closed/4416.v
@@ -0,0 +1,3 @@
+Goal exists x, x.
+unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
+(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
-- 
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.
---
 kernel/entries.mli            |  7 ++++++-
 kernel/safe_typing.ml         |  7 -------
 proofs/proofview.ml           | 28 ++++++++++++++++++++++++++--
 test-suite/bugs/closed/4863.v | 32 ++++++++++++++++++++++++++++++++
 4 files changed, 64 insertions(+), 10 deletions(-)
 create mode 100644 test-suite/bugs/closed/4863.v

diff --git a/kernel/entries.mli b/kernel/entries.mli
index f94068f31e..8e8e97d615 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -97,7 +97,12 @@ type module_entry =
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type seff_env =
+  [ `Nothing
+  (* The proof term and its universes.
+     Same as the constant_body's but not in an ephemeron *)
+  | `Opaque of Constr.t * Univ.universe_context_set ]
 
 type side_eff =
   | SEsubproof of constant * Declarations.constant_body * seff_env
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 927278965f..8b28cd87bd 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -222,13 +222,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
-let constant_entry_of_private_constant = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-      [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-      List.map (fun (_,kn,cb,eff_env) ->
-        kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
-
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
   { Entries.from_env = CEphemeron.create env.revstruct;
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 *)
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
new file mode 100644
index 0000000000..e884355fde
--- /dev/null
+++ b/test-suite/bugs/closed/4863.v
@@ -0,0 +1,32 @@
+Require Import Classes.DecidableClass.
+
+Inductive Foo : Set :=
+| foo1 | foo2.
+
+Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Proof.
+  intros P H.
+  refine (Build_Decidable _ (if H then true else false) _).
+  intuition congruence.
+Qed.
+
+Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+
+Goal forall (a b : Foo), {a=b}+{a<>b}.
+intros.
+abstract (abstract (decide equality)). (*abstract works here*)
+Qed.
+
+Check ltac:(abstract (exact I)) : True.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split. typeclasses eauto. typeclasses eauto. Qed.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split.
+refine _.
+refine _.
+Defined.
+(*fails*)
-- 
cgit v1.2.3