diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-27 16:30:32 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 12:14:05 +0200 |
| commit | cf95f2a791c263c7aaa3b488d1b09eaafc29be2b (patch) | |
| tree | 72515081ec6bf1e2d75362767aa2bcc0ce08b48d /toplevel | |
| parent | f14b6f1a17652566f0cbc00ce81421ba0684dad5 (diff) | |
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
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 750f7a60c..1be5226de 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 04c01f3cd..e4a2ca5a0 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) *) |