From e497afaccc78e92b71e60878d593273dce0036a1 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 5 Aug 2014 11:53:36 +0200
Subject: Better fix of e5c025

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b5693ebe84..fb232762cd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1179,7 +1179,7 @@ let drop_notations_pattern looked_for =
     | CPatDelimiters (loc, key, e) ->
       in_pat top {env with scopes=find_delimiters_scope loc key::env.scopes;
 	tmp_scope = None} e
-    | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) p
+    | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p
 				 (env.tmp_scope,env.scopes))
     | CPatAtom (loc, Some id) ->
       begin
-- 
cgit v1.2.3