[cleanup] Change Id.t option to Name.t in TacFun

18 files changed, 39 insertions, 31 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index f54f3fcc8..2a083b360 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -40,6 +40,9 @@ important things:
 - Some printing functions were moved from Pptactic to Pputils
 - A part of Tacexpr has been moved to Tactypes
 
+The TacFun tactic expression constructor now takes a `Name.t list` for the
+variable list rather than an `Id.t option list`.
+
 ** Error handling **
 
 - All error functions now take an optional parameter `?loc:Loc.t`. For
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index a5e36e47b..37ec1d56a 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -41,6 +41,8 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
+val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr
+
 val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr
 
 val type_of_user_symbol : user_symbol -> argument_type
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 919ca3ad7..0dd096ef7 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -58,6 +58,10 @@ let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
 
+let mlexpr_of_name f = function
+  | None -> <:expr< Anonymous >>
+  | Some e -> <:expr< Name $f e$ >>
+
 let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >>
 
 let rec mlexpr_of_prod_entry_key f = function
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index fe864ed40..8605dda3a 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -88,7 +88,7 @@ let declare_tactic loc s c cl = match cl with
       add any grammar nor printing rule and add it as a true Ltac definition. *)
   let patt = make_patt rem in
   let vars = List.map make_var rem in
-  let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
+  let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
   let entry = mlexpr_of_string s in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index a37cf306e..f32548cd3 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -16,6 +16,7 @@ open Pcoq.Constr
 open Pltac
 open Hints
 open Tacexpr
+open Names
 
 DECLARE PLUGIN "g_auto"
 
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index a28132a4b..ca9537c82 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -13,6 +13,7 @@ open Class_tactics
 open Pltac
 open Stdarg
 open Tacarg
+open Names
 
 DECLARE PLUGIN "g_class"
 
diff --git a/ltac/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4
index 905653281..679aa1127 100644
--- a/ltac/g_eqdecide.ml4
+++ b/ltac/g_eqdecide.ml4
@@ -15,6 +15,7 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Eqdecide
+open Names
 
 DECLARE PLUGIN "g_eqdecide"
 
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 54229bb2a..aab568746 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -17,6 +17,7 @@ open Misctypes
 open Genarg
 open Genredexpr
 open Tok (* necessary for camlp4 *)
+open Names
 
 open Pcoq
 open Pcoq.Constr
@@ -226,8 +227,8 @@ GEXTEND Gram
       | "multimatch" -> General ] ]
   ;
   input_fun:
-    [ [ "_" -> None
-      | l = ident -> Some l ] ]
+    [ [ "_" -> Anonymous
+      | l = ident -> Name l ] ]
   ;
   let_clause:
     [ [ id = identref; ":="; te = tactic_expr ->
@@ -499,8 +500,8 @@ let pr_tacdef_body tacdef_body =
       | Tacexpr.TacFun (idl,b) -> idl,b
       | _ -> [], body in
   id ++
-    prlist (function None -> str " _"
-      | Some id -> spc () ++ Nameops.pr_id id) idl
+    prlist (function Anonymous -> str " _"
+      | Name id -> spc () ++ Nameops.pr_id id) idl
   ++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
   ++ Pptactic.pr_raw_tactic body
 
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index fccee6e40..6f4ef37b4 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -574,9 +574,7 @@ module Make
               str "=>" ++ brk (1,4) ++ pr t))
     | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
-  let pr_funvar = function
-    | None -> spc () ++ str "_"
-    | Some id -> spc () ++ pr_id id
+  let pr_funvar n = spc () ++ pr_name n
 
   let pr_let_clause k pr (id,(bl,t)) =
     hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 2e2b55be7..75edf150e 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -504,10 +504,7 @@ let print_ltacs () =
     | Tacexpr.TacFun (l, t) -> (l, t)
     | _ -> ([], body)
     in
-    let pr_ltac_fun_arg = function
-    | None -> spc () ++ str "_"
-    | Some id -> spc () ++ pr_id id
-    in
+    let pr_ltac_fun_arg n = spc () ++ pr_name n in
     hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
   in
   Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
diff --git a/ltac/tacexpr.mli b/ltac/tacexpr.mli
index 9c25a1645..e23992a80 100644
--- a/ltac/tacexpr.mli
+++ b/ltac/tacexpr.mli
@@ -282,7 +282,7 @@ constraint 'a = <
 >
 
 and 'a gen_tactic_fun_ast =
-    Id.t option list * 'a gen_tactic_expr
+    Name.t list * 'a gen_tactic_expr
 
 constraint 'a = <
     term:'t;
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 763e0dc22..3292c8353 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -646,7 +646,7 @@ and intern_tactic_or_tacarg ist = intern_tactic false ist
 and intern_pure_tactic ist = intern_tactic true ist
 
 and intern_tactic_fun ist (var,body) =
-  let lfun = List.fold_left opt_cons ist.ltacvars var in
+  let lfun = List.fold_left name_cons ist.ltacvars var in
   (var,intern_tactic_or_tacarg { ist with ltacvars = lfun } body)
 
 and intern_tacarg strict onlytac ist = function
@@ -722,9 +722,7 @@ let split_ltac_fun = function
   | TacFun (l,t) -> (l,t)
   | t -> ([],t)
 
-let pr_ltac_fun_arg = function
-  | None -> spc () ++ str "_"
-  | Some id -> spc () ++ pr_id id
+let pr_ltac_fun_arg n = spc () ++ pr_name n
 
 let print_ltac id =
  try
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 32bcdfb6a..adc393d2c 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -120,7 +120,7 @@ let combine_appl appl1 appl2 =
 (* Values for interpretation *)
 type tacvalue =
   | VFun of appl*ltac_trace * value Id.Map.t *
-      Id.t option list * glob_tactic_expr
+      Name.t list * glob_tactic_expr
   | VRec of value Id.Map.t ref * glob_tactic_expr
 
 let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
@@ -1087,8 +1087,8 @@ let head_with_value (lvar,lval) =
     | ([],[]) -> (lacc,[],[])
     | (vr::tvr,ve::tve) ->
       (match vr with
-      |	None -> head_with_value_rec lacc (tvr,tve)
-      | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
+      |	Anonymous -> head_with_value_rec lacc (tvr,tve)
+      | Name v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
     | (vr,[]) -> (lacc,vr,[])
     | ([],ve) -> (lacc,[],ve)
   in
@@ -2119,8 +2119,8 @@ let lift_constr_tac_to_ml_tac vars tac =
     let env = Proofview.Goal.env gl in
     let sigma = project gl in
     let map = function
-    | None -> None
-    | Some id ->
+    | Anonymous -> None
+    | Name id ->
       let c = Id.Map.find id ist.lfun in
       try Some (coerce_to_closed_constr env c)
       with CannotCoerceTo ty ->
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 6f64981ef..adbd1d32b 100644
--- a/ltac/tacinterp.mli
+++ b/ltac/tacinterp.mli
@@ -115,7 +115,7 @@ val error_ltac_variable : Loc.t -> Id.t ->
 
 (** Transforms a constr-expecting tactic into a tactic finding its arguments in
     the Ltac environment according to the given names. *)
-val lift_constr_tac_to_ml_tac : Id.t option list ->
+val lift_constr_tac_to_ml_tac : Name.t list ->
   (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic
 
 val default_ist : unit -> Geninterp.interp_sign
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index 756958c2f..fb05fd7d0 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -259,7 +259,7 @@ let with_flags flags _ ist =
 
 let register_tauto_tactic tac name0 args =
   let ids = List.map (fun id -> Id.of_string id) args in
-  let ids = List.map (fun id -> Some id) ids in
+  let ids = List.map (fun id -> Name id) ids in
   let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in
   let entry = { mltac_name = name; mltac_index = 0 } in
   let () = Tacenv.register_ml_tactic name [| tac |] in
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 5f906a8da..fda7c0fa8 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -10,6 +10,8 @@ DECLARE PLUGIN "nsatz_plugin"
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Names
+
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 657efe175..d1f3bd6d3 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -122,7 +122,7 @@ let closed_term_ast l =
     mltac_index = 0;
   } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
-  TacFun([Some(Id.of_string"t")],
+  TacFun([Name(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
   [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
    TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))
@@ -205,7 +205,7 @@ let exec_tactic env evd n f args =
   let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
   let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
   let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in
-  let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in
+  let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
   (** Evaluate the whole result *)
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
@@ -722,8 +722,8 @@ let ltac_ring_structure e =
   let pow_tac = tacarg e.ring_pow_tac in
   let lemma1 = carg e.ring_lemma1 in
   let lemma2 = carg e.ring_lemma2 in
-  let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in
-  let posttac = tacarg (TacFun([None],e.ring_post_tac)) in
+  let pretac = tacarg (TacFun([Anonymous],e.ring_pre_tac)) in
+  let posttac = tacarg (TacFun([Anonymous],e.ring_post_tac)) in
   [req;sth;ext;morph;th;cst_tac;pow_tac;
    lemma1;lemma2;pretac;posttac]
 
@@ -994,8 +994,8 @@ let ltac_field_structure e =
   let field_simpl_eq_ok = carg e.field_simpl_eq_ok in
   let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in
   let cond_ok = carg e.field_cond in
-  let pretac = tacarg (TacFun([None],e.field_pre_tac)) in
-  let posttac = tacarg (TacFun([None],e.field_post_tac)) in
+  let pretac = tacarg (TacFun([Anonymous],e.field_pre_tac)) in
+  let posttac = tacarg (TacFun([Anonymous],e.field_post_tac)) in
   [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc988a2c5..ea14bc00a 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1411,7 +1411,7 @@ let () =
   let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in
   let () = Tacenv.register_ml_tactic name [|mltac|] in
   let tac =
-    TacFun ([Some (Id.of_string "pattern")],
+    TacFun ([Name (Id.of_string "pattern")],
       TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in
   let obj () =
     Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in