From 13458380eaef14078bb5805db3d8027bc76adeba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 12 May 2017 19:33:52 +0200
Subject: Adapting to PR #590 (a more explicit algebraic type for evars of kind
 MatchingVar).

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index f98a251..18c1e3d 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -1351,7 +1351,7 @@ let interp_search_notation ?loc tag okey =
     err (pr_ntn ntn ++ str " is an n-ary notation");
   let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
   let rec sub () = function
-  | NVar x when List.mem_assoc x nvars -> CAst.make ?loc @@ GPatVar (false, x)
+  | NVar x when List.mem_assoc x nvars -> CAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
   | c ->
     glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
-- 
cgit v1.2.3