diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 2 | ||||
| -rw-r--r-- | plugins/syntax/int63_syntax.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/numeral.ml | 12 |
4 files changed, 11 insertions, 11 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 97d75261c5..ecfe6c1664 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -121,8 +121,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with end | _ -> ElimOnConstr clbind -let mkNumeral n = - Numeral (NumTok.Signed.of_int_string (string_of_int n)) +let mkNumber n = + Number (NumTok.Signed.of_int_string (string_of_int n)) let mkTacCase with_evar = function | [(clear,ElimOnConstr cl),(None,None),None],None -> @@ -130,7 +130,7 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(CAst.make @@ CPrim (mkNumeral n), + (clear,(CAst.make @@ CPrim (mkNumber n), NoBindings))) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 35fecfb0a5..ccdf5fa68e 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -350,7 +350,7 @@ let interp_index ist gl idx = | Some c -> let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc (None, []) with - | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n -> + | Constrexpr.Number n, _ when NumTok.Signed.is_int n -> int_of_string (NumTok.Signed.to_string n) | _ -> raise Not_found end diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml index 5f4db8e800..73a9341145 100644 --- a/plugins/syntax/int63_syntax.ml +++ b/plugins/syntax/int63_syntax.ml @@ -50,7 +50,7 @@ let _ = enable_prim_token_interpretation { pt_local = false; pt_scope = int63_scope; - pt_interp_info = NumeralNotation o; + pt_interp_info = NumberNotation o; pt_required = (int63_path, int63_module); pt_refs = []; pt_in_match = false }) diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 313798b102..8635f39f1a 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -90,7 +90,7 @@ let locate_number () = int = int_ty; decimal = unsafe_locate_ind q_dec; hexadecimal = unsafe_locate_ind q_hex; - numeral = unsafe_locate_ind q_num; + number = unsafe_locate_ind q_num; } in Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, num_ty, mkRefC q_num, mkRefC q_dec) @@ -151,8 +151,8 @@ let vernac_number_notation local ty f g scope opts = | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Numeral num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Numeral num_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct @@ -176,8 +176,8 @@ let vernac_number_notation local ty f g scope opts = | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Numeral num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Numeral num_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct @@ -209,7 +209,7 @@ let vernac_number_notation local ty f g scope opts = let i = { pt_local = local; pt_scope = scope; - pt_interp_info = NumeralNotation o; + pt_interp_info = NumberNotation o; pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; pt_refs = constructors; pt_in_match = true } |