From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- plugins/syntax/ascii_syntax.ml | 83 ++++++++ plugins/syntax/ascii_syntax_plugin.mllib | 2 + plugins/syntax/nat_syntax.ml | 78 +++++++ plugins/syntax/nat_syntax_plugin.mllib | 2 + plugins/syntax/numbers_syntax.ml | 330 +++++++++++++++++++++++++++++ plugins/syntax/numbers_syntax_plugin.mllib | 2 + plugins/syntax/r_syntax.ml | 125 +++++++++++ plugins/syntax/r_syntax_plugin.mllib | 2 + plugins/syntax/string_syntax.ml | 69 ++++++ plugins/syntax/string_syntax_plugin.mllib | 2 + plugins/syntax/z_syntax.ml | 194 +++++++++++++++++ plugins/syntax/z_syntax_plugin.mllib | 2 + 12 files changed, 891 insertions(+) create mode 100644 plugins/syntax/ascii_syntax.ml create mode 100644 plugins/syntax/ascii_syntax_plugin.mllib create mode 100644 plugins/syntax/nat_syntax.ml create mode 100644 plugins/syntax/nat_syntax_plugin.mllib create mode 100644 plugins/syntax/numbers_syntax.ml create mode 100644 plugins/syntax/numbers_syntax_plugin.mllib create mode 100644 plugins/syntax/r_syntax.ml create mode 100644 plugins/syntax/r_syntax_plugin.mllib create mode 100644 plugins/syntax/string_syntax.ml create mode 100644 plugins/syntax/string_syntax_plugin.mllib create mode 100644 plugins/syntax/z_syntax.ml create mode 100644 plugins/syntax/z_syntax_plugin.mllib (limited to 'plugins/syntax') diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml new file mode 100644 index 00000000..19473dfa --- /dev/null +++ b/plugins/syntax/ascii_syntax.ml @@ -0,0 +1,83 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 0 + | RRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l) + | _ -> raise Non_closed_ascii in + try + let rec aux = function + | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l + | _ -> raise Non_closed_ascii in + Some (aux r) + with + Non_closed_ascii -> None + +let make_ascii_string n = + if n>=32 && n<=126 then String.make 1 (char_of_int n) + else Printf.sprintf "%03d" n + +let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r) + +let _ = + Notation.declare_string_interpreter "char_scope" + (ascii_path,ascii_module) + interp_ascii_string + ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true) diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib new file mode 100644 index 00000000..b00f9250 --- /dev/null +++ b/plugins/syntax/ascii_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Ascii_syntax +Ascii_syntax_plugin_mod diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml new file mode 100644 index 00000000..5d20c2a3 --- /dev/null +++ b/plugins/syntax/nat_syntax.ml @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > *) + +let nat_of_int dloc n = + if is_pos_or_zero n then begin + if less_than (of_string "5000") n then + Flags.if_warn msg_warning + (strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in nat (observed threshold " ++ + strbrk "may vary from 5000 to 70000 depending on your system " ++ + strbrk "limits and on the command executed)."); + let ref_O = RRef (dloc, glob_O) in + let ref_S = RRef (dloc, glob_S) in + let rec mk_nat acc n = + if n <> zero then + mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n) + else + acc + in + mk_nat ref_O n + end + else + user_err_loc (dloc, "nat_of_int", + str "Cannot interpret a negative number as a number of type nat") + +(************************************************************************) +(* Printing via scopes *) + +exception Non_closed_number + +let rec int_of_nat = function + | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) + | RRef (_,z) when z = glob_O -> zero + | _ -> raise Non_closed_number + +let uninterp_nat p = + try + Some (int_of_nat p) + with + Non_closed_number -> None + +(************************************************************************) +(* Declare the primitive parsers and printers *) + +let _ = + Notation.declare_numeral_interpreter "nat_scope" + (nat_path,["Coq";"Init";"Datatypes"]) + nat_of_int + ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true) diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib new file mode 100644 index 00000000..69b0cb20 --- /dev/null +++ b/plugins/syntax/nat_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Nat_syntax +Nat_syntax_plugin_mod diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml new file mode 100644 index 00000000..4375d5e0 --- /dev/null +++ b/plugins/syntax/numbers_syntax.ml @@ -0,0 +1,330 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + ConstructRef ((bigN_t,0), + if less_than i n_inlined then + (to_int i)+1 + else + (to_int n_inlined)+1 + ) + +(*bigZ stuff*) +let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ] +let bigZ_path = make_path (bigZ_module@["BigZ"]) "t" +let bigZ_t = make_mind_mpdot bigZ_module "BigZ" "t_" +let bigZ_scope = "bigZ_scope" + +let bigZ_pos = ConstructRef ((bigZ_t,0),1) +let bigZ_neg = ConstructRef ((bigZ_t,0),2) + + +(*bigQ stuff*) +let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"] +let bigQ_path = make_path (bigQ_module@["BigQ"]) "t" +let bigQ_t = make_mind_mpdot bigQ_module "BigQ" "t_" +let bigQ_scope = "bigQ_scope" + +let bigQ_z = ConstructRef ((bigQ_t,0),1) + + +(*** Definition of the Non_closed exception, used in the pretty printing ***) +exception Non_closed + +(*** Parsing for int31 in digital notation ***) + +(* parses a *non-negative* integer (from bigint.ml) into an int31 + wraps modulo 2^31 *) +let int31_of_pos_bigint dloc n = + let ref_construct = RRef (dloc, int31_construct) in + let ref_0 = RRef (dloc, int31_0) in + let ref_1 = RRef (dloc, int31_1) in + let rec args counter n = + if counter <= 0 then + [] + else + let (q,r) = div2_with_rest n in + (if r then ref_1 else ref_0)::(args (counter-1) q) + in + RApp (dloc, ref_construct, List.rev (args 31 n)) + +let error_negative dloc = + Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") + +let interp_int31 dloc n = + if is_pos_or_zero n then + int31_of_pos_bigint dloc n + else + error_negative dloc + +(* Pretty prints an int31 *) + +let bigint_of_int31 = + let rec args_parsing args cur = + match args with + | [] -> cur + | (RRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur) + | (RRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | _ -> raise Non_closed + in + function + | RApp (_, RRef (_, c), args) when c=int31_construct -> args_parsing args zero + | _ -> raise Non_closed + +let uninterp_int31 i = + try + Some (bigint_of_int31 i) + with Non_closed -> + None + +(* Actually declares the interpreter for int31 *) +let _ = Notation.declare_numeral_interpreter int31_scope + (int31_path, int31_module) + interp_int31 + ([RRef (Util.dummy_loc, int31_construct)], + uninterp_int31, + true) + + +(*** Parsing for bigN in digital notation ***) +(* the base for bigN (in Coq) that is 2^31 in our case *) +let base = pow two (of_string "31") + +(* base of the bigN of height N : *) +let rank n = pow base (pow two n) + +(* splits a number bi at height n, that is the rest needs 2^n int31 to be stored + it is expected to be used only when the quotient would also need 2^n int31 to be + stored *) +let split_at n bi = + euclid bi (rank (sub_1 n)) + +(* search the height of the Coq bigint needed to represent the integer bi *) +let height bi = + let rec height_aux n = + if less_than bi (rank n) then + n + else + height_aux (add_1 n) + in + height_aux zero + + +(* n must be a non-negative integer (from bigint.ml) *) +let word_of_pos_bigint dloc hght n = + let ref_W0 = RRef (dloc, zn2z_W0) in + let ref_WW = RRef (dloc, zn2z_WW) in + let rec decomp hgt n = + if is_neg_or_zero hgt then + int31_of_pos_bigint dloc n + else if equal n zero then + RApp (dloc, ref_W0, [RHole (dloc, Evd.InternalHole)]) + else + let (h,l) = split_at hgt n in + RApp (dloc, ref_WW, [RHole (dloc, Evd.InternalHole); + decomp (sub_1 hgt) h; + decomp (sub_1 hgt) l]) + in + decomp hght n + +let bigN_of_pos_bigint dloc n = + let ref_constructor i = RRef (dloc, bigN_constructor i) in + let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then + [word] + else + [Nat_syntax.nat_of_int dloc (sub h n_inlined); + word]) + in + let hght = height n in + result hght (word_of_pos_bigint dloc hght n) + +let bigN_error_negative dloc = + Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") + +let interp_bigN dloc n = + if is_pos_or_zero n then + bigN_of_pos_bigint dloc n + else + bigN_error_negative dloc + + +(* Pretty prints a bigN *) + +let bigint_of_word = + let rec get_height rc = + match rc with + | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW -> + let hleft = get_height lft in + let hright = get_height rght in + add_1 + (if less_than hleft hright then + hright + else + hleft) + | _ -> zero + in + let rec transform hght rc = + match rc with + | RApp (_,RRef(_,c),_) when c = zn2z_W0-> zero + | RApp (_,RRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in + add (mult (rank new_hght) + (transform (new_hght) lft)) + (transform (new_hght) rght) + | _ -> bigint_of_int31 rc + in + fun rc -> + let hght = get_height rc in + transform hght rc + +let bigint_of_bigN rc = + match rc with + | RApp (_,_,[one_arg]) -> bigint_of_word one_arg + | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg + | _ -> raise Non_closed + +let uninterp_bigN rc = + try + Some (bigint_of_bigN rc) + with Non_closed -> + None + + +(* declare the list of constructors of bigN used in the declaration of the + numeral interpreter *) + +let bigN_list_of_constructors = + let rec build i = + if less_than i (add_1 n_inlined) then + RRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i)) + else + [] + in + build zero + +(* Actually declares the interpreter for bigN *) +let _ = Notation.declare_numeral_interpreter bigN_scope + (bigN_path, bigN_module) + interp_bigN + (bigN_list_of_constructors, + uninterp_bigN, + true) + + +(*** Parsing for bigZ in digital notation ***) +let interp_bigZ dloc n = + let ref_pos = RRef (dloc, bigZ_pos) in + let ref_neg = RRef (dloc, bigZ_neg) in + if is_pos_or_zero n then + RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) + else + RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)]) + +(* pretty printing functions for bigZ *) +let bigint_of_bigZ = function + | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg + | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg -> + let opp_val = bigint_of_bigN one_arg in + if equal opp_val zero then + raise Non_closed + else + neg opp_val + | _ -> raise Non_closed + + +let uninterp_bigZ rc = + try + Some (bigint_of_bigZ rc) + with Non_closed -> + None + +(* Actually declares the interpreter for bigZ *) +let _ = Notation.declare_numeral_interpreter bigZ_scope + (bigZ_path, bigZ_module) + interp_bigZ + ([RRef (Util.dummy_loc, bigZ_pos); + RRef (Util.dummy_loc, bigZ_neg)], + uninterp_bigZ, + true) + +(*** Parsing for bigQ in digital notation ***) +let interp_bigQ dloc n = + let ref_z = RRef (dloc, bigQ_z) in + RApp (dloc, ref_z, [interp_bigZ dloc n]) + +let uninterp_bigQ rc = + try match rc with + | RApp (_, RRef(_,c), [one_arg]) when c = bigQ_z -> + Some (bigint_of_bigZ one_arg) + | _ -> None (* we don't pretty-print yet fractions *) + with Non_closed -> None + +(* Actually declares the interpreter for bigQ *) +let _ = Notation.declare_numeral_interpreter bigQ_scope + (bigQ_path, bigQ_module) + interp_bigQ + ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ, + true) diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib new file mode 100644 index 00000000..ebc0bb20 --- /dev/null +++ b/plugins/syntax/numbers_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Numbers_syntax +Numbers_syntax_plugin_mod diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml new file mode 100644 index 00000000..f85309e6 --- /dev/null +++ b/plugins/syntax/r_syntax.ml @@ -0,0 +1,125 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* zero then r_of_pos n else RRef(dloc,glob_R0) + +let r_of_int dloc z = + if is_strictly_neg z then + RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) + else + r_of_posint dloc z + +(**********************************************************************) +(* Printing R via scopes *) +(**********************************************************************) + +let bignat_of_r = +(* for numbers > 1 *) +let rec bignat_of_pos = function + (* 1+1 *) + | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)]) + when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two + (* 1+(1+1) *) + | RApp (_,RRef (_,p1), [RRef (_,o1); + RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])]) + when p1 = glob_Rplus & p2 = glob_Rplus & + o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three + (* (1+1)*b *) + | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult -> + if bignat_of_pos a <> two then raise Non_closed_number; + mult_2 (bignat_of_pos b) + (* 1+(1+1)*b *) + | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])]) + when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1 -> + if bignat_of_pos a <> two then raise Non_closed_number; + add_1 (mult_2 (bignat_of_pos b)) + | _ -> raise Non_closed_number +in +let bignat_of_r = function + | RRef (_,a) when a = glob_R0 -> zero + | RRef (_,a) when a = glob_R1 -> one + | r -> bignat_of_pos r +in +bignat_of_r + +let bigint_of_r = function + | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> + let n = bignat_of_r a in + if n = zero then raise Non_closed_number; + neg n + | a -> bignat_of_r a + +let uninterp_r p = + try + Some (bigint_of_r p) + with Non_closed_number -> + None + +let _ = Notation.declare_numeral_interpreter "R_scope" + (r_path,["Coq";"Reals";"Rdefinitions"]) + r_of_int + ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0); + RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult); + RRef(dummy_loc,glob_R1)], + uninterp_r, + false) diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib new file mode 100644 index 00000000..5c173a14 --- /dev/null +++ b/plugins/syntax/r_syntax_plugin.mllib @@ -0,0 +1,2 @@ +R_syntax +R_syntax_plugin_mod diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml new file mode 100644 index 00000000..bc02357a --- /dev/null +++ b/plugins/syntax/string_syntax.ml @@ -0,0 +1,69 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (match uninterp_ascii a with + | Some c -> Buffer.add_char b (Char.chr c); aux s + | _ -> raise Non_closed_string) + | RRef (_,z) when z = force glob_EmptyString -> + Some (Buffer.contents b) + | _ -> + raise Non_closed_string + in aux r + with + Non_closed_string -> None + +let _ = + Notation.declare_string_interpreter "string_scope" + (string_path,["Coq";"Strings";"String"]) + interp_string + ([RRef (dummy_loc,static_glob_String); + RRef (dummy_loc,static_glob_EmptyString)], + uninterp_string, true) diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib new file mode 100644 index 00000000..b108c9e0 --- /dev/null +++ b/plugins/syntax/string_syntax_plugin.mllib @@ -0,0 +1,2 @@ +String_syntax +String_syntax_plugin_mod diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml new file mode 100644 index 00000000..f6afd080 --- /dev/null +++ b/plugins/syntax/z_syntax.ml @@ -0,0 +1,194 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* RApp (dloc, ref_xO,[pos_of q]) + | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q]) + | (q,true) -> ref_xH + in + pos_of x + +let error_non_positive dloc = + user_err_loc (dloc, "interp_positive", + str "Only strictly positive numbers in type \"positive\".") + +let interp_positive dloc n = + if is_strictly_pos n then pos_of_bignat dloc n + else error_non_positive dloc + +(**********************************************************************) +(* Printing positive via scopes *) +(**********************************************************************) + +let rec bignat_of_pos = function + | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a) + | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a)) + | RRef (_, a) when a = glob_xH -> Bigint.one + | _ -> raise Non_closed_number + +let uninterp_positive p = + try + Some (bignat_of_pos p) + with Non_closed_number -> + None + +(************************************************************************) +(* Declaring interpreters and uninterpreters for positive *) +(************************************************************************) + +let _ = Notation.declare_numeral_interpreter "positive_scope" + (positive_path,positive_module) + interp_positive + ([RRef (dummy_loc, glob_xI); + RRef (dummy_loc, glob_xO); + RRef (dummy_loc, glob_xH)], + uninterp_positive, + true) + +(**********************************************************************) +(* Parsing N via scopes *) +(**********************************************************************) + +let binnat_module = ["Coq";"NArith";"BinNat"] +let n_kn = make_kn (make_dir binnat_module) (id_of_string "N") +let glob_n = IndRef (n_kn,0) +let path_of_N0 = ((n_kn,0),1) +let path_of_Npos = ((n_kn,0),2) +let glob_N0 = ConstructRef path_of_N0 +let glob_Npos = ConstructRef path_of_Npos + +let n_path = make_path binnat_module "N" + +let n_of_binnat dloc pos_or_neg n = + if n <> zero then + RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n]) + else + RRef (dloc, glob_N0) + +let error_negative dloc = + user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") + +let n_of_int dloc n = + if is_pos_or_zero n then n_of_binnat dloc true n + else error_negative dloc + +(**********************************************************************) +(* Printing N via scopes *) +(**********************************************************************) + +let bignat_of_n = function + | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a + | RRef (_, a) when a = glob_N0 -> Bigint.zero + | _ -> raise Non_closed_number + +let uninterp_n p = + try Some (bignat_of_n p) + with Non_closed_number -> None + +(************************************************************************) +(* Declaring interpreters and uninterpreters for N *) + +let _ = Notation.declare_numeral_interpreter "N_scope" + (n_path,binnat_module) + n_of_int + ([RRef (dummy_loc, glob_N0); + RRef (dummy_loc, glob_Npos)], + uninterp_n, + true) + +(**********************************************************************) +(* Parsing Z via scopes *) +(**********************************************************************) + +let binint_module = ["Coq";"ZArith";"BinInt"] +let z_path = make_path binint_module "Z" +let z_kn = make_kn (make_dir binint_module) (id_of_string "Z") +let glob_z = IndRef (z_kn,0) +let path_of_ZERO = ((z_kn,0),1) +let path_of_POS = ((z_kn,0),2) +let path_of_NEG = ((z_kn,0),3) +let glob_ZERO = ConstructRef path_of_ZERO +let glob_POS = ConstructRef path_of_POS +let glob_NEG = ConstructRef path_of_NEG + +let z_of_int dloc n = + if n <> zero then + let sgn, n = + if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in + RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n]) + else + RRef (dloc, glob_ZERO) + +(**********************************************************************) +(* Printing Z via scopes *) +(**********************************************************************) + +let bigint_of_z = function + | RApp (_, RRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a + | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a) + | RRef (_, a) when a = glob_ZERO -> Bigint.zero + | _ -> raise Non_closed_number + +let uninterp_z p = + try + Some (bigint_of_z p) + with Non_closed_number -> None + +(************************************************************************) +(* Declaring interpreters and uninterpreters for Z *) + +let _ = Notation.declare_numeral_interpreter "Z_scope" + (z_path,binint_module) + z_of_int + ([RRef (dummy_loc, glob_ZERO); + RRef (dummy_loc, glob_POS); + RRef (dummy_loc, glob_NEG)], + uninterp_z, + true) diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib new file mode 100644 index 00000000..36d41acc --- /dev/null +++ b/plugins/syntax/z_syntax_plugin.mllib @@ -0,0 +1,2 @@ +Z_syntax +Z_syntax_plugin_mod -- cgit v1.2.3