diff options
| author | Matthieu Sozeau | 2014-08-25 21:46:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-25 21:55:34 +0200 |
| commit | 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e (patch) | |
| tree | f7860f13dc18938953ead65c63923aba117d890b /pretyping/tacred.ml | |
| parent | 12c803053572194c85e4c7b7f347175c7c335858 (diff) | |
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index f2a0b6fd18..a2791f7a20 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -930,10 +930,10 @@ let simpl env sigma c = strong whd_simpl env sigma c (* Reduction at specific subterms *) -let matches_head c t = +let matches_head env sigma c t = match kind_of_term t with - | App (f,_) -> ConstrMatching.matches c f - | Proj (p, _) -> ConstrMatching.matches c (mkConst p) + | App (f,_) -> ConstrMatching.matches env sigma c f + | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst p) | _ -> raise ConstrMatching.PatternMatchingFailure let e_contextually byhead (occs,c) f env sigma t = @@ -946,7 +946,8 @@ let e_contextually byhead (occs,c) f env sigma t = else try let subst = - if byhead then matches_head c t else ConstrMatching.matches c t in + if byhead then matches_head env sigma c t + else ConstrMatching.matches env sigma c t in let ok = if nowhere_except_in then Int.List.mem !pos locs else not (Int.List.mem !pos locs) in |