diff options
| author | Emilio Jesus Gallego Arias | 2020-05-22 03:34:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-26 18:28:08 +0200 |
| commit | d9d4dcb41d8a63b7d535200b68bcbef4a38993df (patch) | |
| tree | bfb3c3cd7f27bf6634382b4003c3e362b7be4564 /vernac/comFixpoint.ml | |
| parent | baef9828c3e6ea11fce2e172797f0f67e51885ad (diff) | |
[declare] Turn restrict_ucontext hack into an internal parameter
This is not needed outside of `Declare` now.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 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 () |