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 8b1d20e6de..b5e2880134 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -101,7 +101,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 [] 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.") |