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

1 files changed, 6 insertions, 5 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 0818a55256..71dbc39f3f 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,