diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:46 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:46 +0000 |
| commit | 056c7c4c33ca20c3185f09fedb9e963cd440907b (patch) | |
| tree | ac9191aa6936eb8fee91658a658a4241b818d10b | |
| parent | eeb75da21bedfdaa5fe975edc62aeb93b7c849b8 (diff) | |
Refine now does iota reduction in addition to beta.
Restores more compatibility with the earlier implementation of refine. Needed in ssreflect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17023 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c933ec44e..0bf295b3c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3880,7 +3880,7 @@ module New = struct Proofview.Goal.lift c >>= fun c -> Proofview.tclSENSITIVE (Goal.refine c) <*> Proofview.V82.tactic (reduce - (Lazy {rBeta=true;rIota=false;rZeta=false;rDelta=false;rConst=[]}) + (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) {onhyps=None; concl_occs=AllOccurrences } ) |