diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-20 09:57:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-20 09:57:01 +0000 |
| commit | 2ff58aa2c8592a5ce56815e10c8477f481ab25fd (patch) | |
| tree | 38aeeb28a6ef5131fb65286b4dedc23d23cc54ac /contrib/extraction/mlutil.mli | |
| parent | c5d686f2abee4f7d6376cfbdbc2d49c42c423c17 (diff) | |
decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8724 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/mlutil.mli')
| -rw-r--r-- | contrib/extraction/mlutil.mli | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index 05e773c5d..b5b47490e 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -62,13 +62,15 @@ val var2var' : ml_type -> ml_type type abbrev_map = global_reference -> ml_type option val type_expand : abbrev_map -> ml_type -> ml_type -val type_eq : abbrev_map -> ml_type -> ml_type -> bool -val type_neq : abbrev_map -> ml_type -> ml_type -> bool -val type_to_sign : abbrev_map -> ml_type -> bool list +val type_to_sign : abbrev_map -> ml_type -> sign +val type_to_signature : abbrev_map -> ml_type -> signature val type_expunge : abbrev_map -> ml_type -> ml_type -val case_expunge : bool list -> ml_ast -> identifier list * ml_ast -val term_expunge : bool list -> identifier list * ml_ast -> ml_ast +val isDummy : ml_type -> bool +val isKill : sign -> bool + +val case_expunge : signature -> ml_ast -> identifier list * ml_ast +val term_expunge : signature -> identifier list * ml_ast -> ml_ast (*s Special identifiers. [dummy_name] is to be used for dead code @@ -86,9 +88,9 @@ val collect_n_lams : int -> ml_ast -> identifier list * ml_ast val nb_lams : ml_ast -> int val dummy_lams : ml_ast -> int -> ml_ast -val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast +val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast -val eta_args_sign : int -> bool list -> ml_ast list +val eta_args_sign : int -> signature -> ml_ast list (*s Utility functions over ML terms. *) |