3 files changed, 9 insertions, 8 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c7bda43465..1640bff43b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -373,11 +373,6 @@ end) = struct
 
 end
 
-(* let my_type_of env evars c = Typing.e_type_of env evars c *)
-(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *)
-(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *)
-
-
 let type_app_poly env env evd f args =
   let evars, c = app_poly_nocheck env evd f args in
   let evd', t = Typing.type_of env (goalevars evars) c in
@@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r =
 
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
-(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *)
-(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
-
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals =
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 5e88bf7c79..f2f5fc16a6 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -91,6 +91,13 @@ let to_int v =
     Some (out_gen (topwit wit_int) v)
   else None
 
+let of_ident id = in_gen (topwit wit_ident) id
+
+let to_ident v =
+  if has_type v (topwit wit_ident) then
+    Some (out_gen (topwit wit_ident) v)
+  else None
+
 let to_list v = prj Val.typ_list v
 
 let to_option v = prj Val.typ_opt v
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 8ca2510459..c748fb3d1a 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -39,6 +39,8 @@ sig
   val to_uconstr : t -> Ltac_pretype.closed_glob_constr option
   val of_int : int -> t
   val to_int : t -> int option
+  val of_ident : Id.t -> t
+  val to_ident : t -> Id.t option
   val to_list : t -> t list option
   val to_option : t -> t option option
   val to_pair : t -> (t * t) option