diff options
| author | Hugo Herbelin | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-28 16:40:22 +0200 |
| commit | 7943b1fade775af48917d54878e65b80217be038 (patch) | |
| tree | 1ea76a0ca0fb5b9a1c1699842268324cae4c1488 /interp/constrintern.ml | |
| 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 '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 94924374a8..ea1802ccfa 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, (true,n)) + GPatVar (loc, Evar_kinds.SecondOrderPatVar n) | CEvar (loc, n, []) when pattern_mode -> - GPatVar (loc, (false,n)) + GPatVar (loc, Evar_kinds.FirstOrderPatVar n) (* end *) (* Parsing existential variables *) | CEvar (loc, n, l) -> |