diff options
| author | Maxime Dénès | 2019-01-25 17:47:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-05 09:36:51 +0100 |
| commit | 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 (patch) | |
| tree | e6697a39eb0cfb7b45a08e88dd08ad2fe7eedadb /vernac/classes.mli | |
| parent | 5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff) | |
Make Program a regular attribute
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index 6f61da66cf..7e0ec42625 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -55,6 +55,7 @@ val new_instance : val declare_new_instance : ?global:bool (** Not global by default. *) -> + program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> ident_decl * Decl_kinds.binding_kind * constr_expr -> |