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.
---
 plugins/extraction/table.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction/table.ml')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2058837b8e..399a77c596 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -449,11 +449,11 @@ let argnames_of_global r =
   let typ, _ = Typeops.type_of_global_in_context env r in
   let rels,_ =
     decompose_prod (Reduction.whd_all env typ) in
-  List.rev_map fst rels
+  List.rev_map (fun x -> Context.binder_name (fst x)) rels
 
 let msg_of_implicit = function
   | Kimplicit (r,i) ->
-     let name = match List.nth (argnames_of_global r) (i-1) with
+     let name = match (List.nth (argnames_of_global r) (i-1)) with
        | Anonymous -> ""
        | Name id -> "(" ^ Id.to_string id ^ ") "
      in
-- 
cgit v1.2.3