diff options
| -rw-r--r-- | tactics/tactics.ml | 35 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 1 | ||||
| -rw-r--r-- | test-suite/success/induct.v | 11 |
3 files changed, 38 insertions, 9 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ab0cd6fb3c..34fd8a8beb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2743,35 +2743,52 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = let hd,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 params args = + let rec atomize_one i args avoid = if Int.equal i nparams then - let t = applist (hd, params @ List.map mkVar args) in + let t = applist (hd, params@args) in Proofview.V82.tactic (change_in_hyp None (fun _ sigma -> sigma, t) (hyp0,InHypTypeOnly)) else let c = List.nth argl (i-1) in match kind_of_term c with - | Var id when not (List.mem id args) && + | Var id when not (List.exists (occur_var env id) args) && not (List.exists (occur_var env id) params) -> - (* We know that the name can be cleared after destruction *) - atomize_one (i-1) params (id::args) + (* Based on the knowledge given by the user, all + constraints on the variable are generalizable in the + current environment so that it is clearable after destruction *) + atomize_one (i-1) (c::args) (id::avoid) | _ -> + if List.exists (dependent c) params || + List.exists (dependent c) args + then + (* This is a case where the argument is constrained in a + way which would require some kind of inversion; we + follow the (old) discipline of not generalizing over + this term, since we don't try to invert the + constraint anyway. *) + atomize_one (i-1) (c::args) avoid + else + (* We reason blindly on the term and do as if it were + generalizable, ignoring the constraints coming from + its structure *) 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 = fresh_id_in_env args id env in + let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) - (atomize_one (i-1) (List.map (replace_term c (mkVar x)) params) (x::args)) + (atomize_one (i-1) (mkVar x::args) (x::avoid)) in - atomize_one (List.length argl) params [] + atomize_one (List.length argl) [] [] end let find_atomic_param_of_ind nparams indtyp = let argl = snd (decompose_app indtyp) in - List.map destVar (snd (List.chop nparams argl)) + let params,args = List.chop nparams argl in + let test c = isVar c && not (List.exists (dependent c) params) in + List.map destVar (List.filter test args) (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 2aa07cde1b..56cdf18e68 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -396,6 +396,7 @@ Abort. Goal 2=1 -> 1=0. intro H. destruct H. Fail (match goal with n:nat |- _ => unfold n end). (* Check that no let-in remains *) +Abort. (* Check clearing of names *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 0d0466cb58..3715f65f6c 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -140,3 +140,14 @@ intros x H1 H. induction H. change True in IHrepr'. Abort. + +(* In this case, generalization was done in 8.4 and we preserve it; this + is arbitrary choice *) + +Inductive repr'' : nat -> nat -> Prop := reprc'' x z : repr'' x z -> repr'' x z. + +Goal forall x, 0 = x -> repr'' x x -> True. +intros x H1 H. +induction H. +change (0 = z -> True) in IHrepr''. +Abort. |