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

3 files changed, 57 insertions, 5 deletions

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index ab61c8abb..649764da3 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -385,7 +385,7 @@ let interp_ltac_var coerce ist env locid =
   with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
 
 let interp_ident ist env sigma id =
-  try try_interp_ltac_var (coerce_to_ident false env) ist (Some (env,sigma)) (dloc,id)
+  try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id)
   with Not_found -> id
 
 let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl)
@@ -541,6 +541,10 @@ let extract_ids ids lfun =
 let default_fresh_id = Id.of_string "H"
 
 let interp_fresh_id ist env sigma l =
+  let extract_ident ist env sigma id =
+    try try_interp_ltac_var (coerce_to_ident_not_fresh sigma env)
+			    ist (Some (env,sigma)) (dloc,id)
+    with Not_found -> id in
   let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
   let avoid = match TacStore.get ist.extra f_avoid_ids with
   | None -> []
@@ -553,7 +557,7 @@ let interp_fresh_id ist env sigma l =
       let s =
 	String.concat "" (List.map (function
 	  | ArgArg s -> s
-	  | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in
+	  | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in
       let s = if CLexer.is_keyword s then s^"0" else s in
       Id.of_string s in
   Tactics.fresh_id_in_env avoid id env
@@ -570,7 +574,7 @@ let extract_ltac_constr_context ist env =
     with CannotCoerceTo _ -> map
   in
   let add_ident id env v map =
-    try Id.Map.add id (coerce_to_ident false env v) map
+    try Id.Map.add id (coerce_var_to_ident false env v) map
     with CannotCoerceTo _ -> map
   in
   let fold id v {idents;typed;untyped} =
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index d53c1cc04..0110510d3 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 7a963f95f..0b67f8726 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