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