diff options
| author | Pierre Courtieu | 2016-01-12 16:06:51 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2016-01-12 16:06:51 +0100 |
| commit | be824224cc76f729872e9d803fc64831b95aee94 (patch) | |
| tree | c4056d41a6437ee6db3a6a082abbd1daa9759299 | |
| parent | 4f1aa43babc8fdb1704d7b13d3b367e4e8044e6e (diff) | |
Adding support for fresh for meta's and evar's.
| -rw-r--r-- | tactics/taccoerce.ml | 10 | ||||
| -rw-r--r-- | tactics/taccoerce.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
3 files changed, 10 insertions, 4 deletions
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 8ee52c96f3..371ae7040b 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -102,10 +102,14 @@ let coerce_var_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 env v = +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 @@ -119,7 +123,9 @@ let coerce_to_ident_not_fresh env v = | None -> fail () | Some c -> match Constr.kind c with - | Var id -> id + | Var id -> id + | Meta m -> id_of_name (Evd.meta_name g m) + | Evar (kn,_) -> (Evd.evar_ident kn g) | Const (cst,_) -> Label.to_id (Constant.label cst) | Construct (cstr,_) -> let ref = Globnames.ConstructRef cstr in diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index bf522b6116..de7651a1a9 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -50,7 +50,7 @@ val coerce_to_constr_context : Value.t -> constr val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t -val coerce_to_ident_not_fresh : 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 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c2e3400835..77a1cce78e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -479,7 +479,7 @@ 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 env) + 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 |