diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /tactics/redexpr.ml | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
Diffstat (limited to 'tactics/redexpr.ml')
| -rw-r--r-- | tactics/redexpr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 9c2df71f82..b415b30de8 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -81,7 +81,7 @@ let subst_strategy (subs,(local,obj)) = local, List.Smart.map (fun (k,ql as entry) -> - let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.Smart.map (Tacred.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj @@ -344,7 +344,7 @@ let subst_red_expr subs = let sigma = Evd.from_env env in Redops.map_red_expr_gen (subst_mps subs) - (Mod_subst.subst_evaluable_reference subs) + (Tacred.subst_evaluable_reference subs) (Patternops.subst_pattern env sigma subs) let inReduction : bool * string * red_expr -> obj = |