diff options
| author | Pierre-Marie Pédrot | 2018-07-26 11:01:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 11:01:34 +0200 |
| commit | 1f083eb5d964ca8740f94ebdec1d69b85b85a6e1 (patch) | |
| tree | 917742ce74d4fcb44699a207a41c2c99a14d6b91 /pretyping | |
| parent | 6cd6f1edae2e2c7b2aaedd039b39caaf1d50aa9f (diff) | |
| parent | 190ff373ed3728ae816da674ceeae3ba8ffa1919 (diff) | |
Merge PR #7274: Avoiding introducing dependency on the indices of a term which has no matching clauses.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6a63fb02f8..ad33297f0a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -373,6 +373,11 @@ let ltac_interp_realnames lvar = function | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal) | _ as x -> x +let is_patvar pat = + match DAst.get pat with + | PatVar _ -> true + | _ -> false + let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in @@ -381,6 +386,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let typ = nf_evar !evdref j.uj_type in lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = + if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else try try_find_ind env !evdref typ realnames with Not_found -> unify_tomatch_with_patterns evdref env loc typ pats realnames in |