diff options
| author | Hugo Herbelin | 2014-11-06 11:29:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-06 17:00:30 +0100 |
| commit | ca609f7ea0653a282a81e5d4f9392b1c05a03d8f (patch) | |
| tree | 36a3cf7a8032c5c4040732ae7ea4ef2d71250c4b | |
| parent | 34de09e9a072a937f1510d69cad1204a53e007aa (diff) | |
Restoring clear_flag (thanks a lot to jonikelee to notice it).
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 8 |
2 files changed, 11 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 01996c4e10..8e95f742e4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3885,8 +3885,7 @@ let check_enough_applied env sigma elim = (* Last argument is supposed to be the induction argument *) check_expected_type env sigma elimc elimt -let pose_induction_arg_then clear_flag isrec with_evars - (is_arg_pure_hyp,from_prefix) elim +let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -3956,6 +3955,7 @@ let induction_gen clear_flag isrec with_evars elim let is_arg_pure_hyp = isVar c && not (mem_named_context (destVar c) (Global.named_context())) && lbind == NoBindings && not with_evars && Option.is_empty eqname + && clear_flag == None && has_generic_occurrences_but_goal cls (destVar c) env ccl in let enough_applied = check_enough_applied env sigma elim t in if is_arg_pure_hyp && enough_applied then @@ -3978,7 +3978,7 @@ let induction_gen clear_flag isrec with_evars elim new_fresh_id [] x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in pose_induction_arg_then - clear_flag isrec with_evars info_arg elim id arg t inhyps cls + isrec with_evars info_arg elim id arg t inhyps cls (induction_with_atomization_of_ind_arg isrec with_evars elim names id inhyps) end diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index c74bda2a9b..f5848ffe0e 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -377,6 +377,14 @@ intros. Fail destruct H. Abort. +(* Check keep option (bug #3791) *) + +Goal forall b:bool, True. +intro b. +destruct !b. +clear b. (* b has to be here *) +Abort. + (* Check clearing of names *) Inductive IND2 : nat -> Prop := CONSTR2 : forall y, y = y -> IND2 y. |