From 1556c6b8f77d16814ff1c53fb14fc9b06574ec4b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 24 Oct 2014 17:35:05 +0200
Subject: Remove an ununsed pattern and commented code in the kernel.
 Reestablish completeness in conversion when Opaque primitive projections are
 used.

---
 kernel/context.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/context.ml')

diff --git a/kernel/context.ml b/kernel/context.ml
index 6b5a6cdb9..e43e08865 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -80,7 +80,7 @@ let rel_context_tags ctx =
   let rec aux l = function
   | [] -> l
   | (_,Some _,_)::ctx -> aux (true::l) ctx
-  | (_,None _,_)::ctx -> aux (false::l) ctx
+  | (_,None,_)::ctx -> aux (false::l) ctx
   in aux [] ctx
 
 (*s Signatures of named hypotheses. Used for section variables and
-- 
cgit v1.2.3