diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-02 22:58:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-02 22:58:59 +0000 |
| commit | 97a5868bd73300793f25d6b13ea8c7536003c171 (patch) | |
| tree | 54816e6f37369922ce223b1d8a1a1b144e4e204c /parsing | |
| parent | 9df7ef3bdd8288cb06888b7390441eae8d2c7aba (diff) | |
Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute, nouveaux flags utilisateurs pour Evar et Zeta
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1820 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
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)) >> |