Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

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

4 files changed, 8 insertions, 19 deletions

diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 71f1b03bdc..6465bdd88f 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -61,6 +61,6 @@ constr_of_com_casted -> interp_casted_constr
 constr_of_com_sort   -> interp_type
 constr_of_com        -> interp_constr
 rawconstr_of_com     -> interp_rawconstr  [+ env instead of sign]
-type_of_com          -> typed_type_of_com Evd.empty
+type_of_com          -> types_of_com Evd.empty
 constr_of_com1 true  -> interp_type
 *)
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 43f28fbe6b..5b4317f2a2 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -404,7 +404,7 @@ let print_val env {uj_val=trm;uj_type=typ} =
   print_typed_value_in_env env (trm,typ)
     
 let print_type env {uj_val=trm;uj_type=typ} =
-  print_typed_value_in_env env (trm, typed_app (nf_betaiota env Evd.empty) typ)
+  print_typed_value_in_env env (trm, type_app (nf_betaiota env Evd.empty) typ)
     
 let print_eval red_fun env {uj_val=trm;uj_type=typ} =
   let ntrm = red_fun env Evd.empty trm in
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 04578675ac..3bda750b0b 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -91,24 +91,13 @@ let prterm_env_at_top env = gentermpr_core true env
 let prterm_env env = gentermpr_core false env
 let prterm = prterm_env empty_env
 
-let prtype_env env typ = prterm_env env (incast_type typ)
+let prtype_env env typ = prterm_env env typ
 let prtype = prtype_env empty_env
 
 let prjudge_env env j =
-  (prterm_env env j.uj_val, prterm_env env (incast_type j.uj_type))
+  (prterm_env env j.uj_val, prterm_env env j.uj_type)
 let prjudge = prjudge_env empty_env
 
-(* Plus de "k"...
-let gentermpr k = gentermpr_core false
-let gentermpr_at_top k = gentermpr_core true
-
-let fprterm_env a = gentermpr FW a
-let fprterm = fprterm_env empty_env
-
-let fprtype_env env typ = fprterm_env env (incast_type typ)
-let fprtype = fprtype_env empty_env
-*)
-
 let fprterm_env a =
   warning "Fw printing not implemented, use CCI printing 1"; prterm_env a
 let fprterm a =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 3e5b589b4a..d9d3b5ce5f 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -17,8 +17,8 @@ val gentacpr  : Coqast.t -> std_ppcmds
 val prterm_env      : env -> constr -> std_ppcmds
 val prterm_env_at_top : env -> constr -> std_ppcmds
 val prterm          : constr -> std_ppcmds
-val prtype_env      : env -> typed_type -> std_ppcmds
-val prtype          : typed_type -> std_ppcmds
+val prtype_env      : env -> types -> std_ppcmds
+val prtype          : types -> std_ppcmds
 val prjudge_env     :
   env -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
 val prjudge         : Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
@@ -48,8 +48,8 @@ val emacs_str       : string -> string
 (*i*) 
 val fprterm_env     : env -> constr -> std_ppcmds
 val fprterm         : constr -> std_ppcmds
-val fprtype_env     : env -> typed_type -> std_ppcmds
-val fprtype         : typed_type -> std_ppcmds
+val fprtype_env     : env -> types -> std_ppcmds
+val fprtype         : types -> std_ppcmds
 
 (* For compatibility *)
 val fterm0          : env -> constr -> std_ppcmds