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

(limited to 'proofs/clenv.ml')

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
 
-- 
cgit v1.2.3