diff options
| author | Matthieu Sozeau | 2015-01-15 18:45:27 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:43 +0530 |
| commit | c87579a20b8f99b8dd968320f96dd470d274c3ca (patch) | |
| tree | c0600c17af66feaee7529b6291f62b975dfc600a /pretyping | |
| parent | 93628d2e7156943edf3cfffa25a21855fb4b06db (diff) | |
Correct restriction of vm_compute when handling universe polymorphic
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 4 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 11 |
2 files changed, 7 insertions, 8 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3f9f7ff289..203b1ec8a6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -511,8 +511,8 @@ let oracle_order env cf1 cf2 = when eq_constant p (Projection.constant p') -> Some (Projection.unfolded p') | _ -> - Some (Conv_oracle.oracle_order (Environ.oracle env) false - (translate_key k1) (translate_key k2)) + Some (Conv_oracle.oracle_order (fun x -> x) + (Environ.oracle env) false (translate_key k1) (translate_key k2)) let is_rigid_head flags t = match kind_of_term t with diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 1d97aef278..3f1e6e5d60 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -93,12 +93,11 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false -(* FIXME: treatment of universes *) let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - let const_type = (Environ.lookup_constant cst env).const_type in - mkConst cst, Typeops.type_of_constant_type env const_type + let const_type = Typeops.type_of_constant_in env cst in + mkConstU cst, const_type | VarKey id -> let (_,_,ty) = lookup_named id env in mkVar id, ty @@ -107,7 +106,7 @@ let constr_type_of_idkey env idkey = let (_,_,ty) = lookup_rel n env in mkRel n, lift n ty -let type_of_ind env ind u = +let type_of_ind env (ind, u) = type_of_inductive env (Inductive.lookup_mind_specif env ind, u) let build_branches_type env (mind,_ as _ind) mib mip u params dep p = @@ -176,7 +175,7 @@ and nf_whd env whd typ = | Vatom_stk(Aiddef(idkey,v), stk) -> nf_whd env (whd_stack v stk) typ | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkInd ind) (type_of_ind env ind Univ.Instance.empty (*FIXME*)) stk + nf_stk env (mkIndU ind) (type_of_ind env ind) stk and nf_stk env c t stk = match stk with @@ -194,7 +193,7 @@ and nf_stk env c t stk = let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in let pT = - hnf_prod_applist env (type_of_ind env ind u) (Array.to_list params) in + hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_betadeltaiota env pT in let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in (* Calcul du type des branches *) |