From d9d4dcb41d8a63b7d535200b68bcbef4a38993df Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 03:34:03 +0200
Subject: [declare] Turn restrict_ucontext hack into an internal parameter

This is not needed outside of `Declare` now.
---
 vernac/comFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 80ca85e9a6..0b75e7f410 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -285,7 +285,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let fix_kind = Decls.IsDefinition fix_kind in
   let _ : GlobRef.t list =
     Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
-      ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
+      ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration
       fixitems
   in
   ()
-- 
cgit v1.2.3