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.

8 files changed, 19 insertions, 30 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) ->
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 75dad2e91..470ad2a23 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Globnames
-open Misctypes
 
 (** The kinds of existential variable *)
 
@@ -17,8 +16,6 @@ open Misctypes
 
 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 *)
@@ -30,6 +27,6 @@ type t =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
-  | MatchingVar of matching_var_kind
+  | MatchingVar of bool * Id.t
   | VarInstance of Id.t
   | SubEvar of Constr.existential_key
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ba4a47a36..ced5a8b44 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 * Evar_kinds.matching_var_kind (** Used for patterns only *)
+  | GPatVar of Loc.t * (bool * patvar) (** 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 7fb539fb5..ebbfa195f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,7 +12,6 @@ open Nameops
 open Globnames
 open Misctypes
 open Glob_term
-open Evar_kinds
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
@@ -62,18 +61,14 @@ 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 (_, k1), GPatVar (_, k2) -> matching_var_kind_eq k1 k2
+| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
+  (b1 : bool) == b2 && Id.equal pat1 pat2
 | 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 b310da9a3..b16d04495 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 (Evar_kinds.SecondOrderPatVar id) -> Some id
+              Evar_kinds.MatchingVar (true,id) -> Some id
             | _ -> None)
           | _ -> None
          with
@@ -158,11 +158,10 @@ 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 (Evar_kinds.FirstOrderPatVar id) ->
-        PMeta (Some id)
+      | Evar_kinds.MatchingVar (b,id) ->
+        assert (not b); 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) ->
@@ -329,12 +328,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 (_,Evar_kinds.FirstOrderPatVar n) ->
+  | GPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
   | GRef (_,gr,_) ->
       PRef (canonical_gr gr)
   (* Hack to avoid rewriting a complete interpretation of patterns *)
-  | GApp (_, GPatVar (_,Evar_kinds.SecondOrderPatVar n), cl) ->
+  | GApp (_, GPatVar (_,(true,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 6c490045c..ae87cd8c0 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,kind) ->
+  | GPatVar (loc,(someta,n)) ->
     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 kind in
+    let k = Evar_kinds.MatchingVar (someta,n) 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 257c092d7..851554b83 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, Evar_kinds.FirstOrderPatVar (Id.of_string id))
+let mkGPatVar id = GPatVar(Loc.ghost, (false, Id.of_string id))
 let mkGRef r = GRef (Loc.ghost, Lazy.force r, None)
 let mkGAppRef r args = mkGApp (mkGRef r) args