From 29b2b65a4ac3154860189b6123b561bed3d16c15 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 May 2000 13:23:25 +0000
Subject: Réorganisation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@424 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 9 +++++----
 pretyping/retyping.ml  | 2 +-
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3401298136..77c422b378 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -279,6 +279,10 @@ let pretype_ref loc isevars env lvar = function
     let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in
     {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind}
 
+let pretype_sort = function
+  | RProp c -> judge_of_prop_contents c
+  | RType -> { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort}
+
 (* pretype vtcon isevars env constr tries to solve the *)
 (* existential variables in constr in environment env with the *)
 (* constraint vtcon (see Tradevar). *)
@@ -358,10 +362,7 @@ match cstr with   (* O
 	check_cofix env !isevars cofix;
 	make_judge cofix lara.(i))
 
-| RSort (loc,RProp c) -> judge_of_prop_contents c
-
-| RSort (loc,RType) -> 
-    { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort }
+| RSort (loc,s) -> pretype_sort s
 
 | RApp (loc,f,args) -> 
     let j = pretype empty_tycon env isevars lvar lmeta f in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 0e61614b3d..6eb095d539 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -15,7 +15,7 @@ type metamap = (int * constr) list
 let outsort env sigma t =
   match whd_betadeltaiota env sigma t with
       DOP0(Sort s) -> s
-    | _ -> anomaly "outsort: Not a sort"
+    | _ -> anomaly "Retyping: found a type of type which is not a sort"
 
 let rec subst_type env sigma typ = function
     [] -> typ
-- 
cgit v1.2.3