Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

1 files changed, 5 insertions, 5 deletions

diff --git a/kernel/clambda.mli b/kernel/clambda.mli
index 4d921fd45e..1476bb6e45 100644
--- a/kernel/clambda.mli
+++ b/kernel/clambda.mli
@@ -8,8 +8,8 @@ type lambda =
   | Lvar          of Id.t
   | Levar         of Evar.t * lambda array
   | Lprod         of lambda * lambda
-  | Llam          of Name.t array * lambda
-  | Llet          of Name.t * lambda * lambda
+  | Llam          of Name.t Context.binder_annot array * lambda
+  | Llet          of Name.t Context.binder_annot * lambda * lambda
   | Lapp          of lambda * lambda array
   | Lconst        of pconstant
   | Lprim         of pconstant option * CPrimitives.t * lambda array
@@ -28,15 +28,15 @@ type lambda =
 
 and lam_branches =
   { constant_branches : lambda array;
-    nonconstant_branches : (Name.t array * lambda) array }
+    nonconstant_branches : (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
 
 exception TooLargeInductive of Pp.t
 
 val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda
 
-val decompose_Llam : lambda -> Name.t array * lambda
+val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda
 
 val get_alias : env -> Constant.t -> Constant.t