diff options
| author | Hugo Herbelin | 2018-10-30 15:04:06 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-31 16:16:41 +0100 |
| commit | ae39925d64cc51663ab3f2ad397501b435bd0e5e (patch) | |
| tree | 6bb3f85d9654b17b890d0332125315653063e08a /pretyping | |
| parent | 2a93216a3851688dd29c06a29c6d1442898faab8 (diff) | |
Renaming is_template_polymorphic -> is_template_polymorphic_ind.
This emphasizes that it works only on inductive types.
Also, the name is_template_polymorphic will be reused for a more
general version.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 8 |
3 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index dd38ec6f64..96213af9c6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) (** Refresh the types of evars under template polymorphic references *) let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with - | App (f, args) when is_template_polymorphic env !evdref f -> + | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f -> let pos = get_polymorphic_positions !evdref f in refresh_polymorphic_positions args pos; t | App (f, args) when top && isEvar !evdref f -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 55817f1b76..756e2d4bc9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -691,7 +691,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma let sigma, resj = match EConstr.kind sigma resj.uj_val with | App (f,args) -> - if is_template_polymorphic !!env sigma f then + if Termops.is_template_polymorphic_ind !!env sigma f then (* Special case for inductive type applications that must be refreshed right away. *) let c = mkApp (f, args) in diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 7e43c5e41d..62ad296ecb 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -130,7 +130,7 @@ 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 sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in strip_outer_cast sigma (subst_type env sigma t (Array.to_list args)) | App(f,args) -> @@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma = let dom = sort_of env t in let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in Typeops.sort_of_product env dom rang - | App(f,args) when is_template_polymorphic env sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> 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 @@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = 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 sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> if truncation_style then InType else let t = type_of_global_reference_knowing_parameters env f args in Sorts.family (sort_of_atomic_type env sigma t args) | App(f,args) -> Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType + | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType | _ -> Sorts.family (decomp_sort env sigma (type_of env t)) in sort_family_of env t |