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 | |
| parent | cd8aefceb03effbda979ea7403c20eaa7ca4cef7 (diff) | |
Using labels to document match_notation_constr.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 2 | ||||
| -rw-r--r-- | interp/reserve.ml | 2 |
4 files changed, 6 insertions, 6 deletions
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) -> 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') -> diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 68f25e1600..0d4bdf3e85 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -63,7 +63,7 @@ exception No_match val print_parentheses : bool ref -val match_notation_constr : bool -> 'a glob_constr_g -> Id.Set.t -> interpretation -> +val match_notation_constr : print_univ:bool -> 'a glob_constr_g -> vars:Id.Set.t -> interpretation -> ((Id.Set.t * 'a glob_constr_g) * extended_subscopes) list * ((Id.Set.t * 'a glob_constr_g list) * extended_subscopes) list * ((Id.Set.t * 'a cases_pattern_disjunction_g) * extended_subscopes) list * diff --git a/interp/reserve.ml b/interp/reserve.ml index ee0e1940cb..274d3655d3 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -119,7 +119,7 @@ let revert_reserved_type t = then I've introduced a bug... *) let filter _ pat = try - 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 No_match -> false in |