diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 284bcd75ec..38bc0e568e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -877,7 +877,7 @@ let well_founded = init_constant ["Init"; "Wf"] "well_founded" let mkSubset name typ prop = mkApp (Universes.constr_of_global (delayed_force build_sigma).typ, [| typ; mkLambda (name, typ, prop) |]) -let sigT = Lazy.lazy_from_fun build_sigma_type +let sigT = Lazy.from_fun build_sigma_type let make_qref s = Qualid (Loc.ghost, qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c63dac3026..02f8c17175 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -334,7 +334,7 @@ let dump_universes_gen g s = | Univ.Eq -> Printf.fprintf output " \"%s\" -> \"%s\" [style=dashed];\n" left right end, begin fun () -> - if Lazy.lazy_is_val init then Printf.fprintf output "}\n"; + if Lazy.is_val init then Printf.fprintf output "}\n"; close_out output end end else begin |