diff options
| author | Hugo Herbelin | 2014-08-03 19:18:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:22 +0200 |
| commit | 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae (patch) | |
| tree | 75d664dd62bb332cd3e8203c39e748102e0b2a57 /plugins/decl_mode/decl_proof_instr.ml | |
| parent | 8b8f8efe356a190ed2ae70b42688ef9170ef13b2 (diff) | |
Experimentally adding an option for automatically erasing an
hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).
Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.ml')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 4218286b0f..f780d1bb50 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -721,7 +721,7 @@ let rec consider_match may_intro introduced available expected gls = try conjunction_arity id gls with Not_found -> error "Matching hypothesis not found." in tclTHENLIST - [Proofview.V82.of_tactic (general_case_analysis false (mkVar id,NoBindings)); + [Proofview.V82.of_tactic (simplest_case (mkVar id)); intron_then nhyps [] (fun l -> consider_match may_intro introduced (List.rev_append l rest_ids) expected)] gls) @@ -1313,7 +1313,7 @@ let end_tac et2 gls = tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)] | ET_Case_analysis,EK_nodep -> tclTHEN - (Proofview.V82.of_tactic (general_case_analysis false (pi.per_casee,NoBindings))) + (Proofview.V82.of_tactic (simplest_case pi.per_casee)) (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST |