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 /proofs | |
| 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')
| -rw-r--r-- | proofs/proof_trees.ml | 6 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 21 |
2 files changed, 12 insertions, 15 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 45fe9e5a4..8bfa53842 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 *) diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index cb5395447..90bb5d805 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -10,6 +10,7 @@ open Astterm open Closure +open RedFlags open Declarations open Dyn open Libobject @@ -1110,7 +1111,7 @@ and cvt_fold (evc,env,lfun,lmatch,goalopt,debug) = function and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = let rec add_flag red = function | [] -> red - | Node(_,"Beta",[])::lf -> add_flag (red_add red BETA) lf + | Node(_,"Beta",[])::lf -> add_flag (red_add red fBETA) lf | Node(_,"Delta",[])::lf -> (match lf with | Node(loc,"Unf",l)::lf -> @@ -1119,8 +1120,8 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = (fun v red -> match glob_const_nvar loc env (qid_interp (evc,env,lfun,lmatch,goalopt,debug) v) with - | EvalVarRef id -> red_add red (VAR id) - | EvalConstRef sp -> red_add red (CONST [sp])) l red + | EvalVarRef id -> red_add red (fVAR id) + | EvalConstRef sp -> red_add red (fCONST sp)) l red in add_flag idl lf (* (id_of_Identifier (unvarg @@ -1133,18 +1134,12 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = (fun v red -> match glob_const_nvar loc env (qid_interp (evc,env,lfun,lmatch,goalopt,debug)v) with - | EvalVarRef id -> red_add red (VARBUT id) - | EvalConstRef sp -> red_add red (CONSTBUT [sp])) l red + | EvalVarRef id -> red_add red (fVARBUT id) + | EvalConstRef sp -> red_add red (fCONSTBUT sp)) l red in add_flag idl lf -(* - List.map - (fun v -> glob_const_nvar loc (id_of_Identifier (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l - in add_flag (red_add red (CONSTBUT idl)) lf -*) - | _ -> add_flag (red_add red DELTA) lf) - | Node(_,"Iota",[])::lf -> add_flag (red_add red IOTA) lf + | _ -> add_flag (red_add red fDELTA) lf) + | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf | Node(loc,("Unf"|"UnfBut"),l)::_ -> user_err_loc(loc,"flag_of_ast", [<'sTR "Delta must be specified just before">]) |