From 2ff58aa2c8592a5ce56815e10c8477f481ab25fd Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 20 Apr 2006 09:57:01 +0000 Subject: 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 --- contrib/extraction/mlutil.mli | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'contrib/extraction/mlutil.mli') 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. *) -- cgit v1.2.3