diff options
| author | Emilio Jesus Gallego Arias | 2020-05-25 14:57:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | a6d663c85d71b3cce007af23419e8030b8c5ac88 (patch) | |
| tree | c610d417d2132edbb2c634d2edf495a4946a0e7e /vernac/comDefinition.mli | |
| parent | d83e95cce852c5471593a27d0fdca39a262c885f (diff) | |
[declare] [api] Removal of duplicated type aliases.
Diffstat (limited to 'vernac/comDefinition.mli')
| -rw-r--r-- | vernac/comDefinition.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 2b846f17e0..e3417d0062 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,7 +17,7 @@ open Constrexpr val do_definition : ?hook:Declare.Hook.t -> name:Id.t - -> scope:Declare.locality + -> scope:Locality.locality -> poly:bool -> kind:Decls.definition_object_kind -> universe_decl_expr option @@ -30,7 +30,7 @@ val do_definition val do_definition_program : ?hook:Declare.Hook.t -> name:Id.t - -> scope:Declare.locality + -> scope:Locality.locality -> poly:bool -> kind:Decls.logical_kind -> universe_decl_expr option |