From c893dc56fa579c8d1f6ea3a1859681bb316d9979 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 15:55:15 +0200
Subject: Accept section variables in notations with mixed terms and binders.

---
 pretyping/glob_ops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index bdf3495479..f42c754ef5 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -523,6 +523,7 @@ let rec cases_pattern_of_glob_constr env na c =
     | Anonymous -> PatVar (Name id)
     end
   | GHole (_,_,_) -> PatVar na
+  | GRef (GlobRef.VarRef id,_) -> PatVar (Name id)
   | GRef (GlobRef.ConstructRef cstr,_) -> PatCstr (cstr,[],na)
   | GApp (c, l) ->
     begin match DAst.get c with
-- 
cgit v1.2.3