diff options
| author | herbelin | 2006-10-29 22:49:11 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-29 22:49:11 +0000 |
| commit | f97016c08df3536ee51468a8b22a2a022f3f38a1 (patch) | |
| tree | 76f30f898968c0974157a9b638ad06ec441e6a68 /contrib | |
| parent | 7cae78ffc70a9097beb6d0f1a0e9f741f483e591 (diff) | |
Suite commit polymorphisme
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9316 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index afbc56f68c..f550ac73e8 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -315,12 +315,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with - | App (f,args) when isInd f -> + | App (f,args) when isInd f or isConst f -> let sigma = evars_of !isevars in - let t = Retyping.type_of_inductive_knowing_parameters 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 *) + let c = mkApp (f,Array.map (whd_evar sigma) args) in + let t = Retyping.get_type_of env sigma c in + make_judge c t | _ -> resj in inh_conv_coerce_to_tycon loc env isevars resj tycon |