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 /kernel/inductive.ml | |
| parent | 1b55adb1bea6d0e51fff54d9d94d95d8185476b7 (diff) | |
Removing OCaml deprecated function names from the Lazy module.
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 551632962..499cbf0df 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -480,7 +480,7 @@ type guard_env = let make_renv env recarg tree = { env = env; rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *) - genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } + genv = [Lazy.from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = { env = push_rel (LocalAssum (x,ty)) renv.env; @@ -817,7 +817,7 @@ and stack_element_specif = function |SArg x -> x and extract_stack renv a = function - | [] -> Lazy.lazy_from_val Not_subterm , [] + | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t (* Check term c can be applied to one of the mutual fixpoints. *) |