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/declare.mli | |
| parent | baef9828c3e6ea11fce2e172797f0f67e51885ad (diff) | |
[declare] Turn restrict_ucontext hack into an internal parameter
This is not needed outside of `Declare` now.
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 |