diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 75 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.mli | 5 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 16 |
3 files changed, 0 insertions, 96 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 38600695dc..f4555509cc 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -311,78 +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.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 - -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 -(*| [ "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) ] -END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e477b12cd3..fa70235975 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type -(** Spiwack: Primitive for retroknowledge registration *) - -val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t -val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type - val wit_in_clause : (lident Locus.clause_expr, lident Locus.clause_expr, diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index dc027c4041..8dad6260ae 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -545,22 +545,6 @@ END (**********************************************************************) -(*spiwack : Vernac commands for retroknowledge *) - -VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF - | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> - [ let env = Global.env () in - let evd = Evd.from_env env in - let tc,_ctx = Constrintern.interp_constr env evd c in - let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in - let tc = EConstr.to_constr evd tc in - let tb = EConstr.to_constr evd tb in - Global.register f tc tb ] -END - - - -(**********************************************************************) (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) TACTIC EXTEND generalize_eqs |