diff options
Diffstat (limited to 'contrib/extraction/miniml.mli')
| -rw-r--r-- | contrib/extraction/miniml.mli | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 7c18f9f5..3b4146f8 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*) +(*i $Id: miniml.mli 9456 2006-12-17 20:08:38Z letouzey $ i*) (*s Target language for extraction: a core ML called MiniML. *) @@ -18,11 +18,18 @@ open Libnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML object. *) + +(* We eliminate from terms: 1) types 2) logical parts. + [Kother] stands both for logical or unknown reason. *) + +type kill_reason = Ktype | Kother + +type sign = Keep | Kill of kill_reason + -(* Convention: outmost lambda/product gives the head of the list, - and [true] means that the argument is to be kept. *) +(* Convention: outmost lambda/product gives the head of the list. *) -type signature = bool list +type signature = sign list (*s ML type expressions. *) @@ -32,7 +39,7 @@ type ml_type = | Tvar of int | Tvar' of int (* same as Tvar, used to avoid clash *) | Tmeta of ml_meta (* used during ML type reconstruction *) - | Tdummy + | Tdummy of kill_reason | Tunknown | Taxiom @@ -72,7 +79,9 @@ type ml_ind_packet = { type ml_ind = { ind_info : inductive_info; ind_nparams : int; - ind_packets : ml_ind_packet array } + ind_packets : ml_ind_packet array; + ind_equiv : kernel_name option +} (*s ML terms. *) |