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, 1 insertions, 1 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 7b1ccd542..4260d5553 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -101,7 +101,7 @@ let fail_quick_unif_flags = {
   resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
-  frozen_evars = ExistentialSet.empty;
+  frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;