diff options
| author | Hugo Herbelin | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 02:04:10 +0200 |
| commit | bf3b52f6a950490ad99b032cb0b41d32cff64824 (patch) | |
| tree | f880e1ce1989cd67c06c8a29284f35fc123bec09 /interp/constrintern.ml | |
| parent | 5dd98189c6554733fe4e22401e1637330cc8a30a (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 d4d8299701..4034f145ac 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1751,10 +1751,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* Parsing pattern variables *) | CPatVar n when pattern_mode -> CAst.make ?loc @@ - GPatVar (true,n) + GPatVar (Evar_kinds.SecondOrderPatVar n) | CEvar (n, []) when pattern_mode -> CAst.make ?loc @@ - GPatVar (false,n) + GPatVar (Evar_kinds.FirstOrderPatVar n) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> |