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 /plugins/ltac | |
| parent | 3a25b967a944fe37e1ad54e54a904d90311ef381 (diff) | |
Renaming Numeral into Number
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 6 |
1 files changed, 3 insertions, 3 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 *) |