diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |