diff options
| author | Maxime Dénès | 2018-06-05 23:12:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-05 23:12:47 +0200 |
| commit | af902fa028f8ceb152d9add198e7dd490a4394ca (patch) | |
| tree | 002f7dde0d60cf865d5e643204827eee132299ee /kernel/nativevalues.ml | |
| parent | 1c67e29e735ab1e7bb121304f710ef48a23a8b9b (diff) | |
| parent | e1e7888ac4519f4b7470cc8469f9fd924514e352 (diff) | |
Merge PR #7679: Clean native compilation of primitive projections
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index cfcb0a485b..da4413a0ad 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -64,7 +64,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t * t array - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 |