diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 5914e66fc3..69edb1498c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -568,6 +568,11 @@ let is_primitive env c = | Declarations.Primitive _ -> true | _ -> false +let is_array_type env c = + match env.retroknowledge.Retroknowledge.retro_array with + | None -> false + | Some c' -> Constant.CanOrd.equal c c' + let polymorphic_constant cst env = Declareops.constant_is_polymorphic (lookup_constant cst env) |