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 /tactics/tacticMatching.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 'tactics/tacticMatching.ml')
| -rw-r--r-- | tactics/tacticMatching.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml index 0f48db6766..fa1b7f1586 100644 --- a/tactics/tacticMatching.ml +++ b/tactics/tacticMatching.ml @@ -228,7 +228,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Term p -> begin try - put_subst (ConstrMatching.extended_matches p term) <*> + put_subst (ConstrMatching.extended_matches E.env E.sigma p term) <*> return lhs with ConstrMatching.PatternMatchingFailure -> fail end @@ -247,7 +247,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (ConstrMatching.match_subterm_gen with_app_context p term) matching_error + map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) matching_error (** [rule_match_term term rule] matches the term [term] with the |