diff options
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6f6122d504..aff60eaa4e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -38,12 +38,12 @@ let _True = reference ["Init";"Logic"] "True" let _I = reference ["Init";"Logic"] "I" let whd env= - let infos=Closure.create_clos_infos Closure.betaiotazeta env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let whd_delta env= - let infos=Closure.create_clos_infos Closure.all env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) (* decompose member of equality in an applicative format *) |