From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 proofs/clenv.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f9ebc4233..605914a01 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -27,11 +27,6 @@ open Unification
 open Misctypes
 open Sigma.Notations
 
-(* Abbreviations *)
-
-let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
-
 (******************************************************************)
 (* Clausal environments *)
 
-- 
cgit v1.2.3