Browse files

cbn can be called by Eval

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16353 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent bba4a5f commit 0eda7a25209b2ced8fb50ca0c12ed1f53e5eedae @pirbo pirbo committed Mar 25, 2013
Showing with 1 addition and 0 deletions.
  1. +1 −0 parsing/g_tactic.ml4
View
1 parsing/g_tactic.ml4
@@ -357,6 +357,7 @@ GEXTEND Gram
| IDENT "hnf" -> Hnf
| IDENT "simpl"; po = OPT pattern_occ -> Simpl po
| IDENT "cbv"; s = strategy_flag -> Cbv s
+ | IDENT "cbn"; s = strategy_flag -> Cbn s
| IDENT "lazy"; s = strategy_flag -> Lazy s
| IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
| IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po

0 comments on commit 0eda7a2

Please sign in to comment.