Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + a flag suspectingly renamed in a clearer way

3 files changed, 15 insertions, 9 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6fb1b6089..e53d19b59 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. *)
 
@@ -59,6 +60,11 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
   | CastNative t1, CastNative t2 -> eq t1 t2
   | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> 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
+| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false
+
 let tomatch_tuple_eq f (c1, p1) (c2, p2) =
   let eqp (_, (i1, na1)) (_, (i2, na2)) =
     eq_ind i1 i2 && List.equal Name.equal na1 na2
@@ -97,8 +103,7 @@ let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with
   | GVar id1, GVar id2 -> Id.equal id1 id2
   | GEvar (id1, arg1), GEvar (id2, arg2) ->
     Id.equal id1 id2 && List.equal (instance_eq f) 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) ->
     f f1 f2 && List.equal f arg1 arg2
   | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 0818a5525..71dbc39f3 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -143,7 +143,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
@@ -156,13 +156,14 @@ 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 as ev) ->
       (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 | Evar_kinds.VarInstance _ ->
         (* These are the two evar kinds used for existing goals *)
         (* see Proofview.mark_in_evm *)
          if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
          else 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 +330,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> 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 ({ CAst.v = GPatVar (true,n) }, cl) ->
+  | GApp ({ CAst.v = 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 b0663af70..1839c87b1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -625,13 +625,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 (someta,n) ->
+  | GPatVar 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 (k, naming, None) ->