From bf3b52f6a950490ad99b032cb0b41d32cff64824 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/constrextern.ml | 10 ++++++----
 interp/constrintern.ml |  4 ++--
 2 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4c29fc8097..5dd0783424 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -663,9 +663,11 @@ let rec extern inctx scopes vars r =
   | GEvar (n,l) ->
       extern_evar n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (b,n) ->
+  | GPatVar kind ->
       if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
-        if b then CPatVar n else CEvar (n,[])
+       (match kind with
+         | Evar_kinds.SecondOrderPatVar n -> CPatVar n
+         | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
 
   | GApp (f,args) ->
       (match f with
@@ -1037,13 +1039,13 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
-  | PMeta (Some n) -> GPatVar (false,n)
+  | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
   | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None),
 			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
       GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
-      GApp (CAst.make @@ GPatVar (true,n),
+      GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n),
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
       GProd (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 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) ->
-- 
cgit v1.2.3