Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun

11 files changed, 20 insertions, 23 deletions

diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 4ec42c676f..fcc2b86a91 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/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/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index a28132a4b0..ca9537c824 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/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/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 905653281c..679aa11272 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/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/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 54229bb2ae..aab5687465 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/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/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fccee6e40a..6f4ef37b44 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/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/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be74..75edf150e3 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/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/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9c25a16457..e23992a807 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/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/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 4b5d87fc3c..1a8f26b264 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/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/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fda9142eda..aa646aa517 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/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
@@ -2120,8 +2120,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/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 6f64981eff..adbd1d32be 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/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/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 756958c2f0..fb05fd7d0e 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/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