diff options
| author | Hugo Herbelin | 2014-11-12 09:33:16 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-13 21:40:37 +0100 |
| commit | 014e5ac92a2338f8820be63618c5b0dd631744de (patch) | |
| tree | 326438f8a147fe5de2eefd85325a0f3d7e1ec0db | |
| parent | 12b9f0268182faf9eea4bb3d8b31242316454025 (diff) | |
Removing yet another source of remaining local definitions.
| -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 := |