diff options
| author | Pierre-Marie Pédrot | 2020-08-27 16:50:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-27 16:50:45 +0200 |
| commit | 1abf7c94f97948f8171c2fe1fec99cd890e8d1f6 (patch) | |
| tree | 3c60f0cd4a38608dacceca0b012de120bdc46a79 /tactics | |
| parent | f140359a6df94d1caa2ccea3da2d48e01eacc44b (diff) | |
| parent | 4ee0cedff7726a56ebd53125995a7ae131660b4a (diff) | |
Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
Diffstat (limited to 'tactics')
| -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 c463c06cd5..a8747e0a7c 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -60,7 +60,7 @@ let set_strategy_one ref l = Global.set_strategy k l; match k,l with ConstKey sp, Conv_oracle.Opaque -> - Csymtable.set_opaque_const sp + Vmsymtable.set_opaque_const sp | ConstKey sp, _ -> let cb = Global.lookup_constant sp in (match cb.const_body with @@ -69,7 +69,7 @@ let set_strategy_one ref l = (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); - | _ -> Csymtable.set_transparent_const sp) + | _ -> Vmsymtable.set_transparent_const sp) | _ -> () let cache_strategy (_,str) = |