From 33eea163c72c70eaa3bf76506c1d07a8cde911fd Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 18 Sep 2013 18:29:40 +0000
Subject: 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
---
 dev/include         | 2 +-
 dev/printers.mllib  | 1 +
 dev/top_printers.ml | 7 ++++---
 3 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/include b/dev/include
index 15725ae8b6..f785573ceb 100644
--- a/dev/include
+++ b/dev/include
@@ -45,7 +45,7 @@
 #install_printer  (* Goal.goal *)  ppgoalgoal;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
-#install_printer  (* ExistentialSet.t *) ppexistentialset;;
+#install_printer  (* Evar.Set.t *) ppexistentialset;;
 #install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 8e99b5247a..1eb3aa4bb5 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -45,6 +45,7 @@ Names
 Univ
 Esubst
 Sorts
+Evar
 Constr
 Context
 Vars
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 89e2d7ddde..6bb352c5eb 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -106,11 +106,12 @@ let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
 
 (* proof printers *)
+let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
 let ppevm evd = pp(pr_evar_map (Some 2) evd)
 let ppevmall evd = pp(pr_evar_map None evd)
 let pr_existentialset evars =
-  prlist_with_sep spc pr_meta (ExistentialSet.elements evars)
+  prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
   pp (pr_existentialset evars)
 let ppclenv clenv = pp(pr_clenv clenv)
@@ -172,7 +173,7 @@ let constr_display csr =
       "LetIn("^(name_display na)^","^(term_display b)^","
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
-  | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
+  | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")"
   | Const c -> "Const("^(string_of_con c)^")"
   | Ind (sp,i) ->
       "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")"
@@ -250,7 +251,7 @@ let print_pure_constr csr =
       box_display c;
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string ")"
-  | Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
+  | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{";
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string"}"
   | Const c -> print_string "Cons(";
-- 
cgit v1.2.3