diff options
author | 2012-12-21 21:47:38 +0000 | |
---|---|---|
committer | 2012-12-21 21:47:38 +0000 | |
commit | e9428d3127ca159451437c2abbc6306e0c31f513 (patch) | |
tree | 675eadf0e2790ae2dbe6f378dabf5a77feaec6f4 /tactics/tacsubst.ml | |
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 'tactics/tacsubst.ml')
-rw-r--r-- | tactics/tacsubst.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index bbf4089ed..007ec9c6f 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -117,6 +117,7 @@ let subst_redexp subst = function | Unfold l -> Unfold (List.map (subst_unfold subst) l) | Fold l -> Fold (List.map (subst_glob_constr subst) l) | Cbv f -> Cbv (subst_flag subst f) + | Cbn f -> Cbn (subst_flag subst f) | Lazy f -> Lazy (subst_flag subst f) | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l) | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o) |