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.
---
 vernac/comProgramFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 5b29ab2092..bf38088f71 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -196,7 +196,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let sigma, intern_body =
     let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
     let interning_data =
-      Constrintern.compute_internalization_data env sigma
+      Constrintern.compute_internalization_data env sigma recname
         Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
-- 
cgit v1.2.3