From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 pretyping/retyping.ml | 26 +++++++++-----------------
 1 file changed, 9 insertions(+), 17 deletions(-)

(limited to 'pretyping/retyping.ml')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 32da4cea..428a7306 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: retyping.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
 
 open Util
 open Term
@@ -74,7 +74,7 @@ let typeur sigma metamap =
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
     | App(f,args) when isInd f ->
-	let t = type_of_applied_inductive env (destInd f) args in
+	let t = type_of_inductive_knowing_parameters env (destInd f) args in
         strip_outer_cast (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
         strip_outer_cast
@@ -98,7 +98,7 @@ let typeur sigma metamap =
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
     | App(f,args) when isInd f ->
-	let t = type_of_applied_inductive env (destInd f) args in
+	let t = type_of_inductive_knowing_parameters env (destInd f) args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
@@ -117,25 +117,17 @@ let typeur sigma metamap =
         anomaly "sort_of: Not a type (1)"
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
-  and type_of_applied_inductive env ind args =
-    let specif = lookup_mind_specif env ind in
-    let t = Inductive.type_of_inductive specif in
-    if is_small_inductive specif then
-      (* No polymorphism *)
-      t
-    else
-      (* Retyping constructor with the actual arguments *)
-      let env',llc,ls0 = constructor_instances env specif ind args in
-      let lls = Array.map (Array.map (sort_of env')) llc in
-      let ls = Array.map max_inductive_sort lls in
-      set_inductive_level env (find_inductive_level env specif ind ls0 ls) t
+  and type_of_inductive_knowing_parameters env ind args =
+    let (_,mip) = lookup_mind_specif env ind in
+    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
+    Inductive.type_of_inductive_knowing_parameters env mip argtyps
 
-  in type_of, sort_of, sort_family_of, type_of_applied_inductive
+  in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters
 
 let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
 let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
 let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
-let type_of_applied_inductive env sigma ind args =
+let type_of_inductive_knowing_parameters env sigma ind args =
   let _,_,_,f = typeur sigma [] in f env ind args
 
 let get_type_of_with_meta env sigma metamap = 
-- 
cgit v1.2.3