diff options
| -rw-r--r-- | grammar/coqpp_main.ml | 10 | ||||
| -rw-r--r-- | grammar/tacextend.mlp | 9 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 30 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 4 |
4 files changed, 25 insertions, 28 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$ >> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 876e6f320..fac464a62 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -554,13 +554,18 @@ let () = ] in register_grammars_by_name "tactic" entries +let get_identifier id = + (** Workaround for badly-designed generic arguments lacking a closure *) + Names.Id.of_string_soft ("$" ^ id) + + type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml @@ -578,10 +583,11 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol fun sign -> match sign with | TyNil -> [] | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' - | TyArg ((loc,(a,id)),sig') -> - TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' - | TyAnonArg ((loc,a),sig') -> - TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + | TyArg (a, id, sig') -> + let id = get_identifier id in + TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg (a, sig') -> + TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig' let clause_of_ty_ml = function | TyML (t,_) -> clause_of_sign t @@ -604,7 +610,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i | _ :: _ -> assert false end | TyIdent (s, sig') -> eval_sign sig' tac - | TyArg ((_loc,(a,id)), sig') -> + | TyArg (a, _, sig') -> let f = eval_sign sig' in begin fun tac vals ist -> match vals with | [] -> assert false @@ -612,7 +618,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i let v' = Taccoerce.Value.cast (topwit (prj a)) v in f (tac v') vals ist end tac - | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + | TyAnonArg (a, sig') -> eval_sign sig' tac let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function | TyML (t,tac) -> eval_sign t tac @@ -624,14 +630,14 @@ let is_constr_entry = function let rec only_constr : type a. a ty_sig -> bool = function | TyNil -> true | TyIdent(_,_) -> false -| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false -| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false +| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function | TyNil -> [] | TyIdent (_,s) -> mk_sign_vars s -| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s -| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s +| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s +| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s let dummy_id = Id.of_string "_" diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 2bfbbe2e1..9bba9ba71 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -72,9 +72,9 @@ type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml |