diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 50 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 29 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 2 | ||||
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 4 |
5 files changed, 29 insertions, 57 deletions
@@ -216,6 +216,7 @@ Tactics matching the given pattern is used - non-dependent destruct/induction on an hypothesis with premisses in an inductive type with indices is fixed + - residual local definitions are now correctly removed. Program diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 56568c599..6e767d733 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2656,47 +2656,37 @@ let induct_discharge dests avoid' tac (avoid,ra) names = let atomize_param_of_ind (indref,nparams,_) hyp0 = Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in - let typ0 = reduce_to_quantified_ref indref tmptyp0 in + let typ0 = reduce_to_quantified_ref indref tmptyp0 in let prods, indtyp = decompose_prod typ0 in - let argl = snd (decompose_app indtyp) in + let ind,argl = decompose_app indtyp in let params = List.firstn nparams argl in (* le gl est important pour ne pas préévaluer *) - let rec atomize_one i avoid = - Proofview.Goal.nf_enter begin fun gl -> + let rec atomize_one i args = if not (Int.equal i nparams) then - let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in - (* If argl <> [], we expect typ0 not to be quantified, in order to - avoid bound parameters... then we call pf_reduce_to_atomic_ind *) - let reduce_to_atomic_ref = - Tacmach.New.pf_apply reduce_to_atomic_ref gl - in - let indtyp = reduce_to_atomic_ref indref tmptyp0 in - let argl = snd (decompose_app indtyp) in let c = List.nth argl (i-1) in - let env = Proofview.Goal.env gl in match kind_of_term c with - | Var id when not (List.exists (occur_var env id) avoid) -> - atomize_one (i-1) ((mkVar id)::avoid) - | Var id -> - let x = new_fresh_id [] id gl in - Tacticals.New.tclTHEN - (letin_tac None (Name x) (mkVar id) None allHypsAndConcl) - (atomize_one (i-1) ((mkVar x)::avoid)) + | Var id when not (List.exists (occur_var env id) args) -> + atomize_one (i-1) (mkVar id :: args) | _ -> - let type_of = Tacmach.New.pf_type_of gl in - let id = id_of_name_using_hdchar (Global.env()) (type_of c) - Anonymous in + let id = match kind_of_term c with + | Var id -> id + | _ -> + let type_of = Tacmach.New.pf_type_of gl in + id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let x = new_fresh_id [] id gl in - Tacticals.New.tclTHEN - (letin_tac None (Name x) c None allHypsAndConcl) - (atomize_one (i-1) ((mkVar x)::avoid)) + Tacticals.New.tclTHENLIST [ + (letin_tac None (Name x) c None allHypsAndConcl); + (atomize_one (i-1) (mkVar x :: args)) + ] else - Proofview.tclUNIT () - end + Proofview.V82.tactic + (change_in_hyp None (fun _ sigma -> sigma, applist (ind,params@args)) + (hyp0,InHypTypeOnly)) in - atomize_one (List.length argl) params + atomize_one (List.length argl) [] end let find_atomic_param_of_ind nparams indtyp = @@ -3721,7 +3711,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyp Proofview.Goal.nf_enter begin fun gl -> let sigma, elim_info = find_induction_type isrec elim hyp0 gl in Tacticals.New.tclTHENLIST - [Proofview.Unsafe.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0); + [Proofview.Unsafe.tclEVARS sigma; atomize_param_of_ind elim_info hyp0; (induction_from_context isrec with_evars elim_info hyp0 fixedvars names inhyps)] end diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 7c1e09d6d..cca54bf1c 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -289,41 +289,22 @@ intros. destruct (h 0). Abort. -(* These ones are not satisfactory at the current time +(* Check absence of useless local definitions *) Section S2. Variable H : 1=1. Goal 0=1. destruct H. -(* Should expand the n... *) - n := 1 : nat - H : n = n - ============================ - 0 = n +Fail clear n. (* Check that there is no n as it was in Coq <= 8.4 *) Abort. End S2. -(* Should expand the n... *) -Goal 1=1->0=1. -intro H. -destruct H. -(* - n := 1 : nat - ============================ - 0 = n -*) - -(* Should expand the x0... *) Goal forall x:nat, x=x->x=1. intros x H. destruct H. -(* - x : nat - x0 := x : nat - ============================ - x0=1 -*) -*) +Fail clear n. (* Check that there is no n as it was in Coq <= 8.4 *) +Fail clear H. (* Check that H has been removed *) +Abort. (* Check support for induction arguments which do not expose an inductive type rightaway *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index a7ed3c7f7..a7a1fd97c 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -483,7 +483,7 @@ Proof. destruct (eq_id_comm_l f Hfsymf (f a)). destruct (eq_id_comm_l f Hfsymf a). unfold Hfsymf. - destruct (Hf a). simpl. unfold a0; clear a0. + destruct (Hf a). simpl. rewrite eq_trans_refl_l. reflexivity. Defined. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 939fbe408..1cef233d6 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -374,13 +374,13 @@ Proof. symmetry. apply UIP_refl. } transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x)))). - - destruct z. unfold e. destruct (UIP _ _). reflexivity. + - destruct z. destruct (UIP _ _). reflexivity. - change (match eq_refl x as y' in _ = x' return y' = y' -> Prop with | eq_refl => fun z => z = (eq_refl (eq_refl x)) end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x))))). - destruct z. unfold e. destruct (UIP _ _). reflexivity. + destruct z. destruct (UIP _ _). reflexivity. Qed. Theorem UIP_shift : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = x). Proof (fun U UIP_refl x => |