diff options
| -rw-r--r-- | engine/termops.ml | 2 | ||||
| -rw-r--r-- | engine/termops.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 8 | ||||
| -rw-r--r-- | proofs/logic.ml | 4 |
6 files changed, 10 insertions, 10 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index f720e5195d..c0dd9d07d1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1173,7 +1173,7 @@ let isGlobalRef sigma c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let is_template_polymorphic env sigma f = +let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false diff --git a/engine/termops.mli b/engine/termops.mli index 1054fbbc5e..07c9541f25 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -282,7 +282,7 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool +val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool 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 diff --git a/proofs/logic.ml b/proofs/logic.ml index b8612cd2c0..4d5711c195 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -384,7 +384,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) then + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let ty = (* Template polymorphism of definitions and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in @@ -447,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) |