- Débogueur: positionnement de set_detype_anonymous pour ne pas

  échouer sur les Rel liées a des Anonymous et export de l'instance
  des evars vers le printeur du débogueur.
- Suppression d'un reste de code mort lié à la V7 dans pretyping.ml.


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

1 files changed, 11 insertions, 1 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 9b257014ee..d6c711f95b 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -160,6 +160,16 @@ let pr_prim_token = function
   | Numeral n -> Bigint.pr_bigint n
   | String s -> qs s
 
+let pr_evar pr n l =
+  str (Evd.string_of_existential n) ++ 
+  (match l with
+   | Some l ->
+       pr_in_comment
+         (fun l -> 
+	   str"[" ++ hov 0 (prlist_with_sep pr_coma (pr ltop) l) ++ str"]")
+         l
+   | None -> mt())
+
 let las = lapp
 let lpator = 100
 
@@ -559,7 +569,7 @@ let rec pr sep inherited a =
       lif
      
   | CHole _ -> str "_", latom
-  | CEvar (_,n) -> str (Evd.string_of_existential n), latom
+  | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_rawsort s, latom
   | CCast (_,a,CastConv (k,b)) ->