diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-05-18 13:04:52 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-05-18 13:04:52 -0400 |
| commit | 076274d366f7dd4f09d99fa8f3962b6f78bf9252 (patch) | |
| tree | 75adc332d0ea1e7176ba2c9ac1c01fd64d33b9d4 | |
| parent | e1cf5ccd8df7080d7dd2aadf0305a9d3ba9c5d9d (diff) | |
Suggest Set Injection On Proofs in error message for injection.
| -rw-r--r-- | tactics/equality.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 15a774613..270f9bf6f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1280,7 +1280,8 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inl _ -> Proofview.tclZERO (Errors.UserError ("Inj",strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")) | Inr [] -> - Proofview.tclZERO (Errors.UserError ("Equality.inj",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 restrictions in the sort Prop.")) + let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in + Proofview.tclZERO (Errors.UserError ("Equality.inj",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 [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject.")) | Inr posns -> |