Add relevance marks on binders.

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

1 files changed, 6 insertions, 6 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5fec55fea1..a29f3c6833 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -98,7 +98,7 @@ module type RedFlagsSig = sig
   val red_projection : reds -> Projection.t -> bool
 end
 
-module RedFlags = (struct
+module RedFlags : RedFlagsSig = struct
 
   (* [r_const=(true,cl)] means all constants but those in [cl] *)
   (* [r_const=(false,cl)] means only those in [cl] *)
@@ -195,7 +195,7 @@ module RedFlags = (struct
     if Projection.unfolded p then true
     else red_set red (fCONST (Projection.constant p))
 
-end : RedFlagsSig)
+end
 
 open RedFlags
 
@@ -300,9 +300,9 @@ and fterm =
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
-  | FProd of Name.t * fconstr * constr * fconstr subs
-  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
+  | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
+  | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
   | FLIFT of int * fconstr
@@ -865,7 +865,7 @@ let rec knh info m stk =
     | FLOCKED -> assert false
     | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
     | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
-    | FFix(((ri,n),(_,_,_)),_) ->
+    | FFix(((ri,n),_),_) ->
         (match get_nth_arg m ri.(n) stk with
              (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
            | (None, stk') -> (m,stk'))