diff options
| author | Hugo Herbelin | 2017-05-12 19:33:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 02:08:42 +0200 |
| commit | 13458380eaef14078bb5805db3d8027bc76adeba (patch) | |
| tree | 2fa831362345e31cadc961a80e4697d3f35b2cb8 | |
| parent | c05bfbee9a753b8867bc6ea5847cb7dd696a0cbd (diff) | |
Adapting to PR #590 (a more explicit algebraic type for evars of kind MatchingVar).
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 |