diff options
| author | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
| commit | d1d32f552064b9907fc9815b7412b9a9cde4a0dd (patch) | |
| tree | c4a4b20e92547abae487f8bb1115ba34382f0bfd /vernac/comAssumption.mli | |
| parent | 79b6317f738b6d2d7fdaaaad2cef79a092ec8c77 (diff) | |
| parent | 40ed1b7c5e94f418f9b758ffe1a86e4ad7743267 (diff) | |
Merge PR #9410: Make `Program` a regular attribute
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
Diffstat (limited to 'vernac/comAssumption.mli')
| -rw-r--r-- | vernac/comAssumption.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index c5bf3725a9..385ec33bea 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -17,7 +17,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) -val do_assumptions : locality * polymorphic * assumption_object_kind -> +val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) |