From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 31 Oct 2017 17:04:02 +0100 Subject: Add relevance marks on binders. Kernel should be mostly correct, higher levels do random stuff at times. --- kernel/nativelambda.mli | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'kernel/nativelambda.mli') 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 -- cgit v1.2.3