diff options
| -rw-r--r-- | tactics/equality.ml | 20 | ||||
| -rw-r--r-- | tactics/inv.ml | 10 | ||||
| -rw-r--r-- | test-suite/success/Inversion.v | 22 |
3 files changed, 36 insertions, 16 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index f84a0e303..6adfa3aaf 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -920,7 +920,7 @@ let simplify_args env sigma t = | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2]) | _ -> t -let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns = +let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac = let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (e,None,t) env in let injectors = @@ -938,9 +938,11 @@ let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns = posns in if injectors = [] then errorlabstrm "Equality.inj" (str "Failed to decompose the equality."); - tclMAP - (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf]) - injectors + tclTHEN + (tclMAP + (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf]) + injectors) + (tac (List.length injectors)) exception Not_dep_pair @@ -993,9 +995,8 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = (* not a dep eq or no decidable type found *) ) else (raise Not_dep_pair) ) with _ -> - tclTHEN - (inject_at_positions env sigma u eq_clause posns) - (intros_pattern no_move ipats) + inject_at_positions env sigma u eq_clause posns + (fun _ -> intros_pattern no_move ipats) let inj ipats with_evars = onEquality with_evars (injEq ipats) @@ -1016,10 +1017,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls = | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac 0 gls | Inr posns -> - tclTHEN - (inject_at_positions env sigma u clause (List.rev posns)) - (ntac (List.length posns)) - gls + inject_at_positions env sigma u clause (List.rev posns) ntac gls let dEqThen with_evars ntac = function | None -> onNegatedEquality with_evars (decompEqThen ntac) diff --git a/tactics/inv.ml b/tactics/inv.ml index 0080f079b..2a11d6520 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -320,11 +320,11 @@ let projectAndApply thin id eqname names depids gls = tclTHENSEQ [(if names <> [] then clear [id] else tclIDTAC); (tclMAP_i neqns (fun idopt -> - tclTHEN + tclTRY (tclTHEN (intro_move idopt no_move) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) - (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false))))) + (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false)))))) names); (if names = [] then clear [id] else tclIDTAC)] in @@ -406,7 +406,7 @@ let rewrite_equations othin neqns names ba gl = let rewrite_eqns = let first_eq = ref no_move in match othin with - | Some thin -> fun gl -> + | Some thin -> tclTHENSEQ [onHyps (compose List.rev (nLastDecls neqns)) bring_hyps; onHyps (nLastDecls neqns) (compose clear ids_of_named_context); @@ -420,11 +420,11 @@ let rewrite_equations othin neqns names ba gl = tclMAP (fun (id,_,_) gl -> intro_move None (if thin then no_move else !first_eq) gl) nodepids; - tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] gl + tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] | None -> tclIDTAC in (tclTHENSEQ - [(fun gl -> tclDO neqns intro gl); + [tclDO neqns intro; bring_hyps nodepids; clear (ids_of_named_context nodepids); rewrite_eqns]) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 71e53191b..e8a68c11d 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -107,3 +107,25 @@ Goal forall o, foo2 o -> 0 = 1. intros. eapply trans_eq. inversion H. + +(* Check that the part of "injection" that is called by "inversion" + does the same number of intros as the number of equations + introduced, even in presence of dependent equalities that + "injection" renounces to split *) + +Fixpoint prodn (n : nat) := + match n with + | O => unit + | (S m) => prod (prodn m) nat + end. + +Inductive U : forall n : nat, prodn n -> bool -> Prop := +| U_intro : U 0 tt true. + +Lemma foo3 : forall n (t : prodn n), U n t true -> False. +Proof. +(* used to fail because dEqThen thought there were 2 new equations but + inject_at_positions actually introduced only one; leading then to + an inconsistent state that disturbed "inversion" *) +intros. inversion H. +Abort. |