aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authormsozeau2010-03-15 19:55:35 +0000
committermsozeau2010-03-15 19:55:35 +0000
commite42d29bb54eb3c07c79410e2c222d9f35b7905c1 (patch)
tree5883e415fbc88e9c338fc13b436d38342914f0e6 /plugins
parenta9d792a0cd482ad07e8b8f5e14af705e24a86203 (diff)
Oops, don't use zeta by default.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12869 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r--plugins/subtac/subtac_obligations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index e0ba212c53..24c5a1266d 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -22,7 +22,7 @@ let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
let reduce c =
- Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty c
+ Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c
exception NoObligations of identifier option