diff options
| author | Pierre Letouzey | 2014-02-17 14:32:50 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-01-11 09:49:32 +0100 |
| commit | d15d8cc0ce584a6d80d878faf84314c6712ccf69 (patch) | |
| tree | 0042925526cfd801451cdbe5472f44cd2169a57c /plugins/extraction/table.ml | |
| parent | b858f939f33dc4bc4c8e470ed62310ef15c59a99 (diff) | |
Extraction: minor tweaks to ease ongoing experiments about Lambda
- Common.get_native_char instead of just a pp function of this char
- Enrich the record projection table
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2f64a24ab3..f2d8c3bc07 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -189,11 +189,12 @@ let is_recursor = function (* NB: here, working modulo name equivalence is ok *) -let projs = ref (Refmap.empty : int Refmap.t) +let projs = ref (Refmap.empty : (inductive*int) Refmap.t) let init_projs () = projs := Refmap.empty -let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs +let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs let is_projection r = Refmap.mem r !projs -let projection_arity r = Refmap.find r !projs +let projection_arity r = snd (Refmap.find r !projs) +let projection_info r = Refmap.find r !projs (*s Table of used axioms *) |