From 7534d56bf9b4b5f23b1fe1df87288c2d7565853a Mon Sep 17 00:00:00 2001 From: filliatr Date: Mon, 30 Aug 1999 15:12:11 +0000 Subject: typage constructeur : on ajoute les contraintes d'univers en typant l'arité c d'un constructeur en mettant les paramètres p dans l'environnement, et non pas en typant le produit (p)c. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@34 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/typing.ml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'kernel') diff --git a/kernel/typing.ml b/kernel/typing.ml index 1366738689..1b5a14a3a5 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -354,16 +354,19 @@ let enforce_type_constructor env univ j = set_universes (enforce_geq univ uc u) env | _ -> error "Type of Constructor not well-formed" -let type_one_constructor env_ar env_par nparams ar c = - let (jc,u) = safe_machine env_ar c in - let env = set_universes u env_ar in - let env' = match sort_of_arity env_ar ar with - | Type u -> enforce_type_constructor env u jc - | Prop _ -> env +let type_one_constructor env_ar nparams ar c = + let (params,dc) = decompose_prod_n nparams c in + let env_par = push_rels params env_ar in + let (jc,u) = safe_machine env_par dc in + let env_par' = set_universes u env_par in + let env_par'' = match sort_of_arity env_ar ar with + | Type u -> enforce_type_constructor env_par' u jc + | Prop _ -> env_par' in - let (_,c) = decompose_prod_n nparams jc.uj_val in + let env_ar' = set_universes (universes env_par'') env_ar in + let (j,u) = safe_machine env_ar' c in let issmall = is_small_type env_par c in - (env', (issmall,jc)) + (set_universes u env_ar', (issmall,j)) let logic_constr env c = for_all_prods (fun t -> not (is_info_type env t)) env c @@ -384,7 +387,7 @@ let type_one_inductive env_ar env_par nparams (id,ar,cnames,spec) = let (env',(issmall,jlc)) = List.fold_left (fun (env,(small,jl)) c -> - let (env',(sm,jc)) = type_one_constructor env env_par nparams ar c in + let (env',(sm,jc)) = type_one_constructor env nparams ar c in (env', (small && sm,jc::jl))) (env_ar,(true,[])) (Array.to_list vc) in -- cgit v1.2.3