Ajout make_typed_lazy

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

2 files changed, 3 insertions, 10 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 27f7d7a11c..de4d6cbce0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -73,6 +73,7 @@ type typed_type = sorts judge
 type typed_term = typed_type judge
 
 let make_typed t s = { body = t; typ = s }
+let make_typed_lazy t f = { body = t; typ = f s }
 
 let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
@@ -92,6 +93,7 @@ type typed_type = constr
 type typed_term = typed_type judge
 
 let make_typed t s = t
+let make_typed_lazy t f = t
 
 let typed_app f tt = f tt
 
@@ -341,14 +343,6 @@ let destCast = function
 
 let isCast = function DOP2(Cast,_,_) -> true | _ -> false
 
-let cast_term = function
-  | DOP2(Cast,c,t) -> c
-  | _ -> anomaly "found a type which did not contain a cast (cast_term)"
-
-let cast_type = function
-  | DOP2(Cast,c,t) -> t
-  | _ -> anomaly "found a type which did not contain a cast (cast_type)"
-
 let rec strip_outer_cast = function
   | DOP2(Cast,c,_) -> strip_outer_cast c
   | c -> c
diff --git a/kernel/term.mli b/kernel/term.mli
index bfeccb0c72..7e2e916def 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -63,6 +63,7 @@ type typed_type
 type typed_term = typed_type judge
 
 val make_typed : constr -> sorts -> typed_type
+val make_typed_lazy : constr -> (constr -> sorts) -> typed_type
 
 val typed_app : (constr -> constr) -> typed_type -> typed_type
 val typed_combine : (constr -> constr -> constr) -> (sorts -> sorts -> sorts)
@@ -283,8 +284,6 @@ val is_small : sorts -> bool (* true for \textsf{Prop} and \textsf{Set} *)
 
 (* Destructs a casted term *)
 val destCast : constr -> constr * constr
-val cast_type : constr -> constr (* 2nd proj *)
-val cast_term : constr -> constr (* 1st proj *)
 val isCast : constr -> bool
 
 (* Removes recursively the casts around a term i.e.