diff options
| author | Hugo Herbelin | 2014-11-02 19:55:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-02 19:57:31 +0100 |
| commit | 2c26c287cc36dcbecb4b41ca3a7a3f58bff07ac2 (patch) | |
| tree | 8bf1e2c5f495cdabfd38474a3fd5e92d06c987a2 /tactics | |
| parent | ab2afa67a5b4a8254add3294f52cabaa6c7e80a0 (diff) | |
Fixing 1177da327 (reorganization of the test for generic selection of
occurrences: some uniformisation was not appropriate for "change").
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4d8c97870d..23ec74db0f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3877,7 +3877,7 @@ let pose_induction_arg clear_flag isrec with_evars info_arg elim end let has_generic_occurrences_but_goal cls id env ccl = - clause_with_generic_occurrences cls && + clause_with_generic_context_selection cls && (* TODO: whd_evar of goal *) (cls.concl_occs != NoOccurrences || not (occur_var env id ccl)) |