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.

2 files changed, 7 insertions, 9 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bdbfd8c27..59b8b4e5b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -654,11 +654,9 @@ let rec extern inctx scopes vars r =
   | GEvar (loc,n,l) ->
       extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (loc,kind) ->
-       if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
-       (match kind with
-         | Evar_kinds.SecondOrderPatVar n -> CPatVar (loc,n)
-         | Evar_kinds.FirstOrderPatVar n -> CEvar (loc,n,[]))
+  | GPatVar (loc,(b,n)) ->
+      if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
+        if b then CPatVar (loc,n) else CEvar (loc,n,[])
 
   | GApp (loc,f,args) ->
       (match f with
@@ -1031,13 +1029,13 @@ let rec glob_of_pat env sigma = function
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar (loc,id)
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
-  | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar n)
+  | PMeta (Some n) -> GPatVar (loc,(false,n))
   | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
 			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
       GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
-      GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar n),
+      GApp (loc,GPatVar (loc,(true,n)),
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
       GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ea1802ccf..94924374a 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) ->