diff options
| author | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
| commit | 4ee0cedff7726a56ebd53125995a7ae131660b4a (patch) | |
| tree | f5049f849a27b518f5c27298058df620a0ca38b3 /tactics/redexpr.ml | |
| parent | aa926429727f1f6b5ef07c8912f2618d53f6d155 (diff) | |
Rename VM-related kernel/cfoo files to kernel/vmfoo
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 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) = |