diff options
| author | Pierre Roux | 2020-09-12 09:15:06 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-10-30 14:18:21 +0100 |
| commit | da72fafac3b5b4b21330cd097f5728cbc127aea4 (patch) | |
| tree | 294df4923e6bdca5d66d8c10fbb1c8a20d994148 /interp/constrintern.ml | |
| parent | 3a25b967a944fe37e1ad54e54a904d90311ef381 (diff) | |
Renaming Numeral into Number
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 959b61a3d7..5fb6664dd6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1570,11 +1570,11 @@ let rec subst_pat_iterator y t = DAst.(map (function | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl))) let is_non_zero c = match c with -| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) +| { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p) | _ -> false let is_non_zero_pat c = match c with -| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) +| { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p) | _ -> false let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref @@ -1689,8 +1689,8 @@ let drop_notations_pattern looked_for genv = let (argscs1,_) = find_remaining_scopes expl_pl pl g in DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a -> - let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in - let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in + let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in + let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Number (SMinus,p)) scopes in rcp_of_glob scopes pat | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) -> in_pat top scopes a @@ -2006,8 +2006,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GLetIn (na.CAst.v, inc1, int, intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) | CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a -> - let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in - intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) + let p = match a.CAst.v with CPrim (Number (_, p)) -> p | _ -> assert false in + intern env (CAst.make ?loc @@ CPrim (Number (SMinus,p))) | CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a | CNotation (_,ntn,args) -> let c = intern_notation intern env ntnvars loc ntn args in |