diff options
| author | Hugo Herbelin | 2016-01-21 01:13:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-01-21 09:28:42 +0100 |
| commit | 4b075af747f65bcd73ff1c78417cf77edf6fbd76 (patch) | |
| tree | b6bebd4953c9285d30d83c24ee86e7ba447b0d35 /tactics | |
| parent | 3ad653b53ccbf2feb7807b4618dc9a455e9df877 (diff) | |
Fixing some problems with double induction.
Basically, the hypotheses were treated in an incorrect order, with a
hack for sometimes put them again in the right order, resulting in
failures and redundant hypotheses.
Status unclear, because this new version is incompatible except in
simple cases like a double induction on two "nat".
Fixing the bug incidentally simplify the code, relying on the
deprecation since 8.4 to allow not to ensure a compatibility (beyond
the simple situation of a double induction on simple datatypes).
See file induct.v for effect of changes.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elim.ml | 3 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 48 |
2 files changed, 6 insertions, 45 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 0954f3ddf2..99236e7707 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -145,8 +145,7 @@ let induction_trailer abs_i abs_j bargs = in let ids = List.rev (ids_of_named_context hyps) in (tclTHENLIST - [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids)); - simple_elimination (mkVar id)]) + [revert ids; simple_elimination (mkVar id)]) end } )) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 750ec8fb1e..061c05b9b2 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -239,52 +239,14 @@ let gl_make_case_nodep ind gl = (Sigma.to_evar_map sigma, r) let make_elim_branch_assumptions ba gl = - let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc = - match lb,lc with - | ([], _) -> - { ba = ba; - assums = assums} - | ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) -> - makerec (recarg::indarg::assums, - idrec::cargs, - idrec::recargs, - constargs, - idind::indargs) tl idtl - | ((false::tl), ((id,_,_ as constarg)::idtl)) -> - makerec (constarg::assums, - id::cargs, - id::constargs, - recargs, - indargs) tl idtl - | (_, _) -> anomaly (Pp.str "make_elim_branch_assumptions") - in - makerec ([],[],[],[],[]) ba.branchsign - (try List.firstn ba.nassums (pf_hyps gl) - with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions")) + let assums = + try List.rev (List.firstn ba.nassums (pf_hyps gl)) + with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in + { ba = ba; assums = assums } let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl -let make_case_branch_assumptions ba gl = - let rec makerec (assums,cargs,constargs,recargs) p_0 p_1 = - match p_0,p_1 with - | ([], _) -> - { ba = ba; - assums = assums} - | ((true::tl), ((idrec,_,_ as recarg)::idtl)) -> - makerec (recarg::assums, - idrec::cargs, - idrec::recargs, - constargs) tl idtl - | ((false::tl), ((id,_,_ as constarg)::idtl)) -> - makerec (constarg::assums, - id::cargs, - recargs, - id::constargs) tl idtl - | (_, _) -> anomaly (Pp.str "make_case_branch_assumptions") - in - makerec ([],[],[],[]) ba.branchsign - (try List.firstn ba.nassums (pf_hyps gl) - with Failure _ -> anomaly (Pp.str "make_case_branch_assumptions")) +let make_case_branch_assumptions = make_elim_branch_assumptions let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl |