Moving coercion functions out of Tacinterp.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16577 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 334 insertions, 219 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 2c0ca8fd1..da2660ae5 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -12,6 +12,7 @@ open Pp
 open Genarg
 open Names
 open Tacexpr
+open Taccoerce
 open Tacinterp
 open Misctypes
 open Locus
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
new file mode 100644
index 000000000..f00f55527
--- /dev/null
+++ b/tactics/taccoerce.ml
@@ -0,0 +1,239 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Errors
+open Names
+open Term
+open Pattern
+open Misctypes
+open Genarg
+
+exception CannotCoerceTo of string
+
+let (wit_unit : (unit, unit, unit) Genarg.genarg_type) =
+  Genarg.create_arg None "unit"
+
+let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
+  Genarg.create_arg None "constr_context"
+
+(* includes idents known to be bound and references *)
+let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
+  Genarg.create_arg None "constr_under_binders"
+
+module Value =
+struct
+
+type t = tlevel generic_argument
+
+let rec normalize v =
+  if has_type v (topwit wit_genarg) then
+    normalize (out_gen (topwit wit_genarg) v)
+  else v
+
+let of_constr c = in_gen (topwit wit_constr) c
+
+let to_constr v =
+  let v = normalize v in
+  if has_type v (topwit wit_constr) then
+    let c = out_gen (topwit wit_constr) v in
+    Some c
+  else if has_type v (topwit wit_constr_under_binders) then
+    let vars, c = out_gen (topwit wit_constr_under_binders) v in
+    match vars with [] -> Some c | _ -> None
+  else None
+
+let of_int i = in_gen (topwit wit_int) i
+
+let to_int v =
+  let v = normalize v in
+  if has_type v (topwit wit_int) then
+    Some (out_gen (topwit wit_int) v)
+  else None
+
+let to_list v =
+  let v = normalize v in
+  try Some (fold_list0 (fun v accu -> v :: accu) v [])
+  with Failure _ ->
+    try Some (fold_list1 (fun v accu -> v :: accu) v [])
+    with Failure _ ->
+      None
+
+end
+
+let is_variable env id =
+  List.mem id (Termops.ids_of_named_context (Environ.named_context env))
+
+(* Transforms an id into a constr if possible, or fails with Not_found *)
+let constr_of_id env id =
+  Term.mkVar (let _ = Environ.lookup_named id env in id)
+
+(* Gives the constr corresponding to a Constr_context tactic_arg *)
+let coerce_to_constr_context v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_constr_context) then
+    out_gen (topwit wit_constr_context) v
+  else errorlabstrm "coerce_to_constr_context" (str "Not a context variable.")
+
+(* Interprets an identifier which must be fresh *)
+let coerce_to_ident fresh env v =
+  let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "a fresh identifier") in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroIdentifier id -> id
+    | _ -> fail ()
+  else match Value.to_constr v with
+  | None -> fail ()
+  | Some c ->
+    (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
+    if isVar c && not (fresh && is_variable env (destVar c)) then
+      destVar c
+    else fail ()
+
+let coerce_to_intro_pattern env v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    snd (out_gen (topwit wit_intro_pattern) v)
+  else match Value.to_constr v with
+  | Some c when isVar c ->
+      (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
+      (* but also in "destruct H as (H,H')" *)
+      IntroIdentifier (destVar c)
+  | _ -> raise (CannotCoerceTo "an introduction pattern")
+
+let coerce_to_hint_base v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroIdentifier id -> Id.to_string id
+    | _ -> raise (CannotCoerceTo "a hint base name")
+  else raise (CannotCoerceTo "a hint base name")
+
+let coerce_to_int v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_int) then
+    out_gen (topwit wit_int) v
+  else raise (CannotCoerceTo "an integer")
+
+let coerce_to_constr env v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroIdentifier id -> ([],constr_of_id env id)
+    | _ -> raise Not_found
+  else if has_type v (topwit wit_constr) then
+    let c = out_gen (topwit wit_constr) v in
+    ([], c)
+  else if has_type v (topwit wit_constr_under_binders) then
+    out_gen (topwit wit_constr_under_binders) v
+  else raise Not_found
+
+let coerce_to_closed_constr env v =
+  let ids,c = coerce_to_constr env v in
+  if not (List.is_empty ids) then raise Not_found;
+  c
+
+let coerce_to_evaluable_ref env v =
+  let fail () = raise (CannotCoerceTo "an evaluable reference") in
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroIdentifier id when List.mem id (Termops.ids_of_context env) -> EvalVarRef id
+    | _ -> fail ()
+  else
+    let ev = match Value.to_constr v with
+    | Some c when isConst c -> EvalConstRef (destConst c)
+    | Some c when isVar c -> EvalVarRef (destVar c)
+    | _ -> fail ()
+    in
+    if Tacred.is_evaluable env ev then ev else fail ()
+
+let coerce_to_constr_list env v =
+  let v = Value.to_list v in
+  match v with
+  | Some l ->
+    let map v = coerce_to_closed_constr env v in
+    List.map map l
+  | None -> raise Not_found
+
+let coerce_to_intro_pattern_list loc env v =
+  match Value.to_list v with
+  | None -> raise Not_found
+  | Some l ->
+    let map v = (loc, coerce_to_intro_pattern env v) in
+    List.map map l
+
+let coerce_to_hyp env v =
+  let fail () = raise (CannotCoerceTo "a variable") in
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroIdentifier id when is_variable env id -> id
+    | _ -> fail ()
+  else match Value.to_constr v with
+  | Some c when isVar c -> destVar c
+  | _ -> fail ()
+
+let coerce_to_hyp_list env v =
+  let v = Value.to_list v in
+  match v with
+  | Some l ->
+    let map n = coerce_to_hyp env n in
+    List.map map l
+  | None -> raise Not_found
+
+(* Interprets a qualified name *)
+let coerce_to_reference env v =
+  let v = Value.normalize v in
+  match Value.to_constr v with
+  | Some c ->
+    begin
+      try Globnames.global_of_constr c
+      with Not_found -> raise (CannotCoerceTo "a reference")
+    end
+  | None -> raise (CannotCoerceTo "a reference")
+
+let coerce_to_inductive v =
+  match Value.to_constr v with
+  | Some c when isInd c -> destInd c
+  | _ -> raise (CannotCoerceTo "an inductive type")
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let coerce_to_quantified_hypothesis v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    let v = out_gen (topwit wit_intro_pattern) v in
+    match v with
+    | _, IntroIdentifier id -> NamedHyp id
+    | _ -> raise (CannotCoerceTo "a quantified hypothesis")
+  else if has_type v (topwit wit_int) then
+    AnonHyp (out_gen (topwit wit_int) v)
+  else raise (CannotCoerceTo "a quantified hypothesis")
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let coerce_to_decl_or_quant_hyp env v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_int) then
+    AnonHyp (out_gen (topwit wit_int) v)
+  else
+    try
+      let hyp = coerce_to_hyp env v in
+      NamedHyp hyp
+    with CannotCoerceTo _ ->
+      raise (CannotCoerceTo "a declared or quantified hypothesis")
+
+let coerce_to_int_or_var_list v =
+  match Value.to_list v with
+  | None -> raise Not_found
+  | Some l ->
+    let map n = ArgArg (coerce_to_int n) in
+    List.map map l
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
new file mode 100644
index 000000000..f9ffb70a5
--- /dev/null
+++ b/tactics/taccoerce.mli
@@ -0,0 +1,89 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Names
+open Term
+open Misctypes
+open Pattern
+open Genarg
+
+(** Coercions from highest level generic arguments to actual data used by Ltac
+    interpretation. Those functions examinate dynamic types and try to return
+    something sensible according to the object content. *)
+
+exception CannotCoerceTo of string
+(** Exception raised whenever a coercion failed. *)
+
+(** {5 High-level access to values}
+
+  The [of_*] functions cast a given argument into a value. The [to_*] do the
+  converse, and return [None] if there is a type mismatch.
+
+*)
+
+module Value :
+sig
+  type t = tlevel generic_argument
+  (** Tactics manipulate [tlevel generic_argument]. *)
+
+  val normalize : t -> t
+  (** Eliminated the leading dynamic type casts. *)
+
+  val of_constr : constr -> t
+  val to_constr : t -> constr option
+  val of_int : int -> t
+  val to_int : t -> int option
+  val to_list : t -> t list option
+end
+
+(** {5 Coercion functions} *)
+
+val coerce_to_constr_context : Value.t -> constr
+
+val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t
+
+val coerce_to_intro_pattern : Environ.env -> Value.t -> intro_pattern_expr
+
+val coerce_to_hint_base : Value.t -> string
+
+val coerce_to_int : Value.t -> int
+
+val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
+
+val coerce_to_closed_constr : Environ.env -> Value.t -> constr
+
+val coerce_to_evaluable_ref :
+  Environ.env -> Value.t -> evaluable_global_reference
+
+val coerce_to_constr_list : Environ.env -> Value.t -> constr list
+
+val coerce_to_intro_pattern_list :
+  Loc.t -> Environ.env -> Value.t -> intro_pattern_expr Loc.located list
+
+val coerce_to_hyp : Environ.env -> Value.t -> Id.t
+
+val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
+
+val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
+
+val coerce_to_inductive : Value.t -> inductive
+
+val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
+
+val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
+
+val coerce_to_int_or_var_list : Value.t -> int or_var list
+
+(** {5 Missing generic arguments} *)
+
+val wit_unit : (unit, unit, unit) genarg_type
+
+val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
+
+val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4408c6336..0df40d05b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -41,6 +41,7 @@ open Misctypes
 open Miscops
 open Locus
 open Tacintern
+open Taccoerce
 
 let safe_msgnl s =
   let _ =
@@ -62,58 +63,10 @@ type tacvalue =
 let (wit_tacvalue : (Empty.t, Empty.t, tacvalue) Genarg.genarg_type) =
   Genarg.create_arg None "tacvalue"
 
-let (wit_unit : (unit, unit, unit) Genarg.genarg_type) =
-  Genarg.create_arg None "unit"
-
-let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
-  Genarg.create_arg None "constr_context"
-
-(* includes idents known to be bound and references *)
-let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
-  Genarg.create_arg None "constr_under_binders"
-
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
 
-module Value =
-struct
-
-type t = value
-
-let rec normalize v =
-  if has_type v (topwit wit_genarg) then
-    normalize (out_gen (topwit wit_genarg) v)
-  else v
-
-let of_constr c = in_gen (topwit wit_constr) c
-
-let to_constr v =
-  let v = normalize v in
-  if has_type v (topwit wit_constr) then
-    let c = out_gen (topwit wit_constr) v in
-    Some c
-  else if has_type v (topwit wit_constr_under_binders) then
-    let vars, c = out_gen (topwit wit_constr_under_binders) v in
-    match vars with [] -> Some c | _ -> None
-  else None
-
-let of_int i = in_gen (topwit wit_int) i
-
-let to_int v =
-  let v = normalize v in
-  if has_type v (topwit wit_int) then
-    Some (out_gen (topwit wit_int) v)
-  else None
-
-let to_list v =
-  let v = normalize v in
-  try Some (fold_list0 (fun v accu -> v :: accu) v [])
-  with Failure _ ->
-    try Some (fold_list1 (fun v accu -> v :: accu) v [])
-    with Failure _ ->
-      None
-
-end
+module Value = Taccoerce.Value
 
 let dloc = Loc.ghost
 
@@ -150,13 +103,6 @@ let check_is_value v =
     | _ -> ()
   else ()
 
-(* Gives the constr corresponding to a Constr_context tactic_arg *)
-let coerce_to_constr_context v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_constr_context) then
-    out_gen (topwit wit_constr_context) v
-  else errorlabstrm "coerce_to_constr_context" (str "Not a context variable.")
-
 (* Displays a value *)
 let rec pr_value env v = str "a tactic"
 
@@ -340,8 +286,6 @@ let error_ltac_variable loc id env v s =
    strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
    strbrk "which cannot be coerced to " ++ str s ++ str".")
 
-exception CannotCoerceTo of string
-
 (* Raise Not_found if not in interpretation sign *)
 let try_interp_ltac_var coerce ist env (loc,id) =
   let v = List.assoc id ist.lfun in
@@ -351,22 +295,6 @@ let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
   with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
 
-(* Interprets an identifier which must be fresh *)
-let coerce_to_ident fresh env v =
-  let v = Value.normalize v in
-  let fail () = raise (CannotCoerceTo "a fresh identifier") in
-  if has_type v (topwit wit_intro_pattern) then
-    match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id -> id
-    | _ -> fail ()
-  else match Value.to_constr v with
-  | None -> fail ()
-  | Some c ->
-    (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
-    if isVar c && not (fresh && is_variable env (destVar c)) then
-      destVar c
-    else fail ()
-
 let interp_ident_gen fresh ist env id =
   try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id)
   with Not_found -> id
@@ -381,39 +309,14 @@ let interp_fresh_name ist env = function
   | Anonymous -> Anonymous
   | Name id -> Name (interp_fresh_ident ist env id)
 
-let coerce_to_intro_pattern env v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_intro_pattern) then
-    snd (out_gen (topwit wit_intro_pattern) v)
-  else match Value.to_constr v with
-  | Some c when isVar c ->
-      (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
-      (* but also in "destruct H as (H,H')" *)
-      IntroIdentifier (destVar c)
-  | _ -> raise (CannotCoerceTo "an introduction pattern")
-
 let interp_intro_pattern_var loc ist env id =
   try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env) (loc,id)
   with Not_found -> IntroIdentifier id
 
-let coerce_to_hint_base v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_intro_pattern) then
-    match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id -> Id.to_string id
-    | _ -> raise (CannotCoerceTo "a hint base name")
-  else raise (CannotCoerceTo "a hint base name")
-
 let interp_hint_base ist s =
   try try_interp_ltac_var coerce_to_hint_base ist None (dloc,Id.of_string s)
   with Not_found -> s
 
-let coerce_to_int v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_int) then
-    out_gen (topwit wit_int) v
-  else raise (CannotCoerceTo "an integer")
-
 let interp_int ist locid =
   try try_interp_ltac_var coerce_to_int ist None locid
   with Not_found ->
@@ -424,51 +327,15 @@ let interp_int_or_var ist = function
   | ArgVar locid -> interp_int ist locid
   | ArgArg n -> n
 
-let int_or_var_list_of_VList v =
-  match Value.to_list v with
-  | None -> raise Not_found
-  | Some l ->
-    let map n = ArgArg (coerce_to_int n) in
-    List.map map l
-
 let interp_int_or_var_as_list ist = function
   | ArgVar (_,id as locid) ->
-      (try int_or_var_list_of_VList (List.assoc id ist.lfun)
+      (try coerce_to_int_or_var_list (List.assoc id ist.lfun)
        with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)])
   | ArgArg n as x -> [x]
 
 let interp_int_or_var_list ist l =
   List.flatten (List.map (interp_int_or_var_as_list ist) l)
 
-let coerce_to_constr env v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_intro_pattern) then
-    match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id -> ([],constr_of_id env id)
-    | _ -> raise Not_found
-  else if has_type v (topwit wit_constr) then
-    let c = out_gen (topwit wit_constr) v in
-    ([], c)
-  else if has_type v (topwit wit_constr_under_binders) then
-    out_gen (topwit wit_constr_under_binders) v
-  else raise Not_found
-
-let coerce_to_closed_constr env v =
-  let ids,c = coerce_to_constr env v in
-  if not (List.is_empty ids) then raise Not_found;
-  c
-
-let coerce_to_hyp env v =
-  let fail () = raise (CannotCoerceTo "a variable") in
-  let v = Value.normalize v in
-  if has_type v (topwit wit_intro_pattern) then
-    match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id when is_variable env id -> id
-    | _ -> fail ()
-  else match Value.to_constr v with
-  | Some c when isVar c -> destVar c
-  | _ -> fail ()
-
 (* Interprets a bound variable (especially an existing hypothesis) *)
 let interp_hyp ist gl (loc,id as locid) =
   let env = pf_env gl in
@@ -480,14 +347,6 @@ let interp_hyp ist gl (loc,id as locid) =
   else user_err_loc (loc,"eval_variable",
     str "No such hypothesis: " ++ pr_id id ++ str ".")
 
-let coerce_to_hyp_list env v =
-  let v = Value.to_list v in
-  match v with
-  | Some l ->
-    let map n = coerce_to_hyp env n in
-    List.map map l
-  | None -> raise Not_found
-
 let interp_hyp_list_as_list ist gl (loc,id as x) =
   try coerce_to_hyp_list (pf_env gl) (List.assoc id ist.lfun)
   with Not_found | CannotCoerceTo _ -> [interp_hyp ist gl x]
@@ -501,17 +360,6 @@ let interp_move_location ist gl = function
   | MoveFirst -> MoveFirst
   | MoveLast -> MoveLast
 
-(* Interprets a qualified name *)
-let coerce_to_reference env v =
-  let v = Value.normalize v in
-  match Value.to_constr v with
-  | Some c ->
-    begin
-      try global_of_constr c
-      with Not_found -> raise (CannotCoerceTo "a reference")
-    end
-  | None -> raise (CannotCoerceTo "a reference")
-
 let interp_reference ist env = function
   | ArgArg (_,r) -> r
   | ArgVar locid ->
@@ -519,30 +367,10 @@ let interp_reference ist env = function
 
 let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
 
-let coerce_to_inductive v =
-  match Value.to_constr v with
-  | Some c when isInd c -> destInd c
-  | _ -> raise (CannotCoerceTo "an inductive type")
-
 let interp_inductive ist = function
   | ArgArg r -> r
   | ArgVar locid -> interp_ltac_var coerce_to_inductive ist None locid
 
-let coerce_to_evaluable_ref env v =
-  let fail () = raise (CannotCoerceTo "an evaluable reference") in
-  let v = Value.normalize v in
-  if has_type v (topwit wit_intro_pattern) then
-    match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id when List.mem id (ids_of_context env) -> EvalVarRef id
-    | _ -> fail ()
-  else
-    let ev = match Value.to_constr v with
-    | Some c when isConst c -> EvalConstRef (destConst c)
-    | Some c when isVar c -> EvalVarRef (destVar c)
-    | _ -> fail ()
-    in
-    if Tacred.is_evaluable env ev then ev else fail ()
-
 let interp_evaluable ist env = function
   | ArgArg (r,Some (loc,id)) ->
       (* Maybe [id] has been introduced by Intro-like tactics *)
@@ -707,14 +535,6 @@ let pf_interp_casted_constr ist gl c =
 let pf_interp_constr ist gl =
   interp_constr ist (pf_env gl) (project gl)
 
-let coerce_to_constr_list env v =
-  let v = Value.to_list v in
-  match v with
-  | Some l ->
-    let map v = coerce_to_closed_constr env v in
-    List.map map l
-  | None -> raise Not_found
-
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
     try match dest_fun x with
@@ -880,13 +700,6 @@ let interp_message ist gl l =
      are raised now and not at printing time *)
   prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist gl) l)
 
-let coerce_to_intro_pattern_list loc env v =
-  match Value.to_list v with
-  | None -> raise Not_found
-  | Some l ->
-    let map v = (loc, coerce_to_intro_pattern env v) in
-    List.map map l
-
 let rec interp_intro_pattern ist gl = function
   | loc, IntroOrAndPattern l ->
       loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l)
@@ -910,19 +723,6 @@ and interp_intro_pattern_list_as_list ist gl = function
 let interp_in_hyp_as ist gl (id,ipat) =
   (interp_hyp ist gl id,Option.map (interp_intro_pattern ist gl) ipat)
 
-(* Quantified named or numbered hypothesis or hypothesis in context *)
-(* (as in Inversion) *)
-let coerce_to_quantified_hypothesis v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_intro_pattern) then
-    let v = out_gen (topwit wit_intro_pattern) v in
-    match v with
-    | _, IntroIdentifier id -> NamedHyp id
-    | _ -> raise (CannotCoerceTo "a quantified hypothesis")
-  else if has_type v (topwit wit_int) then
-    AnonHyp (out_gen (topwit wit_int) v)
-  else raise (CannotCoerceTo "a quantified hypothesis")
-
 let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
@@ -938,19 +738,6 @@ let interp_binding_name ist = function
       try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
       with Not_found -> NamedHyp id
 
-(* Quantified named or numbered hypothesis or hypothesis in context *)
-(* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_int) then
-    AnonHyp (out_gen (topwit wit_int) v)
-  else
-    try
-      let hyp = coerce_to_hyp env v in
-      NamedHyp hyp
-    with CannotCoerceTo _ ->
-      raise (CannotCoerceTo "a declared or quantified hypothesis")
-
 let interp_declared_or_quantified_hypothesis ist gl = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 7c04899f3..8395306b6 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -21,7 +21,7 @@ open Misctypes
 
 module Value :
 sig
-  type t
+  type t = tlevel generic_argument
   val of_constr : constr -> t
   val to_constr : t -> constr option
   val of_int : int -> t
@@ -119,8 +119,6 @@ val declare_xml_printer :
 
 (** Internals that can be useful for syntax extensions. *)
 
-exception CannotCoerceTo of string
-
 val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> Id.t Loc.located -> 'a
 
 val interp_int : interp_sign -> Id.t Loc.located -> int
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 7dab21acf..c08cc66da 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -16,6 +16,7 @@ Refine
 Inv
 Leminv
 Tacsubst
+Taccoerce
 Tacintern
 Tacinterp
 Evar_tactics