aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/declare.ml2
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 *)