From e7c20952e90d4f70ae84ab60b6aab62691c18aa0 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 29 Mar 2006 21:21:52 +0000 Subject: Inductifs avec polymorphisme de sorte (version initiale) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pretyping.ml | 27 ++++++++++++--------------- 1 file changed, 12 insertions(+), 15 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 68342e706..b99ada769 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -367,21 +367,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct (join_loc floc argloc) env (evars_of !isevars) resj [hj] - in let resj = apply_rec env 1 fj args in - (* - let apply_one_arg (floc,tycon,jl) c = - let (dom,rng) = split_tycon floc env isevars tycon in - let cj = pretype dom env isevars lvar c in - let rng_tycon = - option_app (subst1 cj.uj_val) rng in - let argloc = loc_of_rawconstr c in - (join_loc floc argloc,rng_tycon,(argloc,cj)::jl) in - let _,_,jl = - List.fold_left apply_one_arg (floc,mk_tycon j.uj_type,[]) args in - let jl = List.rev jl in - let resj = inh_apply_rel_list loc env isevars jl (floc,j) tycon in - *) - inh_conv_coerce_to_tycon loc env isevars resj tycon + in + let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in + let resj = + match kind_of_term resj.uj_val with + | App (f,args) when isInd f -> + let sigma = evars_of !isevars in + let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in + let s = snd (splay_arity env sigma t) in + on_judgment_type (set_inductive_level env s) resj + (* Rem: no need to send sigma: no head evar, it's an arity *) + | _ -> resj in + inh_conv_coerce_to_tycon loc env isevars resj tycon | RLambda(loc,name,c1,c2) -> let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in -- cgit v1.2.3