Options d'affichage maintenant dans Constrextern

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

1 files changed, 3 insertions, 4 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 321a095d0..ac5e3d0c8 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -26,7 +26,7 @@ open Termops
 open Clenv
 open Cerrors
 
-let _ = Termast.print_evar_arguments := true
+let _ = Constrextern.print_evar_arguments := true
 
 let pP s = pp (hov 0 s)
 
@@ -35,7 +35,7 @@ let prast c = pp(print_ast c)
 let prastpat c = pp(print_astpat c)
 let prastpatl c = pp(print_astlpat c)
 let ppterm x = pp(prterm x)
-let ppterm_univ x = Termast.with_universes ppterm x
+let ppterm_univ x = Constrextern.with_universes ppterm x
 let pprawterm = (fun x -> pp(pr_rawterm x))
 let pppattern = (fun x -> pp(pr_pattern x))
 let pptype = (fun x -> pp(prtype x))
@@ -63,8 +63,7 @@ let prconst (sp,j) =
 let prvar ((id,a)) =
     pp (str"#" ++ pr_id id ++ str":" ++ prterm a)
 
-let genprj f j =
-  let (c,t) = Termast.with_casts f j in (c ++ str " : " ++ t)
+let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
 let prj j = pp (genprj prjudge j)