diff options
| author | Pierre-Marie Pédrot | 2016-06-16 15:06:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-16 15:06:58 +0200 |
| commit | bce318b6d991587773ef2fb18c83de8d24bc4a5f (patch) | |
| tree | a68e910597a4c328d99747104a83145ff1319448 /ltac | |
| parent | 1b38f1256924df8897f1737e4b4124fbcc22c790 (diff) | |
| parent | caa1f67de10614984fa7e1c68aa8adf0ff90196a (diff) | |
Merge PR #100: fresh now accepts more things than just identifiers.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacinterp.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index ab61c8abba..649764da37 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} = |