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.mli | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'proofs/clenv.mli')

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