diff options
| author | Maxime Dénès | 2017-06-05 22:33:41 +0200 |
|---|---|---|
| committer | GitHub | 2017-06-05 22:33:41 +0200 |
| commit | 329fa19cc1d35162ce7c8ef82e3bf36aec058b26 (patch) | |
| tree | 2fa831362345e31cadc961a80e4697d3f35b2cb8 /mathcomp | |
| parent | c05bfbee9a753b8867bc6ea5847cb7dd696a0cbd (diff) | |
| parent | 13458380eaef14078bb5805db3d8027bc76adeba (diff) | |
Merge pull request #123 from herbelin/trunk+pr590-patvar
Adapting to PR #590 (a more explicit algebraic type for evars of kind…
Diffstat (limited to 'mathcomp')
| -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 |