From cd9ca8a10e79ed07836a0c212524bc5a3553e2ea Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Sep 2020 13:36:53 +0200
Subject: Remove dead code in clenv-generating functions.

The *_env functions used to be different, but now they were just redundant
with their direct equivalent.
---
 proofs/clenv.ml  | 6 ------
 proofs/clenv.mli | 7 -------
 2 files changed, 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
 
-- 
cgit v1.2.3