At least made the evar type opaque! There are still 5 remaining unsafe

casts of ints to evars.

- 2 in Evarutil and Goal which are really needed, even though the Goal
one could (and should) be removed;
- 2 in G_xml and Detyping that are there for completeness sake, but
that might be made anomalies altogether;
- 1 in Newring which is quite dubious at best, and should be fixed.

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

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 27efb9a5d..225823411 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -211,7 +211,7 @@ struct
 
   let pat_of_constr c : term_pattern =
     (** To each evar we associate a unique identifier. *)
-    let metas = ref Evd.ExistentialMap.empty in
+    let metas = ref Evar.Map.empty in
     let rec pat_of_constr c = match kind_of_term c with
     | Rel _          -> Term DRel
     | Sort _         -> Term DSort
@@ -222,10 +222,10 @@ struct
     | Term.Meta _    -> assert false
     | Evar (i,_)     ->
       let meta =
-        try Evd.ExistentialMap.find i !metas
+        try Evar.Map.find i !metas
         with Not_found ->
           let meta = fresh_meta () in
-          let () = metas := Evd.ExistentialMap.add i meta !metas in
+          let () = metas := Evar.Map.add i meta !metas in
           meta
       in
       Meta meta