diff options
| author | Pierre-Marie Pédrot | 2018-06-22 00:43:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 (patch) | |
| tree | 9f54ad363b2c8f855be97860ba1900572353e164 /kernel/vconv.ml | |
| parent | ecfbeaa62f9d8bd4dc4600cf39df2262af718313 (diff) | |
Move transparent_state to its own module.
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index c1130e62c9..46e52121c7 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed = let vm_conv_gen cv_pb env univs t1 t2 = if not (typing_flags env).Declarations.enable_VM then Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - full_transparent_state env univs t1 t2 + TranspState.full env univs t1 t2 else try let v1 = val_of_constr env t1 in @@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 = with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - full_transparent_state env univs t1 t2 + TranspState.full env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in |