diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-25 21:46:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-25 21:55:34 +0200 |
| commit | 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e (patch) | |
| tree | f7860f13dc18938953ead65c63923aba117d890b /tactics/hipattern.ml4 | |
| 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/hipattern.ml4')
| -rw-r--r-- | tactics/hipattern.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index e171c2147..84fcd6dee 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -245,6 +245,9 @@ let coq_refl_jm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ] open Globnames +let is_matching x y = is_matching (Global.env ()) Evd.empty x y +let matches x y = matches (Global.env ()) Evd.empty x y + let match_with_equation t = if not (isApp t) then raise NoEquationFound; let (hdapp,args) = destApp t in |