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/unification.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/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 7f5cac2d2..0f5a62bb5 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -68,7 +68,7 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> |