aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index d7b03a84f1..eafdc4cb46 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -818,7 +818,7 @@ let fresh_constructor_instance ?loc env evd c =
with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
- with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
+ with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
let is_sort_variable evd s = UState.is_sort_variable evd.universes s