diff options
| author | Hugo Herbelin | 2020-09-02 17:27:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 17:25:16 +0100 |
| commit | 55389f1a1705b5c548161e1e5cc3eb5e34dda41d (patch) | |
| tree | 8340285f440aa45eeaa4fb3f8ca56cbfd7ad1a6d /interp/notation_ops.ml | |
| parent | cd8aefceb03effbda979ea7403c20eaa7ca4cef7 (diff) | |
Using labels to document match_notation_constr.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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') -> |