aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 7d0584a00..17409595a 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -137,7 +137,7 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
let isGHole c = match DAst.get c with GHole _ -> true | _ -> false
let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
let mkCLambda ?loc name ty t = CAst.make ?loc @@
- CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t)
+ CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t)
let mkCLetIn ?loc name bo t = CAst.make ?loc @@
CLetIn ((Loc.tag ?loc name), bo, None, t)
let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)