Using a more explicit algebraic type for evars of kind "MatchingVar".

A priori considered to be a good programming style.

8 files changed, 30 insertions, 19 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 59b8b4e5b9..bdbfd8c277 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -654,9 +654,11 @@ 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,(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,[])
+  | 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,[]))
 
   | GApp (loc,f,args) ->
       (match f with
@@ -1029,13 +1031,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,(false,n))
+  | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar 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,(true,n)),
+      GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar 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 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) ->
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 ced5a8b44f..ba4a47a365 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -38,7 +38,7 @@ type glob_constr =
       (** An identifier that cannot be regarded as "GRef".
           Bound variables are typically represented this way. *)
   | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list
-  | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
+  | GPatVar of Loc.t * Evar_kinds.matching_var_kind (** Used for patterns only *)
   | GApp of Loc.t * glob_constr * glob_constr list
   | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
   | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ebbfa195f0..7fb539fb5b 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,6 +12,7 @@ open Nameops
 open Globnames
 open Misctypes
 open Glob_term
+open Evar_kinds
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
@@ -61,14 +62,18 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
 | CastNative t1, CastNative t2 -> eq t1 t2
 | _ -> false
 
+let matching_var_kind_eq k1 k2 = match k1, k2 with
+| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
+| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2
+| _ -> false
+
 let rec glob_constr_eq c1 c2 = match c1, c2 with
 | GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2
 | GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
 | GEvar (_, id1, arg1), GEvar (_, id2, arg2) ->
   Id.equal id1 id2 &&
   List.equal instance_eq arg1 arg2
-| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
-  (b1 : bool) == b2 && Id.equal pat1 pat2
+| GPatVar (_, k1), GPatVar (_, k2) -> matching_var_kind_eq k1 k2
 | GApp (_, f1, arg1), GApp (_, f2, arg2) ->
   glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2
 | GLambda (_, na1, bk1, t1, c1), GLambda (_, na2, bk2, t2, c2) ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b16d044956..b310da9a37 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -145,7 +145,7 @@ let pattern_of_constr env sigma t =
           match kind_of_term f with
           | Evar (evk,args) ->
             (match snd (Evd.evar_source evk sigma) with
-              Evar_kinds.MatchingVar (true,id) -> Some id
+              Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
             | _ -> None)
           | _ -> None
          with
@@ -158,10 +158,11 @@ let pattern_of_constr env sigma t =
       pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
     | Evar (evk,ctxt) ->
       (match snd (Evd.evar_source evk sigma) with
-      | Evar_kinds.MatchingVar (b,id) ->
-        assert (not b); PMeta (Some id)
+      | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
+        PMeta (Some id)
       | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+      | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ -> 
 	 PMeta None)
     | Case (ci,p,a,br) ->
@@ -328,12 +329,12 @@ let rec pat_of_raw metas vars = function
   | GVar (_,id) ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
-  | GPatVar (_,(false,n)) ->
+  | GPatVar (_,Evar_kinds.FirstOrderPatVar n) ->
       metas := n::!metas; PMeta (Some n)
   | GRef (_,gr,_) ->
       PRef (canonical_gr gr)
   (* Hack to avoid rewriting a complete interpretation of patterns *)
-  | GApp (_, GPatVar (_,(true,n)), cl) ->
+  | GApp (_, GPatVar (_,Evar_kinds.SecondOrderPatVar n), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
   | GApp (_,c,cl) ->
       PApp (pat_of_raw metas vars c,
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ae87cd8c02..6c490045ca 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -596,13 +596,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon
 
-  | GPatVar (loc,(someta,n)) ->
+  | GPatVar (loc,kind) ->
     let env = ltac_interp_name_env k0 lvar env !evdref in
     let ty =
       match tycon with
       | Some ty -> ty
       | None -> new_type_evar env evdref loc in
-    let k = Evar_kinds.MatchingVar (someta,n) in
+    let k = Evar_kinds.MatchingVar kind in
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (loc, k, naming, None) ->
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 851554b832..257c092d72 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -261,7 +261,7 @@ let mkGProd id c1 c2 =
 let mkGArrow c1 c2 =
   GProd (Loc.ghost, Anonymous, Explicit, c1, c2)
 let mkGVar id = GVar (Loc.ghost, Id.of_string id)
-let mkGPatVar id = GPatVar(Loc.ghost, (false, Id.of_string id))
+let mkGPatVar id = GPatVar(Loc.ghost, Evar_kinds.FirstOrderPatVar (Id.of_string id))
 let mkGRef r = GRef (Loc.ghost, Lazy.force r, None)
 let mkGAppRef r args = mkGApp (mkGRef r) args