diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/obligations.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 750f7a60cb..1be5226deb 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -262,7 +262,7 @@ let pperror cmd = CErrors.errorlabstrm "Program" cmd let error s = pperror (str s) let reduce c = - Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c + Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c exception NoObligations of Id.t option diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 04c01f3cd1..e4a2ca5a02 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1287,8 +1287,8 @@ let _ = optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; - optread = (fun () -> !Closure.share); - optwrite = (fun b -> Closure.share := b) } + optread = (fun () -> !CClosure.share); + optwrite = (fun b -> CClosure.share := b) } (* No more undo limit in the new proof engine. The command still exists for compatibility (e.g. with ProofGeneral) *) |