From f99f60902d7492902110fb091c52e58e1ed9cd32 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 19 Oct 2017 18:17:33 +0200 Subject: Use a homebrew parser to replace the GEXTEND extension points of Camlp5. The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one. --- plugins/ltac/tacentries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 98d451536..876e6f320 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -45,7 +45,7 @@ let coincide s pat off = let atactic n = if n = 5 then Aentry Pltac.binder_tactic - else Aentryl (Pltac.tactic_expr, n) + else Aentryl (Pltac.tactic_expr, string_of_int n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name @@ -398,7 +398,7 @@ let create_ltac_quotation name cast (e, l) = let () = ltac_quotations := String.Set.add name !ltac_quotations in let entry = match l with | None -> Aentry e - | Some l -> Aentryl (e, l) + | Some l -> Aentryl (e, string_of_int l) in (* let level = Some "1" in *) let level = None in -- cgit v1.2.3