From 7943b1fade775af48917d54878e65b80217be038 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Apr 2017 16:15:10 +0200
Subject: Using a more explicit algebraic type for evars of kind "MatchingVar".

A priori considered to be a good programming style.
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrintern.ml')

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) ->
-- 
cgit v1.2.3