diff options
| author | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
| commit | 61aeca9ca2a7c46b143b90583dfb84b037eccc5b (patch) | |
| tree | 936cab27bacc3bb779aff810be7b79425544f10d /vernac/comAssumption.mli | |
| parent | 6e5fee168d874b7b6fe7d5c8f4384661bf328d79 (diff) | |
| parent | c62aa0e9d0c33a70822e66a422d4c5926a8c8df7 (diff) | |
Merge PR #12372: [declare] Refactor constant information into a record.
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/comAssumption.mli')
| -rw-r--r-- | vernac/comAssumption.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 989015a9f3..3d425ad768 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -17,7 +17,7 @@ open Constrexpr val do_assumptions : program_mode:bool -> poly:bool - -> scope:Declare.locality + -> scope:Locality.locality -> kind:Decls.assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list @@ -35,7 +35,7 @@ val declare_variable val declare_axiom : coercion_flag -> poly:bool - -> local:Declare.import_status + -> local:Locality.import_status -> kind:Decls.assumption_object_kind -> Constr.types -> Entries.universes_entry * UnivNames.universe_binders |