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 +-
 vernac/declare.ml     | 6 ++++--
 vernac/declare.mli    | 3 ---
 3 files changed, 5 insertions(+), 6 deletions(-)

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
   ()
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 0c98ac9070..65f0265b3e 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -943,7 +943,7 @@ module Recthm = struct
     }
 end
 
-let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
+let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
   let vars, fixdecls, indexes =
     mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
   let uctx, univs =
@@ -969,6 +969,8 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
 
+let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true
+
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
@@ -1540,7 +1542,7 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let udecl = UState.default_univ_decl in
   let kns =
-    declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns
+    declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns
       ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
       ~restrict_ucontext:false fixitems
   in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 4e2ba1833f..5339f4702b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -350,9 +350,6 @@ val declare_mutually_recursive
   -> ntns:Vernacexpr.decl_notation list
   -> rec_declaration:Constr.rec_declaration
   -> possible_indexes:lemma_possible_guards option
-  -> ?restrict_ucontext:bool
-  (** XXX: restrict_ucontext should be always true, this seems like a
-     bug in obligations, so this parameter should go away *)
   -> Recthm.t list
   -> Names.GlobRef.t list
 
-- 
cgit v1.2.3