diff options
| author | Maxime Dénès | 2017-04-28 22:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-28 22:14:09 +0200 |
| commit | 4f742e14441581ece247d33020055f15732f126b (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /interp/constrintern.ml | |
| 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 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ea1802ccfa..94924374a8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1748,9 +1748,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GHole (loc, k, naming, solve) (* Parsing pattern variables *) | CPatVar (loc, n) when pattern_mode -> - GPatVar (loc, Evar_kinds.SecondOrderPatVar n) + GPatVar (loc, (true,n)) | CEvar (loc, n, []) when pattern_mode -> - GPatVar (loc, Evar_kinds.FirstOrderPatVar n) + GPatVar (loc, (false,n)) (* end *) (* Parsing existential variables *) | CEvar (loc, n, l) -> |