From 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 25 Aug 2014 21:46:26 +0200 Subject: 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. --- tactics/hipattern.ml4 | 3 +++ 1 file changed, 3 insertions(+) (limited to 'tactics/hipattern.ml4') 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 -- cgit v1.2.3