From c2a67e6f1cdd803b46a3ff4dc259c1cc57ade33f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Jul 2015 14:02:50 +0200
Subject: Fixing #4305 (compatibility wrt 8.4 in not interpreting an
 abbreviation not bound to an applied constructor as itself but rather as a
 binding variable as it was the case for non-applied constructor). This was
 broken by e5c02503 while fixed #3483 (Not_found uncaught with a notation to a
 non-constructor).

---
 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 982d9bfe39..8c56d0ccfe 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for =
 	      let (argscs,_) = find_remaining_scopes pats [] g in
 	      Some (g, List.map2 (in_pat_sc env) argscs pats, [])
 	| NApp (NRef g,args) ->
-	      ensure_kind top loc g;
+	      test_kind top g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
 	      let pats1,pats2 = List.chop nvars pats in
-- 
cgit v1.2.3