diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-02 18:32:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-02 20:01:39 +0200 |
| commit | 48d7337f0d685efe11b1ec2a7fd3d68bdedf0d60 (patch) | |
| tree | 7ce8fedc1655f4ee7b9538a3dc50ad952e06bd7c /grammar | |
| parent | f3fa8071d78841630f2ec8657478e667f70afc16 (diff) | |
Slight simplification of the Tacentries API to register ML tactics.
It was forcing the macro to generate code that was useless.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/coqpp_main.ml | 10 | ||||
| -rw-r--r-- | grammar/tacextend.mlp | 9 |
2 files changed, 5 insertions, 14 deletions
diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml index a4a6b510a..7caa0a6bd 100644 --- a/grammar/coqpp_main.ml +++ b/grammar/coqpp_main.ml @@ -270,10 +270,6 @@ val print_ast : Format.formatter -> tactic_ext -> unit end = struct -let print_ident chan id = - (** Workaround for badly-designed generic arguments lacking a closure *) - fprintf chan "Names.Id.of_string_soft \"$%s\"" id - let rec print_symbol chan = function | Ulist1 s -> fprintf chan "@[Extend.TUlist1 (%a)@]" print_symbol s @@ -295,11 +291,11 @@ let rec print_clause chan = function | [] -> fprintf chan "@[TyNil@]" | ExtTerminal s :: cl -> fprintf chan "@[TyIdent (\"%s\", %a)@]" s print_clause cl | ExtNonTerminal (g, TokNone) :: cl -> - fprintf chan "@[TyAnonArg (Loc.tag (%a), %a)@]" + fprintf chan "@[TyAnonArg (%a, %a)@]" print_symbol g print_clause cl | ExtNonTerminal (g, TokName id) :: cl -> - fprintf chan "@[TyArg (Loc.tag (%a, %a), %a)@]" - print_symbol g print_ident id print_clause cl + fprintf chan "@[TyArg (%a, \"%s\", %a)@]" + print_symbol g id print_clause cl let rec print_binders chan = function | [] -> fprintf chan "ist@ " diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 525be6432..cea0bed59 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -15,11 +15,6 @@ open Argextend let plugin_name = <:expr< __coq_plugin_name >> -let mlexpr_of_ident id = - (** Workaround for badly-designed generic arguments lacking a closure *) - let id = "$" ^ id in - <:expr< Names.Id.of_string_soft $str:id$ >> - let rec mlexpr_of_symbol = function | Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> | Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> @@ -38,9 +33,9 @@ let rec mlexpr_of_clause = function | [] -> <:expr< TyNil >> | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,None) :: cl -> - <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >> + <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,Some id) :: cl -> - <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >> + <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >> let rec binders_of_clause e = function | [] -> <:expr< fun ist -> $e$ >> |