From 1c7756adb95a70f8d382be062cc2d68bcf37e5a9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 29 Apr 2014 23:20:42 -0400 Subject: Injection: do not fail when arguments have sort Prop. This historic limitation of the injection tactic does not seem to have any precise justification. In fact, the only equalities that are not projectable is when the arguments of the constructor have sort Set or Type and the inductive type is in Prop (due to the restriction on pattern matching). The command "Unset Injection On Proofs" restores the old behavior. --- tactics/equality.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 89c6a091a..7b02443ca 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -610,6 +610,18 @@ let replace_in_clause_maybe_by c2 c1 cl tac_opt = exception DiscrFound of (constructor * int) list * constructor * constructor +let injection_on_proofs = ref true + +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) } + + let find_positions env sigma t1 t2 = let rec findrec sorts posn t1 t2 = let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in @@ -648,8 +660,10 @@ let find_positions env sigma t1 t2 = then [(List.rev posn,t1_0,t2_0)] else [] in try - (* Rem: to allow injection on proofs objects, just add InProp *) - Inr (findrec [InSet;InType] [] t1 t2) + let sorts = if !injection_on_proofs then [InSet;InType;InProp] + else [InSet;InType] + in + Inr (findrec sorts [] t1 t2) with DiscrFound (path,c1,c2) -> Inl (path,c1,c2) -- cgit v1.2.3