aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/subtac/subtac_utils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 49bdfdae19..b684dd320b 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -195,7 +195,7 @@ let non_instanciated_map env evd evm =
QuestionMark _ -> Evd.add evm key evi
| _ ->
debug 2 (str " and is an implicit");
- Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k)
+ Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
Evd.empty (Evarutil.non_instantiated evm)
let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition