diff options
| author | Matthieu Sozeau | 2014-09-27 16:08:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-27 20:41:04 +0200 |
| commit | 84544396cbbf34848be2240acf181b4d5f1f42d2 (patch) | |
| tree | 72d398f334bdc7b1c6a0ee333a05940c34780f12 /kernel/cbytegen.ml | |
| parent | 0efba04058ba28889c83553224309be216873298 (diff) | |
Add a boolean to indicate the unfolding state of a primitive projection,
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 36a022fd98..6fd1c689ff 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -501,11 +501,12 @@ let rec compile_constr reloc c sz cont = | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" | Proj (p,c) -> (* compile_const reloc p [|c|] sz cont *) - let cb = lookup_constant p !global_env in + let kn = Projection.constant p in + let cb = lookup_constant kn !global_env in (* TODO: better representation of projections *) let pb = Option.get cb.const_proj in let args = Array.make pb.proj_npars mkProp in - compile_const reloc p Univ.Instance.empty (Array.append args [|c|]) sz cont + compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont | Cast(c,_,_) -> compile_constr reloc c sz cont |