diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-13 02:09:56 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-13 03:16:20 +0200 |
commit | beb417ffd2ab9acb708c4e54dd28363bcb613853 (patch) | |
tree | b418ec648eb284290e1146255c9a1625b593f53f /kernel/nativecode.ml | |
parent | 01f230dcce3931e1a74b603b0530448af53cac3c (diff) |
Store the {struct} inductive type in native fixpoint AST.
Diffstat (limited to 'kernel/nativecode.ml')
-rw-r--r-- | kernel/nativecode.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 8d69eacbc..b09cd3f79 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1142,7 +1142,7 @@ let ml_of_instance instance u = mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] | Lif(t,bt,bf) -> MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) - | Lfix ((rec_pos,start), (ids, tt, tb)) -> + | Lfix ((rec_pos, inds, start), (ids, tt, tb)) -> (* let type_f fvt = [| type fix |] let norm_f1 fv f1 .. fn params1 = body1 .. |