diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:14:09 +0200 |
| commit | 4f742e14441581ece247d33020055f15732f126b (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /tactics | |
| parent | 7943b1fade775af48917d54878e65b80217be038 (diff) | |
Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
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 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 |