diff options
| author | Vincent Laporte | 2018-09-07 11:18:28 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:12 +0000 |
| commit | 4be2dd481c783bed7c09086b647d860e42b7ea9f (patch) | |
| tree | dfd9a32619175eedb084915ed53d56c356d55174 /plugins | |
| parent | 38be62b56799933cdfc783d4e538963c3aa59fef (diff) | |
Retroknowledge.KInt31: remove the (unused) group parameter
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 38600695dc..a9133512e0 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -345,11 +345,7 @@ let pr_r_int31_field i31f = let pr_retroknowledge_field f = match f with - (* | Retroknowledge.KEq -> str "equality" - | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf - | Retroknowledge.KN nf -> pr_r_n_field () () () nf *) - | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++ - spc () ++ str "in " ++ qs group + | Retroknowledge.KInt31 i31f -> pr_r_int31_field i31f VERNAC ARGUMENT EXTEND retroknowledge_int31 PRINTED BY pr_r_int31_field @@ -381,8 +377,5 @@ END VERNAC ARGUMENT EXTEND retroknowledge_field PRINTED BY pr_retroknowledge_field -(*| [ "equality" ] -> [ Retroknowledge.KEq ] -| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ] -| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*) -| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ] +| [ retroknowledge_int31 (i) ] -> [ Retroknowledge.KInt31 i ] END |