diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:35:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:46:38 +0200 |
| commit | fc579fdc83b751a44a18d2373e86ab38806e7306 (patch) | |
| tree | b325c2ff65c505ad62ac7b3fce6bce28633a60f0 /proofs/pfedit.ml | |
| parent | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff) | |
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b86582def..86c2b7a57 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -131,7 +131,7 @@ let solve ?with_end_tac gi info_lvl tac pr = | CList.IndexOutOfRange -> match gi with | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in - CErrors.user_err "" msg + CErrors.user_err msg | _ -> assert false let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) @@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk = when Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> - let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in + let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in (try let c = Evarutil.nf_evars_universes sigma evi.evar_concl in if Evarutil.has_undefined_evars sigma c then raise Exit; |