diff options
| -rw-r--r-- | tactics/equality.ml | 8 | ||||
| -rw-r--r-- | test-suite/success/Injection.v | 6 |
2 files changed, 10 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 92ebcb2724..1854b41205 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1319,13 +1319,13 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = tclZEROMSG (str "Failed to decompose the equality.") else Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) - (Proofview.tclBIND - (Proofview.Monad.List.map + (Tacticals.New.tclTHENFIRST + (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; Proofview.V82.tactic (refine pf)]) - (if l2r then List.rev injectors else injectors)) - (fun _ -> tac (List.length injectors))) + (if l2r then List.rev injectors else injectors))) + (tac (List.length injectors))) let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 25e464d677..8fd0394625 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -68,6 +68,12 @@ einjection (H O). instantiate (1:=O). Abort. +Goal (forall x y : nat, x = y -> S x = S y) -> True. +intros. +einjection (H O) as H0. +instantiate (y:=O). +Abort. + (* Test the injection intropattern *) Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b. |