diff options
| author | Pierre-Marie Pédrot | 2015-12-15 10:30:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-15 10:38:52 +0100 |
| commit | db282f831cbf619e417593c602de24960c3ca69c (patch) | |
| tree | 6f4bcc1830e37713c571e58084214571c8920ff1 /plugins/extraction/mlutil.mli | |
| parent | f439001caa24671d03d8816964ceb8e483660e70 (diff) | |
| parent | ce395ca02311bbe6ecc1b2782e74312272dd15ec (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 0a71d2c838..c380dfb3e3 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -67,7 +67,8 @@ val type_expunge : abbrev_map -> ml_type -> ml_type val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type val eq_ml_type : ml_type -> ml_type -> bool -val isDummy : ml_type -> bool +val isTdummy : ml_type -> bool +val isMLdummy : ml_ast -> bool val isKill : sign -> bool val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast @@ -125,8 +126,8 @@ exception Impossible type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) val sign_kind : signature -> sign_kind |