diff options
| author | Pierre Roux | 2020-09-07 11:53:49 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 724966f56caa66a5ddc9a992cf870ebc2efae004 (patch) | |
| tree | 53954c47fd9e400d1e6006d38472c0b858893303 /plugins | |
| parent | 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d (diff) | |
[refman] Rename int to integer
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_class.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac_tactics.mlg | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 35c90444b1..8d197e6056 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg index eb9d9cbdce..e5309ea441 100644 --- a/plugins/ltac/profile_ltac_tactics.mlg +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -55,7 +55,7 @@ END TACTIC EXTEND show_ltac_profile | [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff } -| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } +| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } | [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s } END @@ -74,7 +74,7 @@ END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY | [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff } -| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) } +| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) } END VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY |