diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-02 22:31:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-02 22:31:43 +0000 |
| commit | 9df7ef3bdd8288cb06888b7390441eae8d2c7aba (patch) | |
| tree | f98f182862cd74eba63db25ab44dcfebc27339e9 /pretyping/cbv.mli | |
| parent | c25b393a7e121d2742375a3fb00776e5fb9d79da (diff) | |
Nettoyage/restructuration des ensembles d'indicateurs de réductions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cbv.mli')
| -rw-r--r-- | pretyping/cbv.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 778eebff7..7271a3c0b 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -46,6 +46,7 @@ val stack_app : cbv_value list -> cbv_stack -> cbv_stack val under_case_stack : cbv_stack -> bool val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack +open RedFlags val red_allowed : flags -> cbv_stack -> red_kind -> bool val reduce_const_body : (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack |