diff options
| author | Emilio Jesus Gallego Arias | 2019-12-05 23:15:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-05 23:15:19 +0100 |
| commit | a78165d9fb333f2c50ab5ae52c32507429859c89 (patch) | |
| tree | 451872d26bdb93109227e90e0b853dddd54986f4 /interp/notation_ops.ml | |
| parent | 24936224d5170ba76162ff28eb091be10eace684 (diff) | |
| parent | f437655f3afbfd89e7abba7d9d53b49a2334b8ae (diff) | |
Merge PR #11172: Interleave removal of coercions and search for notations
Ack-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ff2498386d..265ca58ed9 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1225,7 +1225,7 @@ let rec match_ inner u alp metas sigma a1 a2 = bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)] else match_names metas (alp,sigma) (Name id') na in - match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 + match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ |