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

10 files changed, 27 insertions, 15 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e3d4d1a4d6..e73e88587b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -623,6 +623,11 @@ let extern_optimal_prim_token scopes r r' =
 (**********************************************************************)
 (* mapping rawterms to constr_expr                                    *)
 
+let extern_rawsort = function
+  | RProp _ as s -> s
+  | RType (Some _) as s when !print_universes -> s
+  | RType _ -> RType None
+
 let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
   try 
@@ -740,12 +745,7 @@ let rec extern inctx scopes vars r =
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
-  | RSort (loc,s) ->
-      let s = match s with
-	 | RProp _ -> s
-	 | RType (Some _) when !print_universes -> s
-	 | RType _ -> RType None in
-      CSort (loc,s)
+  | RSort (loc,s) -> CSort (loc,extern_rawsort s)
 
   | RHole (loc,e) -> CHole loc
 
@@ -873,6 +873,8 @@ let extern_type at_top env t =
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   extern_rawtype (vars_of_env env) r
 
+let extern_sort s = extern_rawsort (detype_sort s)
+
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 37f7369ad6..0ffb8c333a 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -41,6 +41,7 @@ val extern_constr : bool -> env -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
 val extern_reference : loc -> Idset.t -> global_reference -> reference
 val extern_type : bool -> env -> types -> constr_expr
+val extern_sort : sorts -> rawsort
 
 (* Printing options *)
 val print_implicits : bool ref
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
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1f6e4a86b7..ec6edcbdfd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -348,6 +348,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
   | _ ->
       RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
 
+let detype_sort = function
+  | Prop c -> RProp c
+  | Type u -> RType (Some u)
+
 (**********************************************************************)
 (* Main detyping function                                             *)
 
@@ -368,8 +372,7 @@ let rec detype isgoal avoid env t =
 	  let _ = Global.lookup_named id in RRef (dl, VarRef id)
 	 with _ ->
 	  RVar (dl, id))
-    | Sort (Prop c) -> RSort (dl,RProp c)
-    | Sort (Type u) -> RSort (dl,RType (Some u))
+    | Sort s -> RSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
 	RCast(dl,detype isgoal avoid env c1, k,
               detype isgoal avoid env c2)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 3068f97c28..7f979d6e6d 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -38,6 +38,8 @@ val detype_case :
   identifier list -> inductive * case_style * int * int array * int ->
     'a option -> 'a -> 'a array -> rawconstr
 
+val detype_sort : sorts -> rawsort
+
 (* look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_renamed  : env -> constr -> identifier -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option