2 files changed, 15 insertions, 7 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 48d78d8589..dade69865c 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -462,18 +462,22 @@ let clenv_constrain_dep_args hyps_only bl clenv =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen hyps_only n gls (c,t) = function
+let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
   | ImplicitBindings largs ->
-      let clause = mk_clenv_from_n gls n (c,t) in
+      let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args lbind clause
+      let clause = mk_clenv_from_env env sigma n 
+	(c,rename_bound_vars_as_displayed [] t) 
+      in clenv_match_args lbind clause
   | NoBindings ->
-      mk_clenv_from_n gls n (c,t)
+      mk_clenv_from_env env sigma n (c,t)
 
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
-let make_clenv_binding = make_clenv_binding_gen false None
+let make_clenv_binding_env_apply env sigma n =
+  make_clenv_binding_gen true n env sigma
+	
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma
+let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index afda6d9315..209024c9c4 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -97,6 +97,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 -> constr * constr -> constr bindings ->
+   clausenv
+
 val make_clenv_binding_apply :
   Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
    clausenv