diff options
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 2a7b390951..0eb3eaf940 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -23,5 +23,5 @@ type retroknowledge = { val empty : retroknowledge type action = - | Register_ind of CPrimitives.prim_ind * inductive - | Register_type of CPrimitives.prim_type * Constant.t + | Register_ind : 'a CPrimitives.prim_ind * inductive -> action + | Register_type : CPrimitives.prim_type * Constant.t -> action |