diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-21 21:47:38 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-21 21:47:38 +0000 |
| commit | e9428d3127ca159451437c2abbc6306e0c31f513 (patch) | |
| tree | 675eadf0e2790ae2dbe6f378dabf5a77feaec6f4 /grammar | |
| parent | 99674e1e719cede1531ff4c3e21c57cfb6b55b48 (diff) | |
Yet a new reduction tactic in Coq : cbn
It is supposed to become the next generation of the simpl tactics (it "refolds" constant)
but
1/it is a bit more aggresive than the old simpl
2/it cannot be customized as simpl start to be
3/(for now)it does not refold in reccursive calls constant such as
compare x y := compare_cont x y Eq := (fix compare_cont x y s := ...) x y Eq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16111 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 738c3e1f1..ec1471730 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -182,6 +182,8 @@ let mlexpr_of_red_expr = function | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >> | Genredexpr.Cbv f -> <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >> + | Genredexpr.Cbn f -> + <:expr< Genredexpr.Cbn $mlexpr_of_red_flags f$ >> | Genredexpr.Lazy f -> <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >> | Genredexpr.Unfold l -> |