From bf3b52f6a950490ad99b032cb0b41d32cff64824 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 28 Apr 2017 16:15:10 +0200 Subject: Using a more explicit algebraic type for evars of kind "MatchingVar". A priori considered to be a good programming style. --- tactics/hipattern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/hipattern.ml') 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 -- cgit v1.2.3