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.
---
 intf/evar_kinds.mli | 5 ++++-
 intf/glob_term.mli  | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 470ad2a23b..75dad2e918 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Globnames
+open Misctypes
 
 (** The kinds of existential variable *)
 
@@ -16,6 +17,8 @@ open Globnames
 
 type obligation_definition_status = Define of bool | Expand
 
+type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
+
 type t =
   | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
@@ -27,6 +30,6 @@ type t =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
-  | MatchingVar of bool * Id.t
+  | MatchingVar of matching_var_kind
   | VarInstance of Id.t
   | SubEvar of Constr.existential_key
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 33c71884a2..5da20c9d1c 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -39,7 +39,7 @@ type glob_constr_r =
       (** An identifier that cannot be regarded as "GRef".
           Bound variables are typically represented this way. *)
   | GEvar   of existential_name * (Id.t * glob_constr) list
-  | GPatVar of bool * patvar (** Used for patterns only *)
+  | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
   | GApp    of glob_constr * glob_constr list
   | GLambda of Name.t * binding_kind *  glob_constr * glob_constr
   | GProd   of Name.t * binding_kind * glob_constr * glob_constr
-- 
cgit v1.2.3