From 55389f1a1705b5c548161e1e5cc3eb5e34dda41d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Sep 2020 17:27:15 +0200
Subject: Using labels to document match_notation_constr.

---
 interp/constrextern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bfeef59eaf..8d3cf7274a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -85,7 +85,7 @@ let is_reserved_type na t =
   | Name id ->
     try
       let pat = Reserve.find_reserved_type id in
-      let _ = match_notation_constr false t Id.Set.empty ([],pat) in
+      let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([],pat) in
       true
     with Not_found | No_match -> false
 
@@ -1273,7 +1273,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
           | AppBoundedNotation _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
-          match_notation_constr !print_universes t vars pat in
+          match_notation_constr ~print_univ:(!print_universes) t ~vars pat in
         (* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (_,ntn as specific_ntn) ->
-- 
cgit v1.2.3