diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-02-17 14:32:50 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-01-11 09:49:32 +0100 |
| commit | d15d8cc0ce584a6d80d878faf84314c6712ccf69 (patch) | |
| tree | 0042925526cfd801451cdbe5472f44cd2169a57c /plugins/extraction/table.mli | |
| 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.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 823b710cf..e8513e4d4 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -85,9 +85,10 @@ val record_fields_of_type : ml_type -> global_reference option list val add_recursors : Environ.env -> mutual_inductive -> unit val is_recursor : global_reference -> bool -val add_projection : int -> constant -> unit +val add_projection : int -> constant -> inductive -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int +val projection_info : global_reference -> inductive * int (* arity *) val add_info_axiom : global_reference -> unit val remove_info_axiom : global_reference -> unit |