diff options
| author | Cyril Cohen | 2020-08-10 19:54:48 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-08-10 19:54:48 +0200 |
| commit | d5a8bdc8f67b691dd39a27a9fe07a026d998fda3 (patch) | |
| tree | d7c9a94c9fa3edb09c11fd1705654796b6ddda59 /tactics | |
| parent | ef08abec26c2f0017d1136870f8f99144e579538 (diff) | |
| parent | 0aa3f871051c737192f9a19b79957b32b6ecafea (diff) | |
Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)
Reviewed-by: CohenCyril
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 7 | ||||
| -rw-r--r-- | tactics/equality.mli | 1 |
2 files changed, 7 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index a2325b69cc..1689b0d3ad 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1416,6 +1416,11 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) +exception NothingToInject +let () = CErrors.register_handler (function + | NothingToInject -> Some (Pp.str "Nothing to inject.") + | _ -> None) + let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in let env = eq_clause.env in @@ -1429,7 +1434,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) | Inr [([],_,_)] -> - tclZEROMSG (str"Nothing to inject.") + Proofview.tclZERO NothingToInject | Inr posns -> inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) diff --git a/tactics/equality.mli b/tactics/equality.mli index e252eeab28..fdcbbc0e3c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -91,6 +91,7 @@ val discr_tac : evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic (* Below, if flag is [None], it takes the value from the dynamic value of the option *) +exception NothingToInject val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : inj_flags option -> intro_patterns option -> evars_flag -> |