From 4be2dd481c783bed7c09086b647d860e42b7ea9f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 11:18:28 +0200
Subject: Retroknowledge.KInt31: remove the (unused) group parameter

---
 plugins/ltac/extraargs.ml4 | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

(limited to 'plugins/ltac/extraargs.ml4')

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
-- 
cgit v1.2.3


From 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 12:22:17 +0200
Subject: Retroknowledge: simpler parsing rules

---
 plugins/ltac/extraargs.ml4 | 68 ----------------------------------------------
 1 file changed, 68 deletions(-)

(limited to 'plugins/ltac/extraargs.ml4')

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index a9133512e0..f4555509cc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -311,71 +311,3 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
 ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
 | [ local_test_lpar_id_colon(x) ] -> [ () ]
 END
-
-(* spiwack: the print functions are incomplete, but I don't know what they are
-	used for *)
-let pr_r_int31_field i31f =
-  str "int31 " ++
-  match i31f with
-    | Retroknowledge.Int31Bits -> str "bits"
-    | Retroknowledge.Int31Type -> str "type"
-    | Retroknowledge.Int31Twice -> str "twice"
-    | Retroknowledge.Int31TwicePlusOne -> str "twice plus one"
-    | Retroknowledge.Int31Phi -> str "phi"
-    | Retroknowledge.Int31PhiInv -> str "phi inv"
-    | Retroknowledge.Int31Plus -> str "plus"
-    | Retroknowledge.Int31Times -> str "times"
-    | 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
-  | Retroknowledge.KInt31 i31f -> pr_r_int31_field i31f
-
-VERNAC ARGUMENT EXTEND retroknowledge_int31
-PRINTED BY pr_r_int31_field
-| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
-| [ "int31" "type" ] -> [ Retroknowledge.Int31Type ]
-| [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ]
-| [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ]
-| [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ]
-| [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ]
-| [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ]
-| [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ]
-| [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ]
-| [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ]
-| [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ]
-| [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ]
-| [ "int31" "times" ] -> [ Retroknowledge.Int31Times ]
-| [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ]
-| [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ]
-| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ]
-| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ]
-| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ]
-| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
-| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ]
-| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ]
-| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ]
-| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ]
-| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ]
-END
-
-VERNAC ARGUMENT EXTEND retroknowledge_field
-PRINTED BY pr_retroknowledge_field
-| [ retroknowledge_int31 (i) ] -> [ Retroknowledge.KInt31 i ]
-END
-- 
cgit v1.2.3