A slight phase of documentation and uniformization of names of

functions about interpretation, internalization, externalization of
notations.

Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
  (because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
  (because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli

Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
  glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
  (fully implemented) glob_constr_eq

Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.

6 files changed, 133 insertions, 123 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 53497ff0e..4a0130bef 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,10 @@
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
+** Notation_ops **
+
+Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr.
+
 ** Logging and Pretty Printing: **
 
 * Printing functions have been removed from `Pp.mli`, which is now a
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 592f59333..e5ccb76b4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -175,6 +175,10 @@ let add_patt_for_params ind l =
   if !Flags.in_debugger then l else
     Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l
 
+let add_cpatt_for_params ind l =
+  if !Flags.in_debugger then l else
+    Util.List.addn  (Inductiveops.inductive_nparamdecls ind) (PatVar (Loc.ghost,Anonymous)) l
+
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
   let impl_data = extract_impargs_data impl_st in
@@ -299,7 +303,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   with No_match ->
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
-      extern_symbol_pattern scopes vars pat
+      extern_notation_pattern scopes vars pat
 	(uninterp_cases_pattern_notations pat)
     with No_match ->
       match pat with
@@ -382,7 +386,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
       in
       assert (List.is_empty substlist);
       mkPat loc qid (List.rev_append l1 l2')
-and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
@@ -395,9 +399,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
 	| PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id)))
     with
-	No_match -> extern_symbol_pattern allscopes vars t rules
+	No_match -> extern_notation_pattern allscopes vars t rules
 
-let rec extern_symbol_ind_pattern allscopes vars ind args = function
+let rec extern_notation_ind_pattern allscopes vars ind args = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
@@ -405,7 +409,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function
       apply_notation_to_pattern Loc.ghost (IndRef ind)
 	(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
-	No_match -> extern_symbol_ind_pattern allscopes vars ind args rules
+	No_match -> extern_notation_ind_pattern allscopes vars ind args rules
 
 let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
@@ -425,7 +429,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
     with No_match ->
       try
 	if !Flags.raw_print || !print_no_symbol then raise No_match;
-	extern_symbol_ind_pattern scopes vars ind args
+	extern_notation_ind_pattern scopes vars ind args
 	  (uninterp_ind_pattern_notations ind)
     with No_match ->
       let c = extern_reference Loc.ghost vars (IndRef ind) in
@@ -622,7 +626,7 @@ let rec extern inctx scopes vars r =
   try
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
-    extern_symbol scopes vars r'' (uninterp_notations r'')
+    extern_notation scopes vars r'' (uninterp_notations r'')
   with No_match -> match r' with
   | GRef (loc,ref,us) ->
       extern_global loc (select_stronger_impargs (implicits_of_global ref))
@@ -730,9 +734,7 @@ let rec extern inctx scopes vars r =
                   na',
                   Option.map (fun (loc,ind,nal) ->
                               let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
-                              let fullargs =
-                                if !Flags.in_debugger then args else
-                                  Notation_ops.add_patterns_for_params ind args in
+                              let fullargs = add_cpatt_for_params ind args in
                               extern_ind_pattern_in_scope scopes vars ind fullargs
                              ) x))
                 tml
@@ -842,7 +844,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
 
-and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
@@ -917,7 +919,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	  let args = extern_args (extern true) scopes vars args argsscopes in
 	  explicitize loc false argsimpls (None,e) args
       with
-	  No_match -> extern_symbol allscopes vars t rules
+	  No_match -> extern_notation allscopes vars t rules
 
 and extern_recursion_order scopes vars = function
     GStructRec -> CStructRec
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4a451634d..50252a368 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -526,7 +526,7 @@ let rec subst_iterator y t = function
   | GVar (_,id) as x -> if Id.equal id y then t else x
   | x -> map_glob_constr (subst_iterator y t) x
 
-let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
+let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c =
   let (terms,termlists,binders) = subst in
   (* when called while defining a notation, avoid capturing the private binders
      of the expression by variables bound by the notation (see #3892) *)
@@ -649,7 +649,7 @@ let intern_notation intern env lvar loc ntn fullargs =
   let terms = make_subst ids args in
   let termlists = make_subst idsl argslist in
   let binders = make_subst idsbl bll in
-  subst_aconstr_in_glob_constr loc intern lvar
+  instantiate_notation_constr loc intern lvar
     (terms, termlists, binders) (Id.Map.empty, env) c
 
 (**********************************************************************)
@@ -759,7 +759,7 @@ let intern_qualid loc qid intern env lvar us args =
       let subst = (terms, Id.Map.empty, Id.Map.empty) in
       let infos = (Id.Map.empty, env) in
       let projapp = match c with NRef _ -> true | _ -> false in
-      let c = subst_aconstr_in_glob_constr loc intern lvar subst infos c in
+      let c = instantiate_notation_constr loc intern lvar subst infos c in
       let c = match us, c with
       | None, _ -> c
       | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5b49ebcbd..b4cf6e943 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -12,15 +12,103 @@ open Util
 open Names
 open Nameops
 open Globnames
+open Decl_kinds
 open Misctypes
 open Glob_term
 open Glob_ops
 open Mod_subst
 open Notation_term
-open Decl_kinds
 
 (**********************************************************************)
-(* Re-interpret a notation as a glob_constr, taking care of binders     *)
+(* Utilities                                                          *)
+
+let on_true_do b f c = if b then (f c; b) else b
+
+let compare_glob_constr f add t1 t2 = match t1,t2 with
+  | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
+  | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
+  | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
+  | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
+    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+    on_true_do (f ty1 ty2 && f c1 c2) add na1
+  | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
+    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+      on_true_do (f ty1 ty2 && f c1 c2) add na1
+  | GHole _, GHole _ -> true
+  | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
+  | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
+      on_true_do (f b1 b2 && f c1 c2) add na1
+  | (GCases _ | GRec _
+    | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
+  | _,(GCases _ | GRec _
+      | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
+      -> error "Unsupported construction in recursive notations."
+  | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
+    | GHole _ | GSort _ | GLetIn _), _
+      -> false
+
+let rec eq_notation_constr t1 t2 = match t1, t2 with
+| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NVar id1, NVar id2 -> Id.equal id1 id2
+| NApp (t1, a1), NApp (t2, a2) ->
+  eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
+| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2 && b1 == b2
+| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+  let eqpat (p1, t1) (p2, t2) =
+    List.equal cases_pattern_eq p1 p2 &&
+    eq_notation_constr t1 t2
+  in
+  let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
+    let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
+    eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+  in
+  Option.equal eq_notation_constr o1 o2 &&
+  List.equal eqf r1 r2 &&
+  List.equal eqpat p1 p2
+| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+  List.equal Name.equal nas1 nas2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+  eq_notation_constr t1 t2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr u1 u2 &&
+  eq_notation_constr r1 r2
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+  let eq (na1, o1, t1) (na2, o2, t2) =
+    Name.equal na1 na2 &&
+    Option.equal eq_notation_constr o1 o2 &&
+    eq_notation_constr t1 t2
+  in
+  Array.equal Id.equal ids1 ids2 &&
+  Array.equal (List.equal eq) ts1 ts2 &&
+  Array.equal eq_notation_constr us1 us2 &&
+  Array.equal eq_notation_constr rs1 rs2
+| NSort s1, NSort s2 ->
+  Miscops.glob_sort_eq s1 s2
+| NCast (t1, c1), NCast (t2, c2) ->
+  eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
+| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+  | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+  | NRec _ | NSort _ | NCast _), _ -> false
+
+(**********************************************************************)
+(* Re-interpret a notation as a glob_constr, taking care of binders   *)
 
 let name_to_ident = function
   | Anonymous -> Errors.error "This expression should be a simple identifier."
@@ -112,7 +200,7 @@ let glob_constr_of_notation_constr loc x =
     glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x
   in aux () x
 
-(****************************************************************************)
+(******************************************************************************)
 (* Translating a glob_constr into a notation, interpreting recursive patterns *)
 
 let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
@@ -142,94 +230,6 @@ let split_at_recursive_part c =
   | GVar (_,v) when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
   | _ -> outer_iterator, c
 
-let on_true_do b f c = if b then (f c; b) else b
-
-let compare_glob_constr f add t1 t2 = match t1,t2 with
-  | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
-  | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
-  | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
-  | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
-    on_true_do (f ty1 ty2 && f c1 c2) add na1
-  | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
-      on_true_do (f ty1 ty2 && f c1 c2) add na1
-  | GHole _, GHole _ -> true
-  | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
-  | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
-      on_true_do (f b1 b2 && f c1 c2) add na1
-  | (GCases _ | GRec _
-    | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
-  | _,(GCases _ | GRec _
-      | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
-      -> error "Unsupported construction in recursive notations."
-  | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
-    | GHole _ | GSort _ | GLetIn _), _
-      -> false
-
-let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2
-
-let rec eq_notation_constr t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
-| NVar id1, NVar id2 -> Id.equal id1 id2
-| NApp (t1, a1), NApp (t2, a2) ->
-  eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
-| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
-  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
-  eq_notation_constr u1 u2 && b1 == b2
-| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
-  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
-| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
-  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
-| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
-  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
-  eq_notation_constr u1 u2
-| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
-  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
-  let eqpat (p1, t1) (p2, t2) =
-    List.equal cases_pattern_eq p1 p2 &&
-    eq_notation_constr t1 t2
-  in
-  let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
-    let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
-    eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
-  in
-  Option.equal eq_notation_constr o1 o2 &&
-  List.equal eqf r1 r2 &&
-  List.equal eqpat p1 p2
-| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
-  List.equal Name.equal nas1 nas2 &&
-  Name.equal na1 na2 &&
-  Option.equal eq_notation_constr o1 o2 &&
-  eq_notation_constr t1 t2 &&
-  eq_notation_constr u1 u2
-| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
-  eq_notation_constr t1 t2 &&
-  Name.equal na1 na2 &&
-  Option.equal eq_notation_constr o1 o2 &&
-  eq_notation_constr u1 u2 &&
-  eq_notation_constr r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
-  let eq (na1, o1, t1) (na2, o2, t2) =
-    Name.equal na1 na2 &&
-    Option.equal eq_notation_constr o1 o2 &&
-    eq_notation_constr t1 t2
-  in
-  Array.equal Id.equal ids1 ids2 &&
-  Array.equal (List.equal eq) ts1 ts2 &&
-  Array.equal eq_notation_constr us1 us2 &&
-  Array.equal eq_notation_constr rs1 rs2
-| NSort s1, NSort s2 ->
-  Miscops.glob_sort_eq s1 s2
-| NCast (t1, c1), NCast (t2, c2) ->
-  eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
-| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
-  | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NCast _), _ -> false
-
-
 let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
 let check_is_hole id = function GHole _ -> () | t ->
@@ -409,6 +409,7 @@ let notation_constr_of_glob_constr nenv a =
   let () = check_variables nenv found in
   a
 
+(**********************************************************************)
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
@@ -544,7 +545,8 @@ let subst_interpretation subst (metas,pat) =
   let bound = List.map fst metas in
   (metas,subst_notation_constr subst bound pat)
 
-(* Pattern-matching glob_constr and notation_constr *)
+(**********************************************************************)
+(* Pattern-matching a [glob_constr] against a [notation_constr]       *)
 
 let abstract_return_type_context pi mklam tml rtno =
   Option.map (fun rtn ->
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 280ccfd21..576c5b943 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -10,24 +10,28 @@ open Names
 open Notation_term
 open Glob_term
 
-(** Utilities about [notation_constr] *)
+(** {5 Utilities about [notation_constr]} *)
 
-(** Translate a [glob_constr] into a notation given the list of variables
-    bound by the notation; also interpret recursive patterns           *)
+val eq_notation_constr : notation_constr -> notation_constr -> bool
 
-val notation_constr_of_glob_constr : notation_interp_env ->
-  glob_constr -> notation_constr
+(** Substitution of kernel names in interpretation data                *)
 
+val subst_interpretation :
+  Mod_subst.substitution -> interpretation -> interpretation
+                                                
 (** Name of the special identifier used to encode recursive notations  *)
+
 val ldots_var : Id.t
 
-(** Equality of [glob_constr] (warning: only partially implemented) *)
-(** FIXME: nothing to do here *)
-val eq_glob_constr : glob_constr -> glob_constr -> bool
+(** {5 Translation back and forth between [glob_constr] and [notation_constr] *)
 
-val eq_notation_constr : notation_constr -> notation_constr -> bool
+(** Translate a [glob_constr] into a notation given the list of variables
+    bound by the notation; also interpret recursive patterns           *)
+
+val notation_constr_of_glob_constr : notation_interp_env ->
+  glob_constr -> notation_constr
 
-(** Re-interpret a notation as a [glob_constr], taking care of binders     *)
+(** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
 val glob_constr_of_notation_constr_with_binders : Loc.t ->
   ('a -> Name.t -> 'a * Name.t) ->
@@ -36,6 +40,8 @@ val glob_constr_of_notation_constr_with_binders : Loc.t ->
 
 val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 
+(** {5 Matching a notation pattern against a [glob_constr] *)
+
 (** [match_notation_constr] matches a [glob_constr] against a notation
     interpretation; raise [No_match] if the matching fails   *)
 
@@ -55,9 +61,5 @@ val match_notation_constr_ind_pattern :
   ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
     (int * cases_pattern list)
 
-(** Substitution of kernel names in interpretation data                *)
-
-val subst_interpretation :
-  Mod_subst.substitution -> interpretation -> interpretation
+(** {5 Matching a notation pattern against a [glob_constr] *)
 
-val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 72205e2bb..c424fe122 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1217,7 +1217,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
 	   if Array.for_all
 	     (fun l ->
 		let (n',nt',is_defined') = List.nth l i in
-		Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined')
+		Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined')
 	     rels_params
 	   then
 	     l := param::!l