diff options
Diffstat (limited to 'plugins/ltac/extraargs.ml4')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 102 |
1 files changed, 22 insertions, 80 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dbbdbfa396..f4555509cc 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -52,8 +52,11 @@ let () = (* Rewriting orientation *) -let _ = Metasyntax.add_token_obj "<-" -let _ = Metasyntax.add_token_obj "->" +let _ = + Mltop.declare_cache_obj + (fun () -> Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" let pr_orient _prc _prlc _prt = function | true -> Pp.mt () @@ -196,9 +199,9 @@ let pr_gen_place pr_id = function ConclLocation () -> Pp.mt () | HypLocation (id,InHyp) -> str "in " ++ pr_id id | HypLocation (id,InHypTypeOnly) -> - str "in (Type of " ++ pr_id id ++ str ")" + str "in (type of " ++ pr_id id ++ str ")" | HypLocation (id,InHypValueOnly) -> - str "in (Value of " ++ pr_id id ++ str ")" + str "in (value of " ++ pr_id id ++ str ")" let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print @@ -217,6 +220,14 @@ let interp_place ist gl p = let subst_place subst pl = pl +let warn_deprecated_instantiate_syntax = + CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" + (fun (v,v',id) -> + let s = Id.to_string id in + Pp.strbrk + ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") + ) + ARGUMENT EXTEND hloc PRINTED BY pr_place INTERPRETED BY interp_place @@ -231,8 +242,14 @@ ARGUMENT EXTEND hloc | [ "in" ident(id) ] -> [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypTypeOnly) ] + [ warn_deprecated_instantiate_syntax ("Type","type",id); + HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> + [ warn_deprecated_instantiate_syntax ("Value","value",id); + HypLocation ((CAst.make id),InHypValueOnly) ] +| [ "in" "(" "type" "of" ident(id) ")" ] -> + [ HypLocation ((CAst.make id),InHypTypeOnly) ] +| [ "in" "(" "value" "of" ident(id) ")" ] -> [ HypLocation ((CAst.make id),InHypValueOnly) ] END @@ -294,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 |