diff options
| author | Pierre-Marie Pédrot | 2019-12-18 16:56:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-18 16:56:08 +0100 |
| commit | 333b2f369c9a0ab61597cc9174a77632d263f386 (patch) | |
| tree | 2e2db1d45b26c1a758346959a83cd6cd84c36e6a /tactics | |
| parent | dfdfa9eeedebb0aec2cd72be9c1eee27ca9b2fab (diff) | |
| parent | 3c24d4f6398cc80fd070c4e6dcac99670c8c1bba (diff) | |
Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
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 fb06bb8a4f..da4de3df77 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -56,7 +56,7 @@ let declare_universe_context ~poly ctx = let nas = name_instance (Univ.UContext.instance uctx) in Global.push_section_context (nas, uctx) else - Global.push_context_set false ctx + Global.push_context_set ~strict:true ctx (** Declaration of constants and parameters *) |