Merge PR #8115: Support for custom entries in notations (take 2, feature part)

1 files changed, 5 insertions, 5 deletions

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index f038b5be1a..58fa221b16 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -53,18 +53,18 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const
 exception No_match
 
 val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
-      ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list *
-      ('a cases_pattern_disjunction_g * subscopes) list *
-      ('a extended_glob_local_binder_g list * subscopes) list
+      ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
+      ('a cases_pattern_disjunction_g * extended_subscopes) list *
+      ('a extended_glob_local_binder_g list * extended_subscopes) list
 
 val match_notation_constr_cases_pattern :
   'a cases_pattern_g -> interpretation ->
-  (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+  (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
     (int * 'a cases_pattern_g list)
 
 val match_notation_constr_ind_pattern :
   inductive -> 'a cases_pattern_g list -> interpretation ->
-  (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+  (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
     (int * 'a cases_pattern_g list)
 
 (** {5 Matching a notation pattern against a [glob_constr]} *)