diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-05-15 10:40:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:43:29 +0200 |
| commit | 63ac502a4ea7f5c81346deeecfcf0d69d063a130 (patch) | |
| tree | 0ed99e6fa129b8a7413859b7b57073ca5d2dc388 /ltac | |
| parent | 818422ad1ff602d692f712733517e26db013bfa8 (diff) | |
Fixing printing of Register retroknowledge.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extraargs.ml4 | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index e6d0a9c69..8185a14d9 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -292,7 +292,23 @@ let pr_r_int31_field i31f = | Retroknowledge.Int31PhiInv -> str "phi inv" | Retroknowledge.Int31Plus -> str "plus" | Retroknowledge.Int31Times -> str "times" - | _ -> assert false + | Retroknowledge.Int31Constructor -> assert false + | Retroknowledge.Int31PlusC -> str "plusc" + | Retroknowledge.Int31PlusCarryC -> str "pluscarryc" + | Retroknowledge.Int31Minus -> str "minus" + | Retroknowledge.Int31MinusC -> str "minusc" + | Retroknowledge.Int31MinusCarryC -> str "minuscarryc" + | Retroknowledge.Int31TimesC -> str "timesc" + | Retroknowledge.Int31Div21 -> str "div21" + | Retroknowledge.Int31Div -> str "div" + | Retroknowledge.Int31Diveucl -> str "diveucl" + | Retroknowledge.Int31AddMulDiv -> str "addmuldiv" + | Retroknowledge.Int31Compare -> str "compare" + | Retroknowledge.Int31Head0 -> str "head0" + | Retroknowledge.Int31Tail0 -> str "tail0" + | Retroknowledge.Int31Lor -> str "lor" + | Retroknowledge.Int31Land -> str "land" + | Retroknowledge.Int31Lxor -> str "lxor" let pr_retroknowledge_field f = match f with @@ -300,7 +316,7 @@ let pr_retroknowledge_field f = | 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) ++ - str "in " ++ str group + spc () ++ str "in " ++ qs group VERNAC ARGUMENT EXTEND retroknowledge_nat PRINTED BY pr_r_nat_field |