Merge PR #100: fresh now accepts more things than just identifiers.

2 files changed, 50 insertions, 2 deletions

diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index d53c1cc04a..0110510d35 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -107,7 +107,7 @@ let coerce_to_constr_context v =
   else raise (CannotCoerceTo "a term context")
 
 (* Interprets an identifier which must be fresh *)
-let coerce_to_ident fresh env v =
+let coerce_var_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
@@ -124,6 +124,52 @@ let coerce_to_ident fresh env v =
       destVar c
     else fail ()
 
+
+(* Interprets, if possible, a constr to an identifier which may not
+   be fresh but suitable to be given to the fresh tactic. Works for
+   vars, constants, inductive, constructors and sorts. *)
+let coerce_to_ident_not_fresh g env v =
+let id_of_name = function
+  | Names.Anonymous -> Id.of_string "x"
+  | Names.Name x -> x in
+  let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "an identifier") in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroNaming (IntroIdentifier id) -> id
+    | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    out_gen (topwit wit_var) v
+  else
+    match Value.to_constr v with
+    | None -> fail ()
+    | Some c ->
+       match Constr.kind c with
+       | Var id -> id 
+       | Meta m -> id_of_name (Evd.meta_name g m)
+       | Evar (kn,_) ->
+        begin match Evd.evar_ident kn g with
+        | None -> fail ()
+        | Some id -> id
+        end
+       | Const (cst,_) -> Label.to_id (Constant.label cst)
+       | Construct (cstr,_) ->
+	  let ref = Globnames.ConstructRef cstr in
+	  let basename = Nametab.basename_of_global ref in
+	  basename
+       | Ind (ind,_) ->
+	  let ref = Globnames.IndRef ind in
+	  let basename = Nametab.basename_of_global ref in
+	  basename
+       | Sort s ->
+	  begin
+	    match s with
+	    | Prop _ -> Label.to_id (Label.make "Prop")
+	    | Type _ -> Label.to_id (Label.make "Type")
+	  end
+       | _ -> fail()
+
+
 let coerce_to_intro_pattern env v =
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 7a963f95f3..0b67f8726e 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -50,7 +50,9 @@ end
 
 val coerce_to_constr_context : Value.t -> constr
 
-val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t
+val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
+
+val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t
 
 val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr