diff options
| author | Pierre-Marie Pédrot | 2019-06-25 20:57:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-08 20:47:26 +0200 |
| commit | d929838be77e30db04cd91201542bb52ed3ff7fd (patch) | |
| tree | 81a49bd4863424b841963f46025409396756d0bf /tactics | |
| parent | 75de485c233dd7bbb6301b49e6702eee205977fb (diff) | |
Similar purity invariants in the kernel.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 7ad86baa8d..b8ba62a5e5 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -289,7 +289,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind | None -> Cmap.empty | Some r -> Cmap.singleton kn r in - let eff = { Evd.seff_private = eff; Evd.seff_roles; } in + let eff = { Evd.seff_private = eff.Entries.seff_wrap; Evd.seff_roles; } in kn, eff (** Declaration of section variables and local definitions *) |