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/clambda.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/clambda.mli')

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
 
-- 
cgit v1.2.3