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/subtyping.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index dea72e8b59..1857ea3329 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -23,6 +23,7 @@ open Declareops
 open Reduction
 open Inductive
 open Modops
+open Context
 open Mod_subst
 (*i*)
 
@@ -190,8 +191,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x);
   if mib1.mind_record <> NotRecord then begin
     let rec names_prod_letin t = match kind t with
-      | Prod(n,_,t) -> n::(names_prod_letin t)
-      | LetIn(n,_,_,t) -> n::(names_prod_letin t)
+      | Prod(n,_,t) -> n.binder_name::(names_prod_letin t)
+      | LetIn(n,_,_,t) -> n.binder_name::(names_prod_letin t)
       | Cast(t,_,_) -> names_prod_letin t
       | _ -> []
     in
-- 
cgit v1.2.3