diff options
| author | Pierre-Marie Pédrot | 2020-06-26 12:43:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:17:20 +0200 |
| commit | f34dcb97406611704c93970ea623d6a8587e5ba8 (patch) | |
| tree | 5a636c498c4c3fad7c15cc266dd8a386b85123e1 /tactics/tactics.ml | |
| parent | e5b355107d985d7efe2976b9eee9b6c182e25f24 (diff) | |
Moving the remaining Refiner functions to Tacmach.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index eb7f2190a8..af23747d43 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -30,7 +30,6 @@ open Genredexpr open Tacmach.New open Logic open Clenv -open Refiner open Tacticals open Hipattern open Coqlib @@ -355,7 +354,7 @@ let fresh_id_in_env avoid id env = next_ident_away_in_goal id avoid let fresh_id avoid id gl = - fresh_id_in_env avoid id (pf_env gl) + fresh_id_in_env avoid id (Tacmach.pf_env gl) let new_fresh_id avoid id gl = fresh_id_in_env avoid id (Proofview.Goal.env gl) @@ -1007,7 +1006,7 @@ let find_intro_names ctxt gl = let name = fresh_id avoid (default_id env gl.sigma decl) gl in let newenv = push_rel decl env in (newenv, name :: idl, Id.Set.add name avoid)) - ctxt (pf_env gl, [], Id.Set.empty) in + ctxt (Tacmach.pf_env gl, [], Id.Set.empty) in List.rev res let build_intro_tac id dest tac = match dest with |