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

---
 tactics/hipattern.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics/hipattern.ml')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 851554b83..15b40b42d 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
 let meta3 = mkmeta 3
-let meta4 = mkmeta 4
 
 let op2bool = function Some _ -> true | None -> false
 
-- 
cgit v1.2.3