diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 2f6a870c8a..7609c1a64d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -55,7 +55,7 @@ type ('a, 'opaque) constant_def = | Undef of inline (** a global assumption *) | Def of 'a (** or a transparent global definition *) | OpaqueDef of 'opaque (** or an opaque global definition *) - | Primitive of CPrimitives.t (** or a primitive operation *) + | Primitive of CPrimitives.t (** or a primitive operation *) type universes = | Monomorphic of Univ.ContextSet.t @@ -94,6 +94,10 @@ type typing_flags = { cumulative_sprop : bool; (** SProp <= Type *) + + allow_uip: bool; + (** Allow definitional UIP (breaks termination) *) + } (* some contraints are in constant_constraints, some other may be in @@ -112,11 +116,14 @@ type 'opaque constant_body = { } (** {6 Representation of mutual inductive types in the kernel } *) +type nested_type = +| NestedInd of inductive +| NestedPrimitive of Constant.t type recarg = - | Norec - | Mrec of inductive - | Imbr of inductive +| Norec +| Mrec of inductive +| Nested of nested_type type wf_paths = recarg Rtree.t |