aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativevalues.ml')
-rw-r--r--kernel/nativevalues.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 1c9996d89..2f8920088 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -58,10 +58,10 @@ type atom =
(* types, bodies, rec_pos, pos *)
| Acofix of t array * t array * int * t
| Acofixe of t array * t array * int * t
- | Aprod of name * t * (t -> t)
+ | Aprod of Name.t * t * (t -> t)
| Ameta of metavariable * t
| Aevar of existential * t
- | Aproj of constant * accumulator
+ | Aproj of Constant.t * accumulator
let accumulate_tag = 0