From 53e19f76624b7a18792af799e970e9478f8e90a9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 16 Jun 2020 17:09:40 +0200
Subject: Fix #11121: Simultaneous definition of term and notation in custom
 grammar

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

(limited to 'interp/dumpglob.ml')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 57ec708b07..d57c05788d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -207,7 +207,7 @@ let cook_notation (from,df) sc =
   done;
   let df = Bytes.sub_string ntn 0 !j in
   let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in
-  let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in
+  let from_df_sc = match from with Constrexpr.InCustomEntry from -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntry -> ":" ^ df_sc in
   from_df_sc
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
-- 
cgit v1.2.3