normalisation (by closure) was not performed under fixpoints

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9983 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 96 insertions, 101 deletions

diff --git a/.depend b/.depend
index f1d77c104..07c026a86 100644
--- a/.depend
+++ b/.depend
@@ -205,7 +205,7 @@ pretyping/pattern.cmi: kernel/term.cmi kernel/sign.cmi pretyping/rawterm.cmi \
 pretyping/pretype_errors.cmi: lib/util.cmi kernel/term.cmi kernel/sign.cmi \
     pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi \
     pretyping/inductiveops.cmi pretyping/evd.cmi kernel/environ.cmi 
-pretyping/pretyping.cmi: kernel/term.cmi kernel/sign.cmi \
+pretyping/pretyping.cmi: lib/util.cmi kernel/term.cmi kernel/sign.cmi \
     pretyping/rawterm.cmi kernel/names.cmi pretyping/evd.cmi \
     pretyping/evarutil.cmi kernel/environ.cmi lib/dyn.cmi \
     pretyping/coercion.cmi pretyping/cases.cmi 
@@ -492,7 +492,6 @@ contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi
 contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi 
 contrib/rtauto/refl_tauto.cmi: kernel/term.cmi proofs/tacmach.cmi \
     proofs/proof_type.cmi contrib/rtauto/proof_search.cmi kernel/names.cmi 
-contrib/subtac/context.cmi: kernel/term.cmi kernel/names.cmi 
 contrib/subtac/eterm.cmi: lib/util.cmi kernel/term.cmi proofs/tacmach.cmi \
     kernel/names.cmi pretyping/evd.cmi 
 contrib/subtac/subtac_cases.cmi: lib/util.cmi kernel/term.cmi \
@@ -505,11 +504,10 @@ contrib/subtac/subtac_command.cmi: toplevel/vernacexpr.cmo \
     kernel/names.cmi library/libnames.cmi pretyping/evd.cmi \
     kernel/environ.cmi interp/constrintern.cmi 
 contrib/subtac/subtac_errors.cmi: lib/util.cmi lib/pp.cmi 
-contrib/subtac/subtac_interp_fixpoint.cmi: lib/util.cmi interp/topconstr.cmi \
-    lib/pp.cmi kernel/names.cmi library/libnames.cmi 
 contrib/subtac/subtac.cmi: toplevel/vernacexpr.cmo lib/util.cmi 
 contrib/subtac/subtac_obligations.cmi: lib/util.cmi interp/topconstr.cmi \
-    kernel/term.cmi proofs/tacexpr.cmo proofs/proof_type.cmi kernel/names.cmi 
+    kernel/term.cmi proofs/tacexpr.cmo proofs/proof_type.cmi lib/pp.cmi \
+    kernel/names.cmi 
 contrib/subtac/subtac_pretyping.cmi: interp/topconstr.cmi kernel/term.cmi \
     kernel/sign.cmi pretyping/pretyping.cmi kernel/names.cmi \
     library/global.cmi pretyping/evd.cmi kernel/environ.cmi 
@@ -3660,39 +3658,35 @@ contrib/rtauto/refl_tauto.cmx: lib/util.cmx pretyping/termops.cmx \
     kernel/environ.cmx interp/coqlib.cmx kernel/closure.cmx \
     contrib/rtauto/refl_tauto.cmi 
 contrib/setoid_ring/newring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
-    pretyping/typing.cmi kernel/typeops.cmi interp/topconstr.cmi \
-    pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
-    tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \
-    proofs/tacexpr.cmo library/summary.cmi tactics/setoid_replace.cmi \
-    pretyping/retyping.cmi proofs/refiner.cmi pretyping/reductionops.cmi \
-    pretyping/rawterm.cmi contrib/ring/quote.cmo proofs/proof_type.cmi \
-    parsing/printer.cmi pretyping/pretyping.cmi parsing/pptactic.cmi \
-    lib/pp.cmi parsing/pcoq.cmi library/nametab.cmi kernel/names.cmi \
-    kernel/mod_subst.cmi library/libobject.cmi library/libnames.cmi \
-    library/lib.cmi parsing/lexer.cmi library/global.cmi interp/genarg.cmi \
-    pretyping/evd.cmi kernel/esubst.cmi kernel/environ.cmi kernel/entries.cmi \
+    pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \
+    kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
+    proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
+    library/summary.cmi tactics/setoid_replace.cmi pretyping/retyping.cmi \
+    proofs/refiner.cmi pretyping/reductionops.cmi pretyping/rawterm.cmi \
+    contrib/ring/quote.cmo proofs/proof_type.cmi parsing/printer.cmi \
+    pretyping/pretyping.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \
+    library/nametab.cmi kernel/names.cmi kernel/mod_subst.cmi \
+    library/libobject.cmi library/libnames.cmi library/lib.cmi \
+    parsing/lexer.cmi library/global.cmi interp/genarg.cmi pretyping/evd.cmi \
+    kernel/esubst.cmi kernel/environ.cmi kernel/entries.cmi \
     parsing/egrammar.cmi library/declare.cmi library/decl_kinds.cmo \
     interp/coqlib.cmi interp/constrintern.cmi kernel/closure.cmi \
     toplevel/cerrors.cmi 
 contrib/setoid_ring/newring.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
-    pretyping/typing.cmx kernel/typeops.cmx interp/topconstr.cmx \
-    pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
-    tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \
-    proofs/tacexpr.cmx library/summary.cmx tactics/setoid_replace.cmx \
-    pretyping/retyping.cmx proofs/refiner.cmx pretyping/reductionops.cmx \
-    pretyping/rawterm.cmx contrib/ring/quote.cmx proofs/proof_type.cmx \
-    parsing/printer.cmx pretyping/pretyping.cmx parsing/pptactic.cmx \
-    lib/pp.cmx parsing/pcoq.cmx library/nametab.cmx kernel/names.cmx \
-    kernel/mod_subst.cmx library/libobject.cmx library/libnames.cmx \
-    library/lib.cmx parsing/lexer.cmx library/global.cmx interp/genarg.cmx \
-    pretyping/evd.cmx kernel/esubst.cmx kernel/environ.cmx kernel/entries.cmx \
+    pretyping/typing.cmx interp/topconstr.cmx pretyping/termops.cmx \
+    kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \
+    proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
+    library/summary.cmx tactics/setoid_replace.cmx pretyping/retyping.cmx \
+    proofs/refiner.cmx pretyping/reductionops.cmx pretyping/rawterm.cmx \
+    contrib/ring/quote.cmx proofs/proof_type.cmx parsing/printer.cmx \
+    pretyping/pretyping.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
+    library/nametab.cmx kernel/names.cmx kernel/mod_subst.cmx \
+    library/libobject.cmx library/libnames.cmx library/lib.cmx \
+    parsing/lexer.cmx library/global.cmx interp/genarg.cmx pretyping/evd.cmx \
+    kernel/esubst.cmx kernel/environ.cmx kernel/entries.cmx \
     parsing/egrammar.cmx library/declare.cmx library/decl_kinds.cmx \
     interp/coqlib.cmx interp/constrintern.cmx kernel/closure.cmx \
     toplevel/cerrors.cmx 
-contrib/subtac/context.cmo: kernel/term.cmi kernel/names.cmi \
-    contrib/subtac/context.cmi 
-contrib/subtac/context.cmx: kernel/term.cmx kernel/names.cmx \
-    contrib/subtac/context.cmi 
 contrib/subtac/eterm.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tacticals.cmi contrib/subtac/subtac_utils.cmi lib/pp.cmi \
     lib/options.cmi kernel/names.cmi library/global.cmi pretyping/evd.cmi \
@@ -3751,8 +3745,8 @@ contrib/subtac/subtac_coercion.cmo: lib/util.cmi pretyping/typing.cmi \
     pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
     library/nameops.cmi library/global.cmi pretyping/evd.cmi \
     pretyping/evarutil.cmi pretyping/evarconv.cmi contrib/subtac/eterm.cmi \
-    kernel/environ.cmi interp/coqlib.cmi contrib/subtac/context.cmi \
-    pretyping/classops.cmi contrib/subtac/subtac_coercion.cmi 
+    kernel/environ.cmi interp/coqlib.cmi pretyping/classops.cmi \
+    contrib/subtac/subtac_coercion.cmi 
 contrib/subtac/subtac_coercion.cmx: lib/util.cmx pretyping/typing.cmx \
     kernel/typeops.cmx pretyping/termops.cmx kernel/term.cmx \
     contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_errors.cmx \
@@ -3761,8 +3755,8 @@ contrib/subtac/subtac_coercion.cmx: lib/util.cmx pretyping/typing.cmx \
     pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
     library/nameops.cmx library/global.cmx pretyping/evd.cmx \
     pretyping/evarutil.cmx pretyping/evarconv.cmx contrib/subtac/eterm.cmx \
-    kernel/environ.cmx interp/coqlib.cmx contrib/subtac/context.cmx \
-    pretyping/classops.cmx contrib/subtac/subtac_coercion.cmi 
+    kernel/environ.cmx interp/coqlib.cmx pretyping/classops.cmx \
+    contrib/subtac/subtac_coercion.cmi 
 contrib/subtac/subtac_command.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
@@ -3805,30 +3799,6 @@ contrib/subtac/subtac_errors.cmo: lib/util.cmi parsing/printer.cmi lib/pp.cmi \
     contrib/subtac/subtac_errors.cmi 
 contrib/subtac/subtac_errors.cmx: lib/util.cmx parsing/printer.cmx lib/pp.cmx \
     contrib/subtac/subtac_errors.cmi 
-contrib/subtac/subtac_interp_fixpoint.cmo: lib/util.cmi kernel/typeops.cmi \
-    kernel/type_errors.cmi interp/topconstr.cmi pretyping/termops.cmi \
-    kernel/term.cmi contrib/subtac/subtac_utils.cmi \
-    contrib/subtac/subtac_errors.cmi contrib/subtac/subtac_coercion.cmi \
-    kernel/sign.cmi pretyping/reductionops.cmi pretyping/recordops.cmi \
-    pretyping/rawterm.cmi parsing/printer.cmi pretyping/pretype_errors.cmi \
-    parsing/ppconstr.cmi lib/pp.cmi pretyping/pattern.cmi kernel/names.cmi \
-    library/nameops.cmi library/libnames.cmi library/global.cmi \
-    pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \
-    contrib/subtac/eterm.cmi kernel/environ.cmi lib/dyn.cmi interp/coqlib.cmi \
-    contrib/subtac/context.cmi pretyping/classops.cmi \
-    contrib/subtac/subtac_interp_fixpoint.cmi 
-contrib/subtac/subtac_interp_fixpoint.cmx: lib/util.cmx kernel/typeops.cmx \
-    kernel/type_errors.cmx interp/topconstr.cmx pretyping/termops.cmx \
-    kernel/term.cmx contrib/subtac/subtac_utils.cmx \
-    contrib/subtac/subtac_errors.cmx contrib/subtac/subtac_coercion.cmx \
-    kernel/sign.cmx pretyping/reductionops.cmx pretyping/recordops.cmx \
-    pretyping/rawterm.cmx parsing/printer.cmx pretyping/pretype_errors.cmx \
-    parsing/ppconstr.cmx lib/pp.cmx pretyping/pattern.cmx kernel/names.cmx \
-    library/nameops.cmx library/libnames.cmx library/global.cmx \
-    pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \
-    contrib/subtac/eterm.cmx kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \
-    contrib/subtac/context.cmx pretyping/classops.cmx \
-    contrib/subtac/subtac_interp_fixpoint.cmi 
 contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi kernel/type_errors.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
@@ -3843,9 +3813,8 @@ contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
     pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
     lib/dyn.cmi pretyping/detyping.cmi library/decl_kinds.cmo \
-    interp/coqlib.cmi contrib/subtac/context.cmi toplevel/command.cmi \
-    pretyping/classops.cmi toplevel/cerrors.cmi pretyping/cases.cmi \
-    contrib/subtac/subtac.cmi 
+    interp/coqlib.cmi toplevel/command.cmi pretyping/classops.cmi \
+    toplevel/cerrors.cmi pretyping/cases.cmi contrib/subtac/subtac.cmi 
 contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     kernel/typeops.cmx kernel/type_errors.cmx pretyping/termops.cmx \
     kernel/term.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
@@ -3860,29 +3829,26 @@ contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
     pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
     lib/dyn.cmx pretyping/detyping.cmx library/decl_kinds.cmx \
-    interp/coqlib.cmx contrib/subtac/context.cmx toplevel/command.cmx \
-    pretyping/classops.cmx toplevel/cerrors.cmx pretyping/cases.cmx \
-    contrib/subtac/subtac.cmi 
-contrib/subtac/subtac_obligations.cmo: lib/util.cmi pretyping/termops.cmi \
-    kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
-    library/summary.cmi contrib/subtac/subtac_utils.cmi proofs/refiner.cmi \
+    interp/coqlib.cmx toplevel/command.cmx pretyping/classops.cmx \
+    toplevel/cerrors.cmx pretyping/cases.cmx contrib/subtac/subtac.cmi 
+contrib/subtac/subtac_obligations.cmo: lib/util.cmi kernel/term.cmi \
+    tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \
+    contrib/subtac/subtac_utils.cmi proofs/refiner.cmi \
     pretyping/reductionops.cmi proofs/proof_type.cmi parsing/ppconstr.cmi \
     lib/pp.cmi proofs/pfedit.cmi lib/options.cmi kernel/names.cmi \
     library/libobject.cmi library/libnames.cmi library/lib.cmi \
-    library/global.cmi pretyping/evd.cmi kernel/environ.cmi \
-    kernel/entries.cmi library/declare.cmi library/decl_kinds.cmo \
-    toplevel/command.cmi tactics/auto.cmi \
-    contrib/subtac/subtac_obligations.cmi 
-contrib/subtac/subtac_obligations.cmx: lib/util.cmx pretyping/termops.cmx \
-    kernel/term.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
-    library/summary.cmx contrib/subtac/subtac_utils.cmx proofs/refiner.cmx \
+    library/global.cmi pretyping/evd.cmi kernel/entries.cmi \
+    library/declare.cmi library/decl_kinds.cmo toplevel/command.cmi \
+    tactics/auto.cmi contrib/subtac/subtac_obligations.cmi 
+contrib/subtac/subtac_obligations.cmx: lib/util.cmx kernel/term.cmx \
+    tactics/tacinterp.cmx proofs/tacexpr.cmx library/summary.cmx \
+    contrib/subtac/subtac_utils.cmx proofs/refiner.cmx \
     pretyping/reductionops.cmx proofs/proof_type.cmx parsing/ppconstr.cmx \
     lib/pp.cmx proofs/pfedit.cmx lib/options.cmx kernel/names.cmx \
     library/libobject.cmx library/libnames.cmx library/lib.cmx \
-    library/global.cmx pretyping/evd.cmx kernel/environ.cmx \
-    kernel/entries.cmx library/declare.cmx library/decl_kinds.cmx \
-    toplevel/command.cmx tactics/auto.cmx \
-    contrib/subtac/subtac_obligations.cmi 
+    library/global.cmx pretyping/evd.cmx kernel/entries.cmx \
+    library/declare.cmx library/decl_kinds.cmx toplevel/command.cmx \
+    tactics/auto.cmx contrib/subtac/subtac_obligations.cmi 
 contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
     contrib/subtac/subtac_cases.cmi kernel/sign.cmi pretyping/retyping.cmi \
@@ -3914,9 +3880,9 @@ contrib/subtac/subtac_pretyping.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \
     library/libnames.cmi library/global.cmi pretyping/evd.cmi \
     pretyping/evarutil.cmi pretyping/evarconv.cmi contrib/subtac/eterm.cmi \
-    kernel/environ.cmi lib/dyn.cmi interp/coqlib.cmi \
-    contrib/subtac/context.cmi interp/constrintern.cmi toplevel/command.cmi \
-    pretyping/classops.cmi contrib/subtac/subtac_pretyping.cmi 
+    kernel/environ.cmi lib/dyn.cmi interp/coqlib.cmi interp/constrintern.cmi \
+    toplevel/command.cmi pretyping/classops.cmi \
+    contrib/subtac/subtac_pretyping.cmi 
 contrib/subtac/subtac_pretyping.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     kernel/typeops.cmx kernel/type_errors.cmx interp/topconstr.cmx \
     pretyping/termops.cmx kernel/term.cmx contrib/subtac/subtac_utils.cmx \
@@ -3928,9 +3894,9 @@ contrib/subtac/subtac_pretyping.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \
     library/libnames.cmx library/global.cmx pretyping/evd.cmx \
     pretyping/evarutil.cmx pretyping/evarconv.cmx contrib/subtac/eterm.cmx \
-    kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \
-    contrib/subtac/context.cmx interp/constrintern.cmx toplevel/command.cmx \
-    pretyping/classops.cmx contrib/subtac/subtac_pretyping.cmi 
+    kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx interp/constrintern.cmx \
+    toplevel/command.cmx pretyping/classops.cmx \
+    contrib/subtac/subtac_pretyping.cmi 
 contrib/subtac/subtac_utils.cmo: lib/util.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
     tactics/tacticals.cmi proofs/tacexpr.cmo kernel/reduction.cmi \
@@ -4204,14 +4170,34 @@ tools/coq_makefile.cmx:
 tools/coq-tex.cmo: 
 tools/coq-tex.cmx: 
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \
+  /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \
+  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \
+  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
+  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
+  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/int64_emul.h
+  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
+  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
+  kernel/byterun/int64_native.h kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
+  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
+  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h kernel/byterun/coq_interp.h
+  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
+  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_interp.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
+  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
+  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  kernel/byterun/coq_values.h
+  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \
+  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/caml/alloc.h
diff --git a/.depend.coq b/.depend.coq
index 570d02f2d..4b1a57b32 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -363,8 +363,8 @@ theories/Ints/num/GenDiv.vo: theories/Ints/num/GenDiv.v theories/ZArith/ZArith.v
 theories/Ints/num/GenSqrt.vo: theories/Ints/num/GenSqrt.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
 theories/Ints/num/GenLift.vo: theories/Ints/num/GenLift.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/Zmod.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
 theories/Ints/num/Zn2Z.vo: theories/Ints/num/Zn2Z.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenSqrt.vo theories/Ints/num/GenLift.vo theories/Ints/num/GenDivn1.vo theories/Ints/num/GenDiv.vo theories/Ints/num/ZnZ.vo
-theories/Ints/num/Nbasic.vo: theories/Ints/num/Nbasic.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo
-theories/Ints/num/NMake.vo: theories/Ints/num/NMake.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo theories/Ints/num/ZnZ.vo theories/Ints/num/Zn2Z.vo theories/Ints/num/Nbasic.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenDivn1.vo
+theories/Ints/num/Nbasic.vo: theories/Ints/num/Nbasic.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Arith/Max.vo
+theories/Ints/num/NMake.vo: theories/Ints/num/NMake.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo theories/Ints/num/ZnZ.vo theories/Ints/num/Zn2Z.vo theories/Ints/num/Nbasic.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenDivn1.vo theories/Arith/Wf_nat.vo
 theories/Ints/BigN.vo: theories/Ints/BigN.v theories/Ints/Int31.vo theories/Ints/num/NMake.vo theories/Ints/num/ZnZ.vo
 theories/Ints/num/ZMake.vo: theories/Ints/num/ZMake.v theories/ZArith/ZArith.vo
 theories/Ints/BigZ.vo: theories/Ints/BigZ.v theories/Ints/BigN.vo theories/Ints/num/ZMake.vo
diff --git a/contrib/setoid_ring/Ring_zdiv.v b/contrib/setoid_ring/Ring_zdiv.v
index 10141b6b4..9b102c28c 100644
--- a/contrib/setoid_ring/Ring_zdiv.v
+++ b/contrib/setoid_ring/Ring_zdiv.v
@@ -66,7 +66,7 @@ Ltac ztac := repeat (rewrite Zmult_plus_distr_l ||
 
 Theorem pdiv_eucl_correct: forall a b,
   let (q,r) := pdiv_eucl a b in Zpos a = (Z_of_N q * Zpos b + Z_of_N r)%Z.
-induction a; unfold pdiv_eucl; fold pdiv_eucl.
+induction a; cbv beta iota delta [pdiv_eucl]; fold pdiv_eucl; cbv zeta.
   intros b; generalize (IHa b); case pdiv_eucl.
     intros q1 r1 Hq1.
      generalize (Ngeb_correct (2 * r1 + 1) b); case Ngeb; intros H.
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 364475019..01d31441d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -980,7 +980,7 @@ and knht e t stk =
 
 (************************************************************************)
 
-(* Computes a normal form from the result of knh. *)
+(* Computes a weak head normal form from the result of knh. *)
 let rec knr info m stk =
   match m.term with
   | FLambda(n,tys,f,e) when red_set info.i_flags fBETA ->
@@ -1082,6 +1082,11 @@ and norm_head info m =
           let fbds =
             Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
           mkCoFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds))
+      | FFix((n,(na,tys,bds)),e) ->
+          let ftys = Array.map (mk_clos e) tys in
+          let fbds =
+            Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
+          mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds))
       | FEvar(i,args) -> mkEvar(i, Array.map (kl info) args)
       | t -> term_of_fconstr m
 
diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v
index 34b3b35e0..f404c9243 100644
--- a/theories/Ints/num/GenDivn1.v
+++ b/theories/Ints/num/GenDivn1.v
@@ -99,7 +99,7 @@ Section GENDIVN1.
   Proof.
    induction n;intros.
    exact (spec_div21 a b2p_le H).
-   unfold gen_divn1_0, gen_divn1_0_aux;fold gen_divn1_0.
+   simpl (gen_divn1_0 (S n) r a); unfold gen_divn1_0_aux.
    assert (H1 := spec_split n a);destruct (gen_split w_0 n a) as (hh,hl).
    rewrite H1.
    assert (H2 := IHn r hh H);destruct (gen_divn1_0 n r hh) as (qh,rh).
@@ -180,10 +180,12 @@ Section GENDIVN1.
   Proof.
    case (spec_to_Z p); intros HH0 HH1.
    induction n;intros.
-   unfold gen_divn1_p, gen_divn1_p_aux, gen_to_Z, gen_wB, gen_digits.
+   simpl (gen_divn1_p 0 r h l).
+   unfold gen_to_Z, gen_wB, gen_digits.
    rewrite <- spec_add_mul_divp.
    exact (spec_div21 (w_add_mul_div p h l) b2p_le H).
-   unfold gen_divn1_p,gen_divn1_p_aux;fold gen_divn1_p.
+   simpl (gen_divn1_p (S n) r h l).
+   unfold gen_divn1_p_aux.
    assert (H1 := spec_split n h);destruct (gen_split w_0 n h) as (hh,hl).
    rewrite H1. rewrite <- gen_wB_wwB.
    assert (H2 := spec_split n l);destruct (gen_split w_0 n l) as (lh,ll).
@@ -333,7 +335,7 @@ Section GENDIVN1.
   auto with zarith.
   assert (U0 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w0);
    assert (U1 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w1).
-  unfold gen_to_Z,zn2z_to_Z;fold (gen_to_Z w_digits w_to_Z).
+  simpl [!S n|WW w0 w1!].
   unfold gen_wB,base;rewrite Zdiv_shift_r;auto with zarith.
   replace (2 ^ (Zpos (gen_digits w_digits (S n)) - Zpos w_digits)) with
    (2^(Zpos (gen_digits w_digits n) - Zpos w_digits) * 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index d168b0369..f9601b09a 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(* Contribution by Claude Marché and Xavier Urbain *)
+(* Contribution by Claude Marché and Xavier Urbain *)
 
 (** Euclidean Division
 
@@ -129,7 +129,8 @@ Lemma Z_div_mod_POS :
     forall a:positive,
       let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b.
 Proof.
-simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *.
+simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *;
+  fold Zdiv_eucl_POS in |- *; cbv zeta.
 
 intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1].
 generalize (Zgt_cases b (2 * r + 1)).
@@ -238,7 +239,8 @@ Qed.
 Lemma Z_div_POS_ge0 :
   forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0.
 Proof.
-  simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *.
+  simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *;
+    fold Zdiv_eucl_POS in |- *; cbv zeta.
   intro p; case (Zdiv_eucl_POS p b).
   intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega.
   intro p; case (Zdiv_eucl_POS p b).