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/command.ml | |
| parent | 1b55adb1bea6d0e51fff54d9d94d95d8185476b7 (diff) | |
Removing OCaml deprecated function names from the Lazy module.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 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" |