diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 389e0e722..ed8ecfac4 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -99,7 +99,7 @@ let declare_assumption env isevars idl is_coe k bl c nl = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None in let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl + List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") |