diff options
| -rw-r--r-- | tactics/tactics.ml | 13 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 4 |
2 files changed, 5 insertions, 12 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6603c82cd2..ab0cd6fb3c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2771,18 +2771,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = let find_atomic_param_of_ind nparams indtyp = let argl = snd (decompose_app indtyp) in - let argv = Array.of_list argl in - let params = List.firstn nparams argl in - let indvars = ref Id.Set.empty in - for i = nparams to (Array.length argv)-1 do - match kind_of_term argv.(i) with - | Var id - when not (List.exists (occur_var (Global.env()) id) params) -> - indvars := Id.Set.add id !indvars - | _ -> () - done; - Id.Set.elements !indvars; - + List.map destVar (snd (List.chop nparams argl)) (* [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 f5848ffe0e..2aa07cde1b 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -393,6 +393,10 @@ intros * Heq H Heq'. destruct H. 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 *) + (* Check clearing of names *) Inductive eqnat (x : nat) : nat -> Prop := |