diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-10 14:17:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-10 14:19:10 +0100 |
| commit | 10e3c8e59664ed5137cd650ba6e0704943c511e8 (patch) | |
| tree | 79467b438b5fec7fa54ca0564bcb16ad431236f9 /toplevel | |
| parent | 1b55adb1bea6d0e51fff54d9d94d95d8185476b7 (diff) | |
Removing OCaml deprecated function names from the Lazy module.
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 284bcd75e..38bc0e568 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 c63dac302..02f8c1717 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 |