1 files changed, 43 insertions, 44 deletions

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index e510b9f5..636cb8eb 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
@@ -252,7 +252,7 @@ type tactic_grammar_obj = {
   tacobj_key : KerName.t;
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
-  tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+  tacobj_body : Tacenv.alias_tactic;
   tacobj_forml : bool;
 }
 
@@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) =
     extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
-  let (ids, body) = tobj.tacobj_body in
+  let open Tacenv in
+  let alias = tobj.tacobj_body in
   { tobj with
     tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
-    tacobj_body = (ids, Tacsubst.subst_tactic subst body);
+    tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body };
   }
 
 let classify_tactic_notation tacobj = Substitute tacobj
@@ -308,25 +309,26 @@ let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, (_, ido)) -> ido
 
-let add_glob_tactic_notation local ~level prods forml ids tac =
+let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac =
   let parule = {
     tacgram_level = level;
     tacgram_prods = prods;
   } in
+  let open Tacenv in
   let tacobj = {
     tacobj_key = make_fresh_key prods;
     tacobj_local = local;
     tacobj_tacgram = parule;
-    tacobj_body = (ids, tac);
+    tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation };
     tacobj_forml = forml;
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)
 
-let add_tactic_notation local n prods e =
+let add_tactic_notation local n ?deprecation prods e =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local ~level:n prods false ids tac
+  add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
@@ -366,7 +368,7 @@ let extend_atomic_tactic name entries =
   in
   List.iteri add_atomic entries
 
-let add_ml_tactic_notation name ~level prods =
+let add_ml_tactic_notation name ~level ?deprecation prods =
   let len = List.length prods in
   let iter i prods =
     let open Tacexpr in
@@ -376,9 +378,9 @@ let add_ml_tactic_notation name ~level prods =
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
-    let map id = Reference (Misctypes.ArgVar (CAst.make id)) in
+    let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = TacML (Loc.tag (entry, List.map map ids)) in
-    add_glob_tactic_notation false ~level prods true ids tac
+    add_glob_tactic_notation false ~level ?deprecation prods true ids tac
   in
   List.iteri iter (List.rev prods);
   (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
@@ -398,7 +400,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
@@ -430,7 +432,7 @@ let warn_unusable_identifier =
       (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
         strbrk "may be unusable because of a conflict with a notation.")
 
-let register_ltac local tacl =
+let register_ltac local ?deprecation tacl =
   let map tactic_body =
     match tactic_body with
     | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
@@ -449,12 +451,12 @@ let register_ltac local tacl =
         in
         let () = if is_shadowed then warn_unusable_identifier id in
         NewTac id, body
-    | Tacexpr.TacticRedefinition (ident, body) ->
+    | Tacexpr.TacticRedefinition (qid, body) ->
         let kn =
-          try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v
+          try Tacenv.locate_tactic qid
           with Not_found ->
-            CErrors.user_err ?loc:ident.CAst.loc
-                       (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+            CErrors.user_err ?loc:qid.CAst.loc
+                       (str "There is no Ltac named " ++ pr_qualid qid ++ str ".")
         in
         UpdateTac kn, body
   in
@@ -483,10 +485,10 @@ let register_ltac local tacl =
   let defs = States.with_state_protection defs () in
   let iter (def, tac) = match def with
   | NewTac id ->
-    Tacenv.register_ltac false local id tac;
+    Tacenv.register_ltac false local id tac ?deprecation;
     Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
   | UpdateTac kn ->
-    Tacenv.redefine_ltac local kn tac;
+    Tacenv.redefine_ltac local kn tac ?deprecation;
     let name = Tacenv.shortest_qualid_of_tactic kn in
     Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
@@ -554,13 +556,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,23 +585,15 @@ 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
 
-let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
-  | TUentry a -> ExtraArg a
-  | TUentryl (a,l) -> ExtraArg a
-  | TUopt(o) -> OptArg (prj o)
-  | TUlist1 l -> ListArg (prj l)
-  | TUlist1sep (l,_) -> ListArg (prj l)
-  | TUlist0 l -> ListArg (prj l)
-  | TUlist0sep (l,_) -> ListArg (prj l)
-
 let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
   fun sign tac ->
     match sign with
@@ -604,15 +603,15 @@ 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
       | v :: vals ->
-        let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+        let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol 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 +623,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 "_"
 
@@ -652,7 +651,7 @@ let lift_constr_tac_to_ml_tac vars tac =
   end in
   tac
 
-let tactic_extend plugin_name tacname ~level sign =
+let tactic_extend plugin_name tacname ~level ?deprecation sign =
   let open Tacexpr in
   let ml_tactic_name =
     { mltac_tactic = tacname;
@@ -681,10 +680,10 @@ let tactic_extend plugin_name tacname ~level sign =
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
     let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
     let id = Names.Id.of_string name in
-    let obj () = Tacenv.register_ltac true false id body in
+    let obj () = Tacenv.register_ltac true false id body ?deprecation in
     let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
     Mltop.declare_cache_obj obj plugin_name
   | _ ->
-  let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+  let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
   Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
   Mltop.declare_cache_obj obj plugin_name