aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hipattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hipattern.ml')
-rw-r--r--tactics/hipattern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fd5eabe64..30fa7c804 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -260,7 +260,7 @@ let mkGProd id c1 c2 = CAst.make @@
let mkGArrow c1 c2 = CAst.make @@
GProd (Anonymous, Explicit, c1, c2)
let mkGVar id = CAst.make @@ GVar (Id.of_string id)
-let mkGPatVar id = CAst.make @@ GPatVar((false, Id.of_string id))
+let mkGPatVar id = CAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id))
let mkGRef r = CAst.make @@ GRef (Lazy.force r, None)
let mkGAppRef r args = mkGApp (mkGRef r) args