summaryrefslogtreecommitdiff
path: root/pretyping/typing.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /pretyping/typing.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r--pretyping/typing.ml31
1 files changed, 7 insertions, 24 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index be922c7d..78902a7d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: typing.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: typing.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
open Util
open Names
@@ -88,14 +88,16 @@ let rec execute env evd cstr =
judge_of_type u
| App (f,args) ->
- let j = execute env evd f in
let jl = execute_array env evd args in
- let (j,_) = judge_of_apply env j jl in
+ let j =
if isInd f then
(* Sort-polymorphism of inductive types *)
- adjust_inductive_level env evd (destInd f) args j
+ judge_of_inductive_knowing_parameters env (destInd f)
+ (jv_nf_evar (evars_of evd) jl)
else
- j
+ execute env evd f
+ in
+ fst (judge_of_apply env j jl)
| Lambda (name,c1,c2) ->
let j = execute env evd c1 in
@@ -141,25 +143,6 @@ and execute_array env evd = Array.map (execute env evd)
and execute_list env evd = List.map (execute env evd)
-and adjust_inductive_level env evd ind args j =
- let specif = lookup_mind_specif env ind in
- if is_small_inductive specif then
- (* No polymorphism *)
- j
- else
- (* Retyping constructor with the actual arguments *)
- let env',llc,ls0 = constructor_instances env specif ind args in
- let llj = Array.map (execute_array env' evd) llc in
- let ls =
- Array.map (fun lj ->
- let ls =
- Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj
- in
- max_inductive_sort ls) llj
- in
- let s = find_inductive_level env specif ind ls0 ls in
- on_judgment_type (set_inductive_level env s) j
-
let mcheck env evd c t =
let sigma = Evd.evars_of evd in
let j = execute env evd (nf_evar sigma c) in