diff options
Diffstat (limited to 'contrib/extraction/miniml.mli')
| -rw-r--r-- | contrib/extraction/miniml.mli | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 866ff847..7c18f9f5 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.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*) (*s Target language for extraction: a core ML called MiniML. *) @@ -35,7 +35,6 @@ type ml_type = | Tdummy | Tunknown | Taxiom - | Tcustom of string and ml_meta = { id : int; mutable contents : ml_type option } @@ -46,7 +45,11 @@ type ml_schema = int * ml_type (*s ML inductive types. *) -type inductive_info = Record | Singleton | Coinductive | Standard +type inductive_info = + | Singleton + | Coinductive + | Standard + | Record of global_reference list (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields @@ -79,8 +82,9 @@ type ml_ast = | MLlam of identifier * ml_ast | MLletin of identifier * ml_ast * ml_ast | MLglob of global_reference - | MLcons of global_reference * ml_ast list - | MLcase of ml_ast * (global_reference * identifier list * ml_ast) array + | MLcons of inductive_info * global_reference * ml_ast list + | MLcase of inductive_info * ml_ast * + (global_reference * identifier list * ml_ast) array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy |