From 3f2742b2c3fd48706d4bfd8bffdd4ae07a338bbd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 6 Apr 2020 10:04:42 +0200
Subject: Coqdoc: Exporting location and unique id for binding variables.

This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.

In particular, this fixes #7697.
---
 plugins/funind/gen_principle.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index df147b3aa6..7626d6dbad 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -46,7 +46,7 @@ let build_newrecursive lnameargsardef =
           Constrintern.interp_context_evars ~program_mode:false env evd binders
         in
         let impl =
-          Constrintern.compute_internalization_data env0 evd
+          Constrintern.compute_internalization_data env0 evd recname
             Constrintern.Recursive arity impls'
         in
         let open Context.Named.Declaration in
-- 
cgit v1.2.3