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 +-
 test-suite/bugs/closed/4305.v | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4305.v

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
diff --git a/test-suite/bugs/closed/4305.v b/test-suite/bugs/closed/4305.v
new file mode 100644
index 0000000000..39fc02d22b
--- /dev/null
+++ b/test-suite/bugs/closed/4305.v
@@ -0,0 +1,17 @@
+(* Check fallback when an abbreviation is not interpretable as a pattern *)
+
+Notation foo := Type.
+
+Definition t :=
+  match 0 with
+  | S foo => foo
+  | _ => 0
+  end.
+
+Notation bar := (option Type).
+
+Definition u :=
+  match 0 with
+  | S bar => bar
+  | _ => 0
+  end.
-- 
cgit v1.2.3