From 79ccbe6b2b73409d7ce5e0e5797320b6e2fd0dd2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 Apr 2020 09:57:27 +0200
Subject: Making type interning_data abstract in constrintern.ml.

---
 vernac/comProgramFixpoint.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 80e7e6ab96..5b29ab2092 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -195,13 +195,14 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let lift_lets = lift_rel_context 1 letbinders in
   let sigma, intern_body =
     let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
-    let (r, impls, scopes) =
+    let interning_data =
       Constrintern.compute_internalization_data env sigma
         Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
-        (r, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
-         scopes @ [None]) in
+        (Constrintern.extend_internalization_data interning_data
+           (Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false)))
+           None) in
     interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
       ~impls:newimpls body (lift 1 top_arity)
   in
-- 
cgit v1.2.3