diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 2 |
3 files changed, 7 insertions, 1 deletions
@@ -7,6 +7,8 @@ Modifications depuis la V7.0 - Prise en compte des qualid dans Decompose - Correction bug inférence type Cases en présence de K-rédex - Correction bugs Cases en cas de prédicat dépendant +- Le flag Delta n'inclut plus Zeta et Evar, nouveaux flags Zeta et Evar inclus + dans Compute (à documenter) Différences V7.0beta / V7.0 - Portage de Correctness diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c374f5955..d8c4ecf08 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -197,6 +197,8 @@ GEXTEND Gram [ [ IDENT "Beta" -> <:ast< (Beta) >> | IDENT "Delta" -> <:ast< (Delta) >> | IDENT "Iota" -> <:ast< (Iota) >> + | IDENT "Zeta" -> <:ast< (Zeta) >> + | IDENT "Evar" -> <:ast< (Evar) >> | "["; idl = ne_qualidarg_list; "]" -> <:ast< (Unf ($LIST idl)) >> | "-"; "["; idl = ne_qualidarg_list; "]" -> <:ast< (UnfBut ($LIST idl)) >> ] ] @@ -207,7 +209,7 @@ GEXTEND Gram | IDENT "Simpl" -> <:ast< (Simpl) >> | IDENT "Cbv"; s = LIST1 red_flag -> <:ast< (Cbv ($LIST s)) >> | IDENT "Lazy"; s = LIST1 red_flag -> <:ast< (Lazy ($LIST s)) >> - | IDENT "Compute" -> <:ast< (Cbv (Beta) (Delta) (Iota)) >> + | IDENT "Compute" -> <:ast< (Cbv (Beta) (Delta) (Evar) (Iota) (Zeta)) >> | IDENT "Unfold"; ul = ne_unfold_occ_list -> <:ast< (Unfold ($LIST ul)) >> | IDENT "Fold"; cl = constrarg_list -> <:ast< (Fold ($LIST cl)) >> diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 90bb5d805..f2b92ae96 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -1140,6 +1140,8 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = | _ -> add_flag (red_add red fDELTA) lf) | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf + | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf + | Node(_,"Evar",[])::lf -> add_flag (red_add red fEVAR) lf | Node(loc,("Unf"|"UnfBut"),l)::_ -> user_err_loc(loc,"flag_of_ast", [<'sTR "Delta must be specified just before">]) |