Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 4 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 0610c00f1..47cc57fd1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -111,7 +111,7 @@ let pattern_of_constr sigma t =
           match kind_of_term f with
             Evar (evk,args as ev) ->
               (match snd (Evd.evar_source evk sigma) with
-                  MatchingVar (true,id) ->
+                  Evar_kinds.MatchingVar (true,id) ->
                     ctx := (id,None,existential_type sigma ev)::!ctx;
                     Some id
                 | _ -> None)
@@ -124,10 +124,10 @@ let pattern_of_constr sigma t =
     | Construct sp -> PRef (canonical_gr (ConstructRef sp))
     | Evar (evk,ctxt as ev) ->
         (match snd (Evd.evar_source evk sigma) with
-          | MatchingVar (b,id) ->
+          | Evar_kinds.MatchingVar (b,id) ->
               ctx := (id,None,existential_type sigma ev)::!ctx;
               assert (not b); PMeta (Some id)
-          | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
+          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
@@ -308,7 +308,8 @@ let rec pat_of_raw metas vars = function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (loc,nal,(_,None),b,c) ->
-      let mkGLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in
+      let mkGLambda c na =
+	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole),c) in
       let c = List.fold_left mkGLambda c nal in
       let cip =
 	{ cip_style = LetStyle;