diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-30 15:52:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-31 18:49:05 +0100 |
| commit | cc27d50bf7423fe1df00330eddcd81d18b55fd0f (patch) | |
| tree | d8e031956cc5250c9aca3642be8183ea675f9c03 /pretyping/locusops.mli | |
| parent | 19c75f706780ea6c5bc4e22d1fbaa8ed2150ae3d (diff) | |
Enlarge the cases where the like first selection is used in destruct.
This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
Diffstat (limited to 'pretyping/locusops.mli')
| -rw-r--r-- | pretyping/locusops.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index f6d27a185..c1bf2d9ea 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -38,7 +38,8 @@ val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause (** Miscellaneous functions *) -val occurrences_of_hyp : Id.t -> clause or_like_first -> - (occurrences * hyp_location_flag) or_like_first -val occurrences_of_goal : clause or_like_first -> occurrences or_like_first -val in_every_hyp : clause or_like_first -> bool +val occurrences_of_hyp : Id.t -> clause -> (occurrences * hyp_location_flag) +val occurrences_of_goal : clause -> occurrences +val in_every_hyp : clause -> bool + +val has_selected_occurrences : clause -> bool |