Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort

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

6 files changed, 11 insertions, 7 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 7b19b1b6c5..9a6f379b3a 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -117,7 +117,7 @@ let pr_optc pr = function
 
 let pr_universe = Univ.pr_uni 
 
-let pr_sort = function
+let pr_rawsort = function
   | RProp Term.Null -> str "Prop"
   | RProp Term.Pos -> str "Set"
   | RType u -> str "Type" ++ pr_opt pr_universe u
@@ -563,7 +563,7 @@ let rec pr sep inherited a =
   | CHole _ -> str "_", latom
   | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
-  | CSort (_,s) -> pr_sort s, latom
+  | CSort (_,s) -> pr_rawsort s, latom
   | CCast (_,a,_,b) ->
       hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b),
       lcast
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 5c3daa28eb..e7e8a4bbc0 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -60,7 +60,7 @@ val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
     ('a,'b) may_eval -> std_ppcmds
 
-val pr_sort : rawsort -> std_ppcmds
+val pr_rawsort : rawsort -> std_ppcmds
 
 val pr_binders : local_binder list -> std_ppcmds
 val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f1388ab69c..d5a94cd179 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -139,7 +139,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
   | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
   | VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x)
   | RefArgType -> pr_arg prref (out_gen rawwit_ref x)
-  | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
+  | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
       pr_arg (pr_may_eval prc prlc prref)
@@ -182,7 +182,7 @@ let rec pr_glob_generic prc prlc prtac x =
   | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x)
   | VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x)
   | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
-  | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x)
+  | SortArgType -> pr_arg pr_rawsort (out_gen globwit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
       pr_arg (pr_may_eval prc prlc
@@ -228,7 +228,7 @@ let rec pr_generic prc prlc prtac x =
   | IdentArgType -> pr_arg pr_id (out_gen wit_ident x)
   | VarArgType -> pr_arg pr_id (out_gen wit_var x)
   | RefArgType -> pr_arg pr_global (out_gen wit_ref x)
-  | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x))
+  | SortArgType -> pr_arg pr_sort (out_gen wit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen wit_constr x)
   | ConstrMayEvalArgType ->
       pr_arg prc (out_gen wit_constr_may_eval x)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c0aa771ae0..c50b2e52f3 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -277,7 +277,7 @@ let pr_onescheme (id,dep,ind,s) =
   hov 0 (pr_lident id ++ str" :=") ++ spc() ++
   hov 0 ((if dep then str"Induction for" else str"Minimality for")
   ++ spc() ++ pr_reference ind) ++ spc() ++ 
-  hov 0 (str"Sort" ++ spc() ++ pr_sort s)
+  hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
 
 let begin_of_inductive = function
     [] -> 0
diff --git a/parsing/printer.ml b/parsing/printer.ml
index d6d7534955..e1c8b2505e 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -87,6 +87,8 @@ let pr_lconstr_pattern t =
 let pr_constr_pattern t =
   pr_constr_expr (extern_constr_pattern empty_names_context t)
 
+let pr_sort s = pr_rawsort (extern_sort s)
+
 let _ = Termops.set_print_constr pr_lconstr_env
 
 (**********************************************************************)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 3048a7e46c..cd9b526a48 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -58,6 +58,8 @@ val pr_constr_pattern      : constr_pattern -> std_ppcmds
 
 val pr_cases_pattern       : cases_pattern -> std_ppcmds
 
+val pr_sort                : sorts -> std_ppcmds
+
 (* Printing global references using names as short as possible *)
 
 val pr_global_env          : Idset.t -> global_reference -> std_ppcmds