diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /kernel/nativelambda.mli | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index eb06522a33..b0de257a27 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -21,9 +21,9 @@ type lambda = | Lmeta of metavariable * lambda (* type *) | Levar of Evar.t * lambda array (* arguments *) | Lprod of lambda * lambda - | Llam of Name.t array * lambda - | Lrec of Name.t * lambda - | Llet of Name.t * lambda * lambda + | Llam of Name.t Context.binder_annot array * lambda + | Lrec of Name.t Context.binder_annot * lambda + | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) @@ -45,9 +45,9 @@ type lambda = | Llazy | Lforce -and lam_branches = (constructor * Name.t array * lambda) array +and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array -and fix_decl = Name.t array * lambda array * lambda array +and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array type evars = { evars_val : existential -> constr option; @@ -55,8 +55,8 @@ type evars = val empty_evars : evars -val decompose_Llam : lambda -> Name.t array * lambda -val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda +val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda +val decompose_Llam_Llet : lambda -> (Name.t Context.binder_annot * lambda option) array * lambda val is_lazy : constr -> bool val mk_lazy : lambda -> lambda |