diff options
| author | Hugo Herbelin | 2014-10-31 17:29:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-31 18:49:05 +0100 |
| commit | 1177da32723fd46a82b66ca7ffe4d13d93480da6 (patch) | |
| tree | 8d66f89beafc497e529bdcefd2372bdd23d90cba /parsing | |
| parent | 801cd9cb0559d3b78216da166044bd02348ed9af (diff) | |
Reorganization of the test for generic selection of occurrences in
clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index fb09a31085..a57720755a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -174,23 +174,9 @@ let map_int_or_var f = function let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } -let has_no_specified_occs cl = - let forall ((occs, _), _) = match occs with - | AllOccurrences -> true - | _ -> false - in - let hyps = match cl.onhyps with - | None -> true - | Some hyps -> List.for_all forall hyps in - let concl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true - | _ -> false - in - hyps && concl - let merge_occurrences loc cl = function | None -> - if has_no_specified_occs cl then (None, cl) + if Locusops.clause_with_generic_occurrences cl then (None, cl) else user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.") | Some (occs, p) -> @@ -203,7 +189,7 @@ let merge_occurrences loc cl = function | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } -> { cl with onhyps = Some [(occs, id), l] } | _ -> - if has_no_specified_occs cl then + if Locusops.clause_with_generic_occurrences cl then user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") else user_err_loc (loc,"",str "Cannot use clause \"at\" twice.") |