aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r--pretyping/typing.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 339ca19fb..5cd05c58d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -207,12 +207,12 @@ let rec execute env evdref cstr =
let jl = execute_array env evdref args in
let j =
match kind_of_term f with
- | Ind ind when Environ.template_polymorphic_ind ind env ->
+ | Ind ind when Environ.template_polymorphic_pind ind env ->
(* Sort-polymorphism of inductive types *)
make_judge f
(inductive_type_knowing_parameters env ind
(Evarutil.jv_nf_evar !evdref jl))
- | Const cst when Environ.template_polymorphic_constant cst env ->
+ | Const cst when Environ.template_polymorphic_pconstant cst env ->
(* Sort-polymorphism of inductive types *)
make_judge f
(constant_type_knowing_parameters env cst