diff options
| author | herbelin | 2001-07-02 22:31:43 +0000 |
|---|---|---|
| committer | herbelin | 2001-07-02 22:31:43 +0000 |
| commit | 9df7ef3bdd8288cb06888b7390441eae8d2c7aba (patch) | |
| tree | f98f182862cd74eba63db25ab44dcfebc27339e9 /proofs/proof_trees.ml | |
| 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 'proofs/proof_trees.ml')
| -rw-r--r-- | proofs/proof_trees.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 45fe9e5a47..8bfa53842c 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -354,8 +354,10 @@ let rec ast_of_cvt_intro_pattern = function | ListPat l -> ope ("LISTPATTERN", (List.map ast_of_cvt_intro_pattern l)) (* Gives the ast list corresponding to a reduction flag *) +open RedFlags + let last_of_cvt_flags (_,red) = - (if (red_set red BETA) then [ope("Beta",[])] + (if (red_set red fBETA) then [ope("Beta",[])] else [])@ (let (n_unf,lconst) = red_get_const red in let lqid = @@ -368,7 +370,7 @@ let last_of_cvt_flags (_,red) = if lqid = [] then [] else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)] else [ope("Delta",[]);ope("Unf",lqid)])@ - (if (red_set red IOTA) then [ope("Iota",[])] + (if (red_set red fIOTA) then [ope("Iota",[])] else []) (* Gives the ast corresponding to a reduction expression *) |