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 /plugins/ltac | |
| parent | d83e95cce852c5471593a27d0fdca39a262c885f (diff) | |
[declare] [api] Removal of duplicated type aliases.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 67d09acfda..0bf97fefa6 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1900,7 +1900,7 @@ let declare_projection name instance_id r = in it_mkProd_or_LetIn ccl ctx in let types = Some (it_mkProd_or_LetIn typ ctx) in - let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in let _r : GlobRef.t = @@ -1968,7 +1968,7 @@ let add_morphism_as_parameter atts m n : unit = let env = Global.env () in let evd = Evd.from_env env in let poly = atts.polymorphic in - let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let evd, types = build_morphism_signature env evd m in let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in |