From 48d7337f0d685efe11b1ec2a7fd3d68bdedf0d60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 2 Jul 2018 18:32:08 +0200
Subject: Slight simplification of the Tacentries API to register ML tactics.

It was forcing the macro to generate code that was useless.
---
 grammar/coqpp_main.ml | 10 +++-------
 grammar/tacextend.mlp |  9 ++-------
 2 files changed, 5 insertions(+), 14 deletions(-)

(limited to 'grammar')

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$ >>
-- 
cgit v1.2.3