diff options
Diffstat (limited to 'kernel/primred.mli')
| -rw-r--r-- | kernel/primred.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/primred.mli b/kernel/primred.mli index 1bfaffaa44..6e9d4e297e 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -2,6 +2,13 @@ open Names open Environ (** {5 Reduction of primitives} *) +type _ action_kind = + | IncompatTypes : _ CPrimitives.prim_type -> Constant.t action_kind + | IncompatInd : _ CPrimitives.prim_ind -> inductive action_kind + +type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn + +(** May raise [IncomtibleDeclarations] *) val add_retroknowledge : env -> Retroknowledge.action -> env val get_int_type : env -> Constant.t |