diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-30 17:53:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:20:30 +0100 |
| commit | 5143129baac805d3a49ac3ee9f3344c7a447634f (patch) | |
| tree | 60fd3fb22fc95474454a6a60f3a8715bf7d766d0 /pretyping/retyping.ml | |
| parent | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (diff) | |
Termops API using EConstr.
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5b67af3e7..ac3b5ef63 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -93,7 +93,7 @@ let retype ?(polyprop=true) sigma = let rec type_of env cstr = match kind_of_term cstr with | Meta n -> - (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus + (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) with Not_found -> retype_error (BadMeta n)) | Rel n -> let ty = RelDecl.get_type (lookup_rel n env) in @@ -124,12 +124,13 @@ let retype ?(polyprop=true) sigma = subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> + let f = whd_evar sigma f in let t = type_of_global_reference_knowing_parameters env f args in - strip_outer_cast (subst_type env sigma t (Array.to_list args)) + strip_outer_cast sigma (EConstr.of_constr (subst_type env sigma t (Array.to_list args))) | App(f,args) -> - strip_outer_cast - (subst_type env sigma (type_of env f) (Array.to_list args)) + strip_outer_cast sigma + (EConstr.of_constr (subst_type env sigma (type_of env f) (Array.to_list args))) | Proj (p,c) -> let ty = type_of env c in (try @@ -152,7 +153,8 @@ let retype ?(polyprop=true) sigma = | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> + let f = whd_evar sigma f in let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args @@ -168,7 +170,8 @@ let retype ?(polyprop=true) sigma = let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> + let f = whd_evar sigma f in let t = type_of_global_reference_knowing_parameters env f args in family_of_sort (sort_of_atomic_type env sigma t args) | App(f,args) -> |