diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:40:22 +0200 |
| commit | 7943b1fade775af48917d54878e65b80217be038 (patch) | |
| tree | 1ea76a0ca0fb5b9a1c1699842268324cae4c1488 /tactics | |
| parent | 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (diff) | |
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hipattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 851554b83..257c092d7 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, (false, Id.of_string id)) +let mkGPatVar id = GPatVar(Loc.ghost, Evar_kinds.FirstOrderPatVar (Id.of_string id)) let mkGRef r = GRef (Loc.ghost, Lazy.force r, None) let mkGAppRef r args = mkGApp (mkGRef r) args |