3 files changed, 2 insertions, 13 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4893758ab3..31bc698830 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -713,12 +713,6 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
 
-let make_clenv_binding_env_apply env sigma n =
-  make_clenv_binding_gen true n env sigma
-
-let make_clenv_binding_env env sigma =
-  make_clenv_binding_gen false None env sigma
-
 let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
 let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index d4905de434..a72c8c5e1f 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -75,17 +75,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 (** the arity of the lemma is fixed
    the optional int tells how many prods of the lemma have to be used
    use all of them if None *)
-val make_clenv_binding_env_apply :
-  env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
-   clausenv
-
 val make_clenv_binding_apply :
   env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
    clausenv
 
-val make_clenv_binding_env :
-  env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
-
 val make_clenv_binding :
   env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
 
diff --git a/proofs/refine.ml b/proofs/refine.ml
index dcff5e2b6c..ac410a958f 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -75,6 +75,8 @@ let generic_refine ~typecheck f gl =
   let future_goals, sigma = Evd.pop_future_goals sigma in
   (* Select the goals *)
   let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in
+  let shelf = Evd.shelf sigma in
+  let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ List.mem ev shelf) future_goals in
   (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->