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/notation_ops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 599317b585..cfab9d1d98 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1380,9 +1380,9 @@ and match_disjunctive_equations u alp metas sigma {CAst.v=(ids,disjpatl1,rhs1)}
       (alp,sigma) disjpatl1 disjpatl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-let match_notation_constr u c vars (metas,pat) =
+let match_notation_constr ~print_univ c ~vars (metas,pat) =
   let terms,termlists,binders,binderlists =
-    match_ false u (vars,([],[])) metas ([],[],[],[]) c pat in
+    match_ false print_univ (vars,([],[])) metas ([],[],[],[]) c pat in
   (* Turning substitution based on binding/constr distinction into a
      substitution based on entry productions *)
   List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') ->
-- 
cgit v1.2.3