diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 914c951eb6..69edb1498c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref type link_info = | Linked of string - | LinkedInteractive of string | NotLinked type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) @@ -569,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) |