diff options
| author | Gaëtan Gilbert | 2020-07-09 11:32:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-09 11:32:41 +0200 |
| commit | 577ec77f17a872d6bc36073ceeb3cf582fcf01c4 (patch) | |
| tree | 93729a8f221b9d47269279c3672afc2b6854e1ba /vernac/classes.mli | |
| parent | 769823c425f1b3ffc87141ede814976f6cf44128 (diff) | |
| parent | 3ef2bd35926a83fbcfd34d03e1fb1db894a39627 (diff) | |
Merge PR #11836: [obligations] Functionalize Program state
Reviewed-by: SkySkimmer
Ack-by: gares
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index 07695b5bef..e1816fb138 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -52,6 +52,7 @@ val new_instance val new_instance_program : ?global:bool (** Not global by default. *) + -> pm:Declare.OblState.t -> poly:bool -> name_decl -> local_binder_expr list @@ -60,7 +61,7 @@ val new_instance_program -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) -> Vernacexpr.hint_info_expr - -> Id.t + -> Declare.OblState.t * Id.t val declare_new_instance : ?global:bool (** Not global by default. *) |