diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e4bf055c95..383bdc2ef3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -354,6 +354,11 @@ if nmr = 0 then 0 else | _ -> k) in find 0 (n-1) (lpar,List.rev hyps) +let lambda_implicit_lift n a = + let implicit_sort = mkType (make_univ (make_dirpath [id_of_string "implicit"], 0)) in + let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in + iterate lambda_implicit n (lift n a) + (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc env ntyps npars lc = |