Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanup

1 files changed, 3 insertions, 1 deletions

diff --git a/interp/notation.mli b/interp/notation.mli
index 2e92a00a8c..300480ff1c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module ->
 
 val interp_prim_token : Loc.t -> prim_token -> local_scopes ->
   glob_constr * (notation_location * scope_name option)
+
+(* This function returns a glob_const representing a pattern *)
 val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token ->
-  local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option)
+  local_scopes -> glob_constr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)