diff options
| author | Pierre-Marie Pédrot | 2016-10-05 18:18:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-05 18:18:22 +0200 |
| commit | 2dcd8f2e82366bb3b0f51a42426ccdfbb00281dc (patch) | |
| tree | 4e9a44599dec13e262538e70a6a60bcf3e5fa97e /tactics/equality.ml | |
| parent | 01a448be0133872a686e613ab1034b4cb97cd666 (diff) | |
| parent | 8114da3ba8a9b31ffe194e7f7f0239ecc2219b9c (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 444fac1708..7c819edadc 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -702,16 +702,16 @@ let replace_in_clause_maybe_by c1 c2 cl tac_opt = exception DiscrFound of (constructor * int) list * constructor * constructor -let injection_on_proofs = ref false +let keep_proof_equalities_for_injection = ref false let _ = declare_bool_option { optsync = true; optdepr = false; optname = "injection on prop arguments"; - optkey = ["Injection";"On";"Proofs"]; - optread = (fun () -> !injection_on_proofs) ; - optwrite = (fun b -> injection_on_proofs := b) } + optkey = ["Keep";"Proof";"Equalities"]; + optread = (fun () -> !keep_proof_equalities_for_injection) ; + optwrite = (fun b -> keep_proof_equalities_for_injection := b) } let find_positions env sigma t1 t2 = @@ -756,7 +756,7 @@ let find_positions env sigma t1 t2 = project env sorts posn t1_0 t2_0 in try - let sorts = if !injection_on_proofs then [InSet;InType;InProp] + let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp] else [InSet;InType] in Inr (findrec sorts [] t1 t2) @@ -1390,7 +1390,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inl _ -> tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.") | Inr [] -> - let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in + let suggestion = + if !keep_proof_equalities_for_injection then + "" else + " 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 [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> tclZEROMSG (str"Nothing to inject.") |