From 4f742e14441581ece247d33020055f15732f126b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:14:09 +0200
Subject: 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.
---
 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 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) ->
-- 
cgit v1.2.3