aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2001-10-22 16:19:42 +0000
committerletouzey2001-10-22 16:19:42 +0000
commita5b3d9a4486c176d76926d824f2386988d3edd7b (patch)
treebc19e09ee576fa77af9d1e64e2124cc1298fee21
parent115a337d250da743c136dfed77b03c69109f2517 (diff)
chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les options
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend358
-rw-r--r--Makefile4
-rw-r--r--contrib/extraction/Extraction.v39
-rw-r--r--contrib/extraction/extract_env.ml69
-rw-r--r--contrib/extraction/extraction.ml3
-rw-r--r--contrib/extraction/haskell.ml27
-rw-r--r--contrib/extraction/haskell.mli2
-rw-r--r--contrib/extraction/miniml.mli3
-rw-r--r--contrib/extraction/mlutil.ml281
-rw-r--r--contrib/extraction/mlutil.mli31
-rw-r--r--contrib/extraction/ocaml.ml35
-rw-r--r--contrib/extraction/ocaml.mli2
-rw-r--r--contrib/extraction/table.ml203
-rw-r--r--contrib/extraction/table.mli49
-rw-r--r--contrib/extraction/test/addReals2
15 files changed, 599 insertions, 509 deletions
diff --git a/.depend b/.depend
index 063e3d17ee..38e8507dab 100644
--- a/.depend
+++ b/.depend
@@ -29,10 +29,12 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
lib/pp.cmi: lib/pp_control.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
- kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
- library/libobject.cmi library/library.cmi kernel/names.cmi \
- library/nametab.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
+ kernel/environ.cmi kernel/inductive.cmi library/libobject.cmi \
+ library/library.cmi kernel/names.cmi library/nametab.cmi kernel/sign.cmi \
+ kernel/term.cmi kernel/univ.cmi
library/global.cmi: kernel/cooking.cmi kernel/declarations.cmi \
kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \
@@ -46,12 +48,10 @@ library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi
library/libobject.cmi: kernel/names.cmi
library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \
library/nametab.cmi lib/pp.cmi lib/system.cmi
-library/nametab.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi lib/util.cmi
+library/nametab.cmi: kernel/names.cmi lib/pp.cmi lib/util.cmi
library/opaque.cmi: kernel/closure.cmi kernel/environ.cmi kernel/names.cmi \
kernel/safe_typing.cmi
library/summary.cmi: kernel/names.cmi
-lib/system.cmi: lib/pp.cmi
-lib/util.cmi: lib/pp.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
parsing/pcoq.cmi lib/pp.cmi
parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -70,9 +70,10 @@ parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
kernel/term.cmi
parsing/g_zsyntax.cmi: parsing/coqast.cmi
parsing/pcoq.cmi: parsing/coqast.cmi
-parsing/prettyp.cmi: kernel/environ.cmi kernel/inductive.cmi library/lib.cmi \
- kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/reduction.cmi \
- kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi
+parsing/prettyp.cmi: pretyping/classops.cmi kernel/environ.cmi \
+ kernel/inductive.cmi library/lib.cmi kernel/names.cmi library/nametab.cmi \
+ lib/pp.cmi kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+ kernel/term.cmi
parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \
kernel/term.cmi
@@ -119,8 +120,8 @@ pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
kernel/names.cmi kernel/reduction.cmi kernel/term.cmi
pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi
proofs/clenv.cmi: kernel/environ.cmi proofs/evar_refiner.cmi kernel/evd.cmi \
- kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
- kernel/term.cmi lib/util.cmi
+ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ proofs/tacmach.cmi kernel/term.cmi lib/util.cmi
proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
kernel/names.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi
@@ -187,8 +188,8 @@ toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \
kernel/names.cmi kernel/term.cmi
toplevel/command.cmi: parsing/coqast.cmi kernel/declarations.cmi \
library/declare.cmi kernel/environ.cmi library/library.cmi \
- kernel/names.cmi proofs/proof_type.cmi pretyping/tacred.cmi \
- kernel/term.cmi
+ kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \
+ pretyping/tacred.cmi kernel/term.cmi
toplevel/coqinit.cmi: kernel/names.cmi
toplevel/discharge.cmi: kernel/names.cmi
toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi
@@ -202,23 +203,22 @@ toplevel/mltop.cmi: library/libobject.cmi kernel/names.cmi
toplevel/protectedtoplevel.cmi: lib/pp.cmi
toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/sign.cmi \
kernel/term.cmi
-toplevel/recordobj.cmi: kernel/term.cmi
+toplevel/recordobj.cmi: kernel/names.cmi
toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
kernel/term.cmi
toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi
-toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \
- kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \
- kernel/term.cmi toplevel/vernacinterp.cmi
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi
+toplevel/vernacentries.cmi: kernel/environ.cmi kernel/names.cmi \
+ proofs/proof_type.cmi kernel/term.cmi toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
library/nametab.cmi proofs/proof_type.cmi
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi
contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \
contrib/correctness/ptype.cmi kernel/term.cmi
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+ pretyping/rawterm.cmi
contrib/correctness/pcicenv.cmi: kernel/names.cmi \
contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
kernel/sign.cmi kernel/term.cmi
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
- pretyping/rawterm.cmi
contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
contrib/correctness/ptype.cmi
contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi
@@ -259,12 +259,14 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \
contrib/extraction/extraction.cmi: kernel/environ.cmi \
contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi
contrib/extraction/haskell.cmi: contrib/extraction/miniml.cmi \
- contrib/extraction/mlutil.cmi kernel/term.cmi
+ contrib/extraction/mlutil.cmi kernel/names.cmi
contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi
contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
kernel/term.cmi
contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi
+contrib/extraction/table.cmi: library/goptions.cmi kernel/names.cmi \
+ library/summary.cmi toplevel/vernacinterp.cmi
contrib/interface/dad.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \
proofs/tacmach.cmi
contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
@@ -330,12 +332,12 @@ kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
kernel/evd.cmi
kernel/indtypes.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/evd.cmi kernel/inductive.cmi kernel/instantiate.cmi \
- kernel/names.cmi lib/options.cmi kernel/reduction.cmi kernel/sign.cmi \
- kernel/term.cmi kernel/typeops.cmi lib/util.cmi kernel/indtypes.cmi
+ kernel/names.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/typeops.cmi lib/util.cmi kernel/indtypes.cmi
kernel/indtypes.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/evd.cmx kernel/inductive.cmx kernel/instantiate.cmx \
- kernel/names.cmx lib/options.cmx kernel/reduction.cmx kernel/sign.cmx \
- kernel/term.cmx kernel/typeops.cmx lib/util.cmx kernel/indtypes.cmi
+ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/typeops.cmx lib/util.cmx kernel/indtypes.cmi
kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/names.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
kernel/univ.cmi lib/util.cmi kernel/inductive.cmi
@@ -343,11 +345,11 @@ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/univ.cmx lib/util.cmx kernel/inductive.cmi
kernel/instantiate.cmo: kernel/declarations.cmi kernel/environ.cmi \
- kernel/evd.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
- kernel/sign.cmi kernel/term.cmi lib/util.cmi kernel/instantiate.cmi
+ kernel/evd.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+ kernel/term.cmi lib/util.cmi kernel/instantiate.cmi
kernel/instantiate.cmx: kernel/declarations.cmx kernel/environ.cmx \
- kernel/evd.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
- kernel/sign.cmx kernel/term.cmx lib/util.cmx kernel/instantiate.cmi
+ kernel/evd.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
+ kernel/term.cmx lib/util.cmx kernel/instantiate.cmi
kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
kernel/names.cmi
kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
@@ -362,20 +364,18 @@ kernel/reduction.cmx: kernel/closure.cmx kernel/declarations.cmx \
kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/reduction.cmi
kernel/safe_typing.cmo: kernel/cooking.cmi kernel/declarations.cmi \
kernel/environ.cmi kernel/evd.cmi kernel/indtypes.cmi \
- kernel/inductive.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
- kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
- kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
- kernel/safe_typing.cmi
+ kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/safe_typing.cmi
kernel/safe_typing.cmx: kernel/cooking.cmx kernel/declarations.cmx \
kernel/environ.cmx kernel/evd.cmx kernel/indtypes.cmx \
- kernel/inductive.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
- kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
- kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
- kernel/safe_typing.cmi
-kernel/sign.cmo: kernel/names.cmi lib/options.cmi kernel/term.cmi \
- lib/util.cmi kernel/sign.cmi
-kernel/sign.cmx: kernel/names.cmx lib/options.cmx kernel/term.cmx \
- lib/util.cmx kernel/sign.cmi
+ kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/safe_typing.cmi
+kernel/sign.cmo: kernel/names.cmi kernel/term.cmi lib/util.cmi \
+ kernel/sign.cmi
+kernel/sign.cmx: kernel/names.cmx kernel/term.cmx lib/util.cmx \
+ kernel/sign.cmi
kernel/term.cmo: kernel/esubst.cmi lib/hashcons.cmi kernel/names.cmi \
lib/pp.cmi kernel/univ.cmi lib/util.cmi kernel/term.cmi
kernel/term.cmx: kernel/esubst.cmx lib/hashcons.cmx kernel/names.cmx \
@@ -408,24 +408,32 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
lib/explore.cmo: lib/explore.cmi
lib/explore.cmx: lib/explore.cmi
-lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
-lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
lib/gmap.cmo: lib/gmap.cmi
lib/gmap.cmx: lib/gmap.cmi
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
lib/gset.cmo: lib/gset.cmi
lib/gset.cmx: lib/gset.cmi
lib/hashcons.cmo: lib/hashcons.cmi
lib/hashcons.cmx: lib/hashcons.cmi
lib/options.cmo: lib/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.cmi
-lib/pp_control.cmo: lib/pp_control.cmi
-lib/pp_control.cmx: lib/pp_control.cmi
lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
+lib/pp_control.cmo: lib/pp_control.cmi
+lib/pp_control.cmx: lib/pp_control.cmi
lib/predicate.cmo: lib/predicate.cmi
lib/predicate.cmx: lib/predicate.cmi
lib/profile.cmo: lib/profile.cmi
lib/profile.cmx: lib/profile.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/util.cmi
library/declare.cmo: kernel/cooking.cmi kernel/declarations.cmi \
kernel/environ.cmi kernel/evd.cmi library/global.cmi library/impargs.cmi \
library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -494,11 +502,9 @@ library/library.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \
library/libobject.cmx kernel/names.cmx library/nametab.cmx \
lib/options.cmx lib/pp.cmx library/summary.cmx lib/system.cmx \
lib/util.cmx library/library.cmi
-library/nametab.cmo: kernel/declarations.cmi library/libobject.cmi \
- kernel/names.cmi lib/pp.cmi library/summary.cmi kernel/term.cmi \
+library/nametab.cmo: kernel/names.cmi lib/pp.cmi library/summary.cmi \
lib/util.cmi library/nametab.cmi
-library/nametab.cmx: kernel/declarations.cmx library/libobject.cmx \
- kernel/names.cmx lib/pp.cmx library/summary.cmx kernel/term.cmx \
+library/nametab.cmx: kernel/names.cmx lib/pp.cmx library/summary.cmx \
lib/util.cmx library/nametab.cmi
library/opaque.cmo: kernel/closure.cmi kernel/declarations.cmi \
kernel/environ.cmi library/global.cmi kernel/names.cmi \
@@ -514,14 +520,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
library/summary.cmi
library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
library/summary.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
-lib/util.cmo: lib/pp.cmi lib/util.cmi
-lib/util.cmx: lib/pp.cmx lib/util.cmi
parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi
parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \
@@ -546,12 +544,10 @@ parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi kernel/names.cmi \
parsing/coqast.cmi
parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx kernel/names.cmx \
parsing/coqast.cmi
-parsing/coqlib.cmo: library/declare.cmi kernel/evd.cmi library/global.cmi \
- kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi \
- kernel/term.cmi lib/util.cmi parsing/coqlib.cmi
-parsing/coqlib.cmx: library/declare.cmx kernel/evd.cmx library/global.cmx \
- kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx \
- kernel/term.cmx lib/util.cmx parsing/coqlib.cmi
+parsing/coqlib.cmo: library/declare.cmi kernel/names.cmi library/nametab.cmi \
+ pretyping/pattern.cmi kernel/term.cmi lib/util.cmi parsing/coqlib.cmi
+parsing/coqlib.cmx: library/declare.cmx kernel/names.cmx library/nametab.cmx \
+ pretyping/pattern.cmx kernel/term.cmx lib/util.cmx parsing/coqlib.cmi
parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \
parsing/egrammar.cmi
@@ -719,25 +715,25 @@ pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmx \
kernel/term.cmx kernel/typeops.cmx lib/util.cmx pretyping/coercion.cmi
pretyping/detyping.cmo: kernel/declarations.cmi library/declare.cmi \
- kernel/environ.cmi kernel/evd.cmi library/global.cmi library/goptions.cmi \
+ kernel/environ.cmi library/global.cmi library/goptions.cmi \
library/impargs.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
lib/util.cmi pretyping/detyping.cmi
pretyping/detyping.cmx: kernel/declarations.cmx library/declare.cmx \
- kernel/environ.cmx kernel/evd.cmx library/global.cmx library/goptions.cmx \
+ kernel/environ.cmx library/global.cmx library/goptions.cmx \
library/impargs.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
pretyping/rawterm.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
lib/util.cmx pretyping/detyping.cmi
pretyping/evarconv.cmo: pretyping/classops.cmi kernel/closure.cmi \
- kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
- kernel/instantiate.cmi kernel/names.cmi pretyping/recordops.cmi \
- kernel/reduction.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
- pretyping/evarconv.cmi
+ library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \
+ kernel/evd.cmi kernel/instantiate.cmi kernel/names.cmi \
+ pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi \
+ pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi
pretyping/evarconv.cmx: pretyping/classops.cmx kernel/closure.cmx \
- kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \
- kernel/instantiate.cmx kernel/names.cmx pretyping/recordops.cmx \
- kernel/reduction.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
- pretyping/evarconv.cmi
+ library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+ kernel/evd.cmx kernel/instantiate.cmx kernel/names.cmx \
+ pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx \
+ pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi
pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi library/global.cmi \
library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \
@@ -748,20 +744,22 @@ pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx library/global.cmx \
pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \
kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
pretyping/evarutil.cmi
-pretyping/pattern.cmo: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
- library/global.cmi kernel/names.cmi pretyping/rawterm.cmi \
- kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/pattern.cmi
-pretyping/pattern.cmx: library/declare.cmx kernel/environ.cmx kernel/evd.cmx \
- library/global.cmx kernel/names.cmx pretyping/rawterm.cmx \
- kernel/reduction.cmx kernel/term.cmx lib/util.cmx pretyping/pattern.cmi
+pretyping/pattern.cmo: library/declare.cmi kernel/environ.cmi \
+ kernel/names.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+ kernel/term.cmi lib/util.cmi pretyping/pattern.cmi
+pretyping/pattern.cmx: library/declare.cmx kernel/environ.cmx \
+ kernel/names.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+ kernel/term.cmx lib/util.cmx pretyping/pattern.cmi
pretyping/pretype_errors.cmo: kernel/environ.cmi kernel/evd.cmi \
kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi \
pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
- kernel/term.cmi kernel/type_errors.cmi pretyping/pretype_errors.cmi
+ kernel/term.cmi kernel/type_errors.cmi lib/util.cmi \
+ pretyping/pretype_errors.cmi
pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/evd.cmx \
kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \
pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \
- kernel/term.cmx kernel/type_errors.cmx pretyping/pretype_errors.cmi
+ kernel/term.cmx kernel/type_errors.cmx lib/util.cmx \
+ pretyping/pretype_errors.cmi
pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
pretyping/coercion.cmi library/declare.cmi lib/dyn.cmi kernel/environ.cmi \
pretyping/evarconv.cmi pretyping/evarutil.cmi kernel/evd.cmi \
@@ -1003,15 +1001,15 @@ tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi
tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \
pretyping/evarutil.cmi kernel/evd.cmi lib/explore.cmi proofs/logic.cmi \
kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
- proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
- proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
- kernel/term.cmi lib/util.cmi
+ proofs/proof_type.cmi kernel/reduction.cmi parsing/search.cmi \
+ kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+ tactics/tactics.cmi kernel/term.cmi lib/util.cmi
tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \
pretyping/evarutil.cmx kernel/evd.cmx lib/explore.cmx proofs/logic.cmx \
kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
- proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
- proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
- kernel/term.cmx lib/util.cmx
+ proofs/proof_type.cmx kernel/reduction.cmx parsing/search.cmx \
+ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+ tactics/tactics.cmx kernel/term.cmx lib/util.cmx
tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \
tactics/hiddentac.cmi tactics/hipattern.cmi kernel/inductive.cmi \
kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \
@@ -1196,12 +1194,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
lib/util.cmx tactics/wcclausenv.cmi
-tools/coqdep_lexer.cmo: config/coq_config.cmi
-tools/coqdep_lexer.cmx: config/coq_config.cmx
-tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
-tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi
tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
+tools/coqdep_lexer.cmo: config/coq_config.cmi
+tools/coqdep_lexer.cmx: config/coq_config.cmx
tools/gallina.cmo: tools/gallina_lexer.cmo
tools/gallina.cmx: tools/gallina_lexer.cmx
toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \
@@ -1220,26 +1218,28 @@ toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
kernel/evd.cmi library/global.cmi library/impargs.cmi library/indrec.cmi \
kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
- library/library.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \
- proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
- kernel/reduction.cmi kernel/safe_typing.cmi library/states.cmi \
- pretyping/syntax_def.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
- kernel/term.cmi lib/util.cmi toplevel/command.cmi
+ library/library.cmi proofs/logic.cmi kernel/names.cmi library/nametab.cmi \
+ lib/options.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_type.cmi kernel/reduction.cmi kernel/safe_typing.cmi \
+ library/states.cmi pretyping/syntax_def.cmi proofs/tacmach.cmi \
+ pretyping/tacred.cmi kernel/term.cmi lib/util.cmi toplevel/command.cmi
toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
kernel/evd.cmx library/global.cmx library/impargs.cmx library/indrec.cmx \
kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
- library/library.cmx proofs/logic.cmx kernel/names.cmx lib/options.cmx \
- proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
- kernel/reduction.cmx kernel/safe_typing.cmx library/states.cmx \
- pretyping/syntax_def.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
- kernel/term.cmx lib/util.cmx toplevel/command.cmi
+ library/library.cmx proofs/logic.cmx kernel/names.cmx library/nametab.cmx \
+ lib/options.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_type.cmx kernel/reduction.cmx kernel/safe_typing.cmx \
+ library/states.cmx pretyping/syntax_def.cmx proofs/tacmach.cmx \
+ pretyping/tacred.cmx kernel/term.cmx lib/util.cmx toplevel/command.cmi
toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
- library/nametab.cmi lib/options.cmi lib/pp.cmi lib/system.cmi \
- toplevel/toplevel.cmi toplevel/vernac.cmi toplevel/coqinit.cmi
+ kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
+ lib/system.cmi toplevel/toplevel.cmi toplevel/vernac.cmi \
+ toplevel/coqinit.cmi
toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \
- library/nametab.cmx lib/options.cmx lib/pp.cmx lib/system.cmx \
- toplevel/toplevel.cmx toplevel/vernac.cmx toplevel/coqinit.cmi
+ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
+ lib/system.cmx toplevel/toplevel.cmx toplevel/vernac.cmx \
+ toplevel/coqinit.cmi
toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
toplevel/errors.cmi library/lib.cmi library/library.cmi \
toplevel/mltop.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
@@ -1347,13 +1347,13 @@ toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
pretyping/recordops.cmx kernel/term.cmx kernel/type_errors.cmx \
lib/util.cmx toplevel/record.cmi
toplevel/recordobj.cmo: pretyping/classops.cmi library/declare.cmi \
- kernel/evd.cmi library/global.cmi kernel/instantiate.cmi library/lib.cmi \
- kernel/names.cmi lib/pp.cmi parsing/printer.cmi pretyping/recordops.cmi \
- kernel/term.cmi lib/util.cmi toplevel/recordobj.cmi
+ library/global.cmi kernel/instantiate.cmi library/lib.cmi \
+ kernel/names.cmi lib/pp.cmi pretyping/recordops.cmi kernel/term.cmi \
+ lib/util.cmi toplevel/recordobj.cmi
toplevel/recordobj.cmx: pretyping/classops.cmx library/declare.cmx \
- kernel/evd.cmx library/global.cmx kernel/instantiate.cmx library/lib.cmx \
- kernel/names.cmx lib/pp.cmx parsing/printer.cmx pretyping/recordops.cmx \
- kernel/term.cmx lib/util.cmx toplevel/recordobj.cmi
+ library/global.cmx kernel/instantiate.cmx library/lib.cmx \
+ kernel/names.cmx lib/pp.cmx pretyping/recordops.cmx kernel/term.cmx \
+ lib/util.cmx toplevel/recordobj.cmi
toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi library/lib.cmi \
toplevel/mltop.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
proofs/pfedit.cmi lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \
@@ -1364,6 +1364,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \
toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi
toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi
toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
+ library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
+ lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi toplevel/vernac.cmi
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
+ library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
+ lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx toplevel/vernac.cmi
toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \
parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
@@ -1406,14 +1414,16 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \
toplevel/vernacinterp.cmi
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
- library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
- lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
- toplevel/vernacinterp.cmi toplevel/vernac.cmi
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
- library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
- lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
- toplevel/vernacinterp.cmx toplevel/vernac.cmi
+contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
+ library/declare.cmi pretyping/detyping.cmi kernel/names.cmi \
+ library/nametab.cmi contrib/correctness/past.cmi \
+ contrib/correctness/pmisc.cmi pretyping/rawterm.cmi toplevel/record.cmi \
+ kernel/sign.cmi kernel/term.cmi lib/util.cmi contrib/correctness/pcic.cmi
+contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
+ library/declare.cmx pretyping/detyping.cmx kernel/names.cmx \
+ library/nametab.cmx contrib/correctness/past.cmi \
+ contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
+ kernel/sign.cmx kernel/term.cmx lib/util.cmx contrib/correctness/pcic.cmi
contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
contrib/correctness/past.cmi contrib/correctness/penv.cmi \
contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
@@ -1426,16 +1436,6 @@ contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
kernel/univ.cmx contrib/correctness/pcicenv.cmi
-contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
- library/declare.cmi pretyping/detyping.cmi kernel/names.cmi \
- library/nametab.cmi contrib/correctness/past.cmi \
- contrib/correctness/pmisc.cmi pretyping/rawterm.cmi toplevel/record.cmi \
- kernel/sign.cmi kernel/term.cmi lib/util.cmi contrib/correctness/pcic.cmi
-contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
- library/declare.cmx pretyping/detyping.cmx kernel/names.cmx \
- library/nametab.cmx contrib/correctness/past.cmi \
- contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
- kernel/sign.cmx kernel/term.cmx lib/util.cmx contrib/correctness/pcic.cmi
contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -1652,28 +1652,30 @@ contrib/extraction/extract_env.cmo: parsing/astterm.cmi kernel/evd.cmi \
library/library.cmi contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi \
contrib/extraction/ocaml.cmi lib/pp.cmi parsing/printer.cmi \
- kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \
- contrib/extraction/extract_env.cmi
+ contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi contrib/extraction/extract_env.cmi
contrib/extraction/extract_env.cmx: parsing/astterm.cmx kernel/evd.cmx \
contrib/extraction/extraction.cmx library/global.cmx \
contrib/extraction/haskell.cmx library/lib.cmx library/libobject.cmx \
library/library.cmx contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmx kernel/names.cmx library/nametab.cmx \
contrib/extraction/ocaml.cmx lib/pp.cmx parsing/printer.cmx \
- kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \
- contrib/extraction/extract_env.cmi
+ contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx contrib/extraction/extract_env.cmi
contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \
kernel/environ.cmi kernel/evd.cmi library/global.cmi lib/gmap.cmi \
kernel/inductive.cmi kernel/instantiate.cmi contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi \
kernel/reduction.cmi pretyping/retyping.cmi library/summary.cmi \
- kernel/term.cmi lib/util.cmi contrib/extraction/extraction.cmi
+ contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
+ contrib/extraction/extraction.cmi
contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
kernel/environ.cmx kernel/evd.cmx library/global.cmx lib/gmap.cmx \
kernel/inductive.cmx kernel/instantiate.cmx contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmx kernel/names.cmx lib/pp.cmx \
kernel/reduction.cmx pretyping/retyping.cmx library/summary.cmx \
- kernel/term.cmx lib/util.cmx contrib/extraction/extraction.cmi
+ contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
+ contrib/extraction/extraction.cmi
contrib/extraction/haskell.cmo: kernel/environ.cmi library/global.cmi \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
kernel/names.cmi contrib/extraction/ocaml.cmi lib/options.cmi lib/pp.cmi \
@@ -1684,26 +1686,34 @@ contrib/extraction/haskell.cmx: kernel/environ.cmx library/global.cmx \
kernel/names.cmx contrib/extraction/ocaml.cmx lib/options.cmx lib/pp.cmx \
lib/pp_control.cmx kernel/term.cmx lib/util.cmx \
contrib/extraction/haskell.cmi
-contrib/extraction/mlutil.cmo: kernel/declarations.cmi library/global.cmi \
- library/lib.cmi library/libobject.cmi contrib/extraction/miniml.cmi \
- kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
- parsing/printer.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
- toplevel/vernacinterp.cmi contrib/extraction/mlutil.cmi
-contrib/extraction/mlutil.cmx: kernel/declarations.cmx library/global.cmx \
- library/lib.cmx library/libobject.cmx contrib/extraction/miniml.cmi \
- kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
- parsing/printer.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
- toplevel/vernacinterp.cmx contrib/extraction/mlutil.cmi
+contrib/extraction/mlutil.cmo: kernel/declarations.cmi \
+ contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi \
+ parsing/printer.cmi contrib/extraction/table.cmi kernel/term.cmi \
+ lib/util.cmi contrib/extraction/mlutil.cmi
+contrib/extraction/mlutil.cmx: kernel/declarations.cmx \
+ contrib/extraction/miniml.cmi kernel/names.cmx lib/pp.cmx \
+ parsing/printer.cmx contrib/extraction/table.cmx kernel/term.cmx \
+ lib/util.cmx contrib/extraction/mlutil.cmi
contrib/extraction/ocaml.cmo: kernel/environ.cmi library/global.cmi \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
kernel/names.cmi lib/options.cmi lib/pp.cmi lib/pp_control.cmi \
- parsing/printer.cmi kernel/term.cmi lib/util.cmi \
- contrib/extraction/ocaml.cmi
+ parsing/printer.cmi contrib/extraction/table.cmi kernel/term.cmi \
+ lib/util.cmi contrib/extraction/ocaml.cmi
contrib/extraction/ocaml.cmx: kernel/environ.cmx library/global.cmx \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
kernel/names.cmx lib/options.cmx lib/pp.cmx lib/pp_control.cmx \
- parsing/printer.cmx kernel/term.cmx lib/util.cmx \
- contrib/extraction/ocaml.cmi
+ parsing/printer.cmx contrib/extraction/table.cmx kernel/term.cmx \
+ lib/util.cmx contrib/extraction/ocaml.cmi
+contrib/extraction/table.cmo: kernel/declarations.cmi library/global.cmi \
+ library/goptions.cmi library/lib.cmi library/libobject.cmi \
+ kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
+ library/summary.cmi kernel/term.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi contrib/extraction/table.cmi
+contrib/extraction/table.cmx: kernel/declarations.cmx library/global.cmx \
+ library/goptions.cmx library/lib.cmx library/libobject.cmx \
+ kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
+ library/summary.cmx kernel/term.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx contrib/extraction/table.cmi
contrib/field/field.cmo: parsing/astterm.cmi parsing/coqast.cmi \
library/declare.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \
library/libobject.cmi kernel/names.cmi library/nametab.cmi \
@@ -1831,31 +1841,21 @@ contrib/interface/parse.cmx: contrib/interface/ascent.cmi \
contrib/interface/paths.cmo: contrib/interface/paths.cmi
contrib/interface/paths.cmx: contrib/interface/paths.cmi
contrib/interface/pbp.cmo: parsing/coqlib.cmi contrib/interface/ctast.cmo \
- library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
- tactics/hipattern.cmi proofs/logic.cmi kernel/names.cmi \
- library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
- pretyping/pretyping.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
- pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacinterp.cmi \
- proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
- kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
- contrib/interface/pbp.cmi
+ library/declare.cmi kernel/environ.cmi tactics/hipattern.cmi \
+ proofs/logic.cmi kernel/names.cmi library/nametab.cmi \
+ pretyping/pattern.cmi lib/pp.cmi pretyping/pretyping.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+ kernel/reduction.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+ pretyping/typing.cmi lib/util.cmi contrib/interface/pbp.cmi
contrib/interface/pbp.cmx: parsing/coqlib.cmx contrib/interface/ctast.cmx \
- library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
- tactics/hipattern.cmx proofs/logic.cmx kernel/names.cmx \
- library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
- pretyping/pretyping.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
- pretyping/rawterm.cmx kernel/reduction.cmx proofs/tacinterp.cmx \
- proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
- kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
- contrib/interface/pbp.cmi
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
- parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
- parsing/printer.cmi contrib/interface/translate.cmi \
- contrib/interface/vtp.cmi contrib/interface/xlate.cmi
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
- parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
- parsing/printer.cmx contrib/interface/translate.cmx \
- contrib/interface/vtp.cmx contrib/interface/xlate.cmx
+ library/declare.cmx kernel/environ.cmx tactics/hipattern.cmx \
+ proofs/logic.cmx kernel/names.cmx library/nametab.cmx \
+ pretyping/pattern.cmx lib/pp.cmx pretyping/pretyping.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+ kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi
contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \
proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
kernel/environ.cmi kernel/evd.cmi library/global.cmi kernel/inductive.cmi \
@@ -1874,6 +1874,14 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \
contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \
toplevel/vernacinterp.cmx contrib/interface/showproof.cmi
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+ parsing/printer.cmi contrib/interface/translate.cmi \
+ contrib/interface/vtp.cmi contrib/interface/xlate.cmi
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+ parsing/printer.cmx contrib/interface/translate.cmx \
+ contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \
kernel/evd.cmi library/libobject.cmi library/library.cmi kernel/names.cmi \
@@ -1966,6 +1974,8 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
tactics/tactics.cmx kernel/term.cmx lib/util.cmx
+contrib/xml/xml.cmo: contrib/xml/xml.cmi
+contrib/xml/xml.cmx: contrib/xml/xml.cmi
contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
kernel/environ.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \
library/libobject.cmi library/library.cmi kernel/names.cmi \
@@ -1984,8 +1994,6 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
contrib/xml/xmlcommand.cmi
contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
contrib/xml/xmlcommand.cmx
-contrib/xml/xml.cmo: contrib/xml/xml.cmi
-contrib/xml/xml.cmx: contrib/xml/xml.cmi
tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
contrib/correctness/psyntax.cmo: parsing/grammar.cma
contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
diff --git a/Makefile b/Makefile
index 557626f79b..d6f3a60373 100644
--- a/Makefile
+++ b/Makefile
@@ -197,7 +197,9 @@ XMLCMO=contrib/xml/xml.cmo \
FOURIERCMO=contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo
-EXTRACTIONCMO=contrib/extraction/mlutil.cmo contrib/extraction/ocaml.cmo \
+EXTRACTIONCMO=contrib/extraction/table.cmo\
+ contrib/extraction/mlutil.cmo\
+ contrib/extraction/ocaml.cmo \
contrib/extraction/haskell.cmo \
contrib/extraction/extraction.cmo \
contrib/extraction/extract_env.cmo
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index f32b3e96db..51574bda0d 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -16,34 +16,42 @@ Grammar vernac vernac : ast :=
(* Monolithic extraction to a file *)
| extr_file
- [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ]
- -> [ (ExtractionFile "ocaml" $o $f ($LIST $l)) ]
+ [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ]
+ -> [ (ExtractionFile "ocaml" $f ($LIST $l)) ]
| haskell_extr_file
- [ "Haskell" "Extraction" stringarg($f) options($o)
- ne_qualidarg_list($l) "." ]
- -> [ (ExtractionFile "haskell" $o $f ($LIST $l)) ]
+ [ "Haskell" "Extraction" stringarg($f) ne_qualidarg_list($l) "." ]
+ -> [ (ExtractionFile "haskell" $f ($LIST $l)) ]
(* Modular extraction (one Coq module = one ML module) *)
| extr_module
- [ "Extraction" "Module" options($o) identarg($m) "." ]
- -> [ (ExtractionModule "ocaml" $o $m) ]
+ [ "Extraction" "Module" identarg($m) "." ]
+ -> [ (ExtractionModule "ocaml" $m) ]
| haskell_extr_module
- [ "Haskell" "Extraction" "Module" options($o) identarg($m) "." ]
- -> [ (ExtractionModule "haskell" $o $m) ]
+ [ "Haskell" "Extraction" "Module" identarg($m) "." ]
+ -> [ (ExtractionModule "haskell" $m) ]
+
+(* Custum inlining directives *)
+| inline_constant
+ [ "Extraction" "Inline" ne_qualidarg_list($l) "." ]
+ -> [ (ExtractionInline ($LIST $l)) ]
+
+| no_inline_constant
+ [ "Extraction" "NoInline" ne_qualidarg_list($l) "." ]
+ -> [ (ExtractionNoInline ($LIST $l)) ]
(* Overriding of a Coq object by an ML one *)
| extract_constant
[ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
- -> [ (EXTRACT_CONSTANT $x $y) ]
+ -> [ (ExtractConstant $x $y) ]
| extract_inlined_constant
[ "Extract" "Inlined" "Constant" qualidarg($x)
"=>" idorstring($y) "." ]
- -> [ (EXTRACT_INLINED_CONSTANT $x $y) ]
+ -> [ (ExtractInlinedConstant $x $y) ]
| extract_inductive
[ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
- -> [ (EXTRACT_INDUCTIVE $x $y) ]
+ -> [ (ExtractInductive $x $y) ]
(* Utility entries *)
with mindnames : ast :=
@@ -57,9 +65,4 @@ with idorstring_list: ast list :=
with idorstring : ast :=
ids_ident [ identarg($id) ] -> [ $id ]
| ids_string [ stringarg($s) ] -> [ $s ]
-
-with options : ast :=
-| ext_opt_noopt [ "[" "noopt" "]" ] -> [ (VERNACARGLIST "noopt") ]
-| ext_op_expand [ "[" "expand" ne_qualidarg_list($l) "]" ] ->
- [ (VERNACARGLIST "expand" ($LIST $l)) ]
-| ext_opt_none [ ] -> [ (VERNACARGLIST "nooption") ].
+. \ No newline at end of file
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index d726d4fa33..02e2da7419 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -15,7 +15,9 @@ open Term
open Lib
open Extraction
open Miniml
+open Table
open Mlutil
+open Vernacinterp
(*s Recursive computation of the global references to extract.
We use a set of functions visiting the extracted objects in
@@ -85,6 +87,7 @@ and visit_decl eenv = function
visit_type eenv t
| Dglob (_,a) ->
visit_ast eenv a
+ | Dcustom _ -> ()
(*s Recursive extracted environment for a list of reference: we just
iterate [visit_reference] on the list, starting with an empty
@@ -110,17 +113,16 @@ end
module Pp = Ocaml.Make(ToplevelParams)
-open Vernacinterp
-
let refs_set_of_list l = List.fold_right Refset.add l Refset.empty
let decl_of_refs refs =
- let params =
- { modular = false ; module_name = "" ;
- optimization = true ; to_keep = refs_set_of_list refs;
- to_expand = Refset.empty } in
- let rl = List.map extract_declaration (extract_env refs) in
- optimize params rl
+ List.map extract_declaration (extract_env refs)
+
+let local_optimize refs =
+ let prm =
+ { strict = true ; modular = false ;
+ module_name = "" ; to_appear = refs} in
+ optimize prm (decl_of_refs refs)
let print_user_extract r =
mSGNL [< 'sTR "User defined extraction:"; 'sPC; 'sTR (find_ml_extraction r) ; 'fNL>]
@@ -129,7 +131,7 @@ let extract_reference r =
if is_ml_extraction r then
print_user_extract r
else
- mSGNL (Pp.pp_decl (list_last (decl_of_refs [r])))
+ mSGNL (Pp.pp_decl (list_last (local_optimize [r])))
let _ =
vinterp_add "Extraction"
@@ -153,17 +155,6 @@ let _ =
\verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
to get the saturated environment to extract. *)
-let no_such_reference q =
- errorlabstrm "reference_of_varg"
- [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
-
-let reference_of_varg = function
- | VARG_QUALID q ->
- (try Nametab.locate q with Not_found -> no_such_reference q)
- | _ -> assert false
-
-let refs_of_vargl = List.map reference_of_varg
-
let _ =
vinterp_add "ExtractionRec"
(fun vl () ->
@@ -181,22 +172,6 @@ let strict_language = function
| "haskell" -> false
| _ -> assert false
-let interp_options lang keep modular m = function
- | [VARG_STRING "noopt"] ->
- { optimization = false; modular = modular; module_name = m;
- to_keep = refs_set_of_list keep; to_expand = Refset.empty }
- | [VARG_STRING "nooption"] ->
- { optimization = strict_language lang;
- modular = modular; module_name = m;
- to_keep = refs_set_of_list keep; to_expand = Refset.empty }
- | VARG_STRING "expand" :: l ->
- { optimization = strict_language lang;
- modular = modular; module_name = m;
- to_keep = refs_set_of_list keep;
- to_expand = refs_set_of_list (refs_of_vargl l) }
- | _ ->
- assert false
-
(*s Extraction to a file (necessarily recursive).
The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
We just call [extract_to_file] on the saturated environment. *)
@@ -212,15 +187,14 @@ let _ =
| VARG_STRING lang :: VARG_VARGLIST o :: VARG_STRING f :: vl ->
(fun () ->
let refs = refs_of_vargl vl in
- let prm = interp_options lang refs false "" o in
+ let prm = {strict=strict_language lang;
+ modular=false;
+ module_name="";
+ to_appear= refs} in
let decls = decl_of_refs refs in
+ let decls = add_ml_decls prm decls in
let decls = optimize prm decls in
- let ml_decls =
- list_subtract
- (List.filter is_ml_extraction refs)
- (fst (ml_cst_extractions ()))
- in
- extract_to_file lang f prm decls ml_decls)
+ extract_to_file lang f prm decls)
| _ -> assert false)
(*s Extraction of a module. The vernacular command is \verb!Extraction Module!
@@ -246,6 +220,7 @@ let decl_mem rl = function
| Dabbrev (r,_,_) -> List.mem r rl
| Dtype ((_,r,_)::_, _) -> List.mem r rl
| Dtype ([],_) -> false
+ | Dcustom (r,s) -> List.mem r rl
let file_suffix = function
| "ocaml" -> ".ml"
@@ -260,9 +235,13 @@ let _ =
Ocaml.current_module := Some m;
let ms = Names.string_of_id m in
let f = (String.uncapitalize ms) ^ (file_suffix lang) in
- let prm = interp_options lang [] true ms o in
+ let prm = {strict=strict_language lang;
+ modular=true;
+ module_name= Names.string_of_id m;
+ to_appear= []} in
let rl = extract_module m in
let decls = optimize prm (decl_of_refs rl) in
+ let decls = add_ml_decls prm decls in
let decls = List.filter (decl_mem rl) decls in
- extract_to_file lang f prm decls [])
+ extract_to_file lang f prm decls)
| _ -> assert false)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f5b28598c7..23264fb075 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -18,6 +18,7 @@ open Reduction
open Inductive
open Instantiate
open Miniml
+open Table
open Mlutil
open Closure
open Summary
@@ -892,7 +893,7 @@ and extract_inductive_declaration sp =
(*s Extraction of a global reference i.e. a constant or an inductive. *)
let false_rec_sp = path_of_string "Coq.Init.Specif.False_rec"
-let false_rec_e = MLlam (prop_name, MLexn (id_of_string "False_rec"))
+let false_rec_e = MLlam (prop_name, MLexn "False_rec")
let extract_declaration r = match r with
| ConstRef sp when sp = false_rec_sp -> Dglob (r, false_rec_e)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 057767f5e6..9549829862 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -196,9 +196,8 @@ let rec pp_expr par env args =
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
- | MLexn id ->
- [< open_par par; 'sTR "error"; 'sPC;
- 'qS (string_of_id id); close_par par >]
+ | MLexn str ->
+ [< open_par par; 'sTR "error"; 'sPC; 'qS str; close_par par >]
| MLprop ->
string "prop"
| MLarity ->
@@ -223,10 +222,7 @@ and pp_pat env pv =
end;
'sTR " ->"; 'sPC; pp_expr par env' [] t >]
in
- if pv = [||] then
- [< 'sTR "_ -> error \"shouldn't happen\" -- empty inductive" >]
- else
- [< prvect_with_sep (fun () -> [< 'fNL; 'sTR " " >]) pp_one_pat pv >]
+ [< prvect_with_sep (fun () -> [< 'fNL; 'sTR " " >]) pp_one_pat pv >]
(*s names of the functions ([ids]) are already pushed in [env],
and passed here just for convenience. *)
@@ -313,6 +309,9 @@ let pp_decl = function
[< >] >]
| Dglob (r, a) ->
hOV 0 [< pp_function (empty_env ()) (pp_global r) a; 'fNL >]
+ | Dcustom (r,s) ->
+ hOV 0 [< 'sTR (string_of_r r); 'sTR " =";
+ 'sPC; 'sTR s; 'fNL >]
let pp_type = pp_type false
@@ -407,23 +406,11 @@ let haskell_preamble prm =
'sTR "type Arity = ()"; 'fNL;
'sTR "arity = ()"; 'fNL; 'fNL >]
-let haskell_header ft b ml_decls =
- let l,l' = ml_cst_extractions () in
- List.iter2
- (fun r s ->
- if (not b) or (Some (module_of_r r) = !current_module) then
- pP_with ft (hV 0
- [< 'sTR (string_of_r r); 'sTR " ="; 'sPC; 'sTR s; 'fNL ; 'fNL >]))
- ((List.rev l) @ ml_decls)
- ((List.rev l') @ (List.map find_ml_extraction ml_decls))
-
-
-let extract_to_file f prm decls ml_decls=
+let extract_to_file f prm decls=
let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
let cout = open_out f in
let ft = Pp_control.with_output_to cout in
pP_with ft (hV 0 (haskell_preamble prm));
- haskell_header ft prm.modular ml_decls;
begin
try
List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 4f380271f5..fa10cb1bd9 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,4 +15,4 @@ open Mlutil
open Names
val extract_to_file :
- string -> extraction_params -> ml_decl list -> global_reference list -> unit
+ string -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index c2ed8e7a97..d8a9597e18 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -40,7 +40,7 @@ type ml_ast =
| MLcons of global_reference * ml_ast list
| MLcase of ml_ast * (global_reference * identifier list * ml_ast) array
| MLfix of int * identifier array * ml_ast array
- | MLexn of identifier
+ | MLexn of string
| MLprop
| MLarity
| MLcast of ml_ast * ml_type
@@ -52,6 +52,7 @@ type ml_decl =
| Dtype of ml_ind list * bool (* cofix *)
| Dabbrev of global_reference * identifier list * ml_type
| Dglob of global_reference * ml_ast
+ | Dcustom of global_reference * string
(*s Pretty-printing of MiniML in a given concrete syntax is parameterized
by a function [pp_global] that pretty-prints global references.
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index cb555a67a4..649d816f6d 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -9,14 +9,12 @@
(*i $Id$ i*)
open Pp
-open Options
open Names
open Term
open Declarations
-open Libobject
-open Lib
open Util
open Miniml
+open Table
(*s Dummy names. *)
@@ -218,12 +216,10 @@ let check_identity_case br =
check_list (List.length l) l'
| _ -> raise Impossible
in
- if br=[||] then raise Impossible;
Array.iter check_one_branch br
let check_constant_case br =
- if br = [||] then raise Impossible;
let (r,l,t) = br.(0) in
let n = List.length l in
if occurs_itvl 1 n t then raise Impossible;
@@ -234,7 +230,19 @@ let check_constant_case br =
if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t))
then raise Impossible
done; cst
-
+
+
+let all_constr br =
+ try
+ Array.iter
+ (fun (_,_,t)->
+ match t with
+ | MLcons _ -> ()
+ | _ -> raise Impossible)
+ br;
+ true
+ with Impossible -> false
+
let rec betaiota = function
| MLapp (f, []) ->
@@ -261,26 +269,37 @@ let rec betaiota = function
(fun (n,l,t) ->
let k = List.length l in
let a'' = List.map (ml_lift k) a' in
- (n, l, betaiota (MLapp (t,a''))))
+ (n, l, betaiota (MLapp (t,a''))))
br
- in
- betaiota (MLcase (e,br'))
+ in betaiota (MLcase (e,br'))
| _ ->
MLapp (f',a'))
+ | MLcase (e,[||]) ->
+ MLexn "Empty inductive"
| MLcase (e,br) ->
(match betaiota e with
- (* iota redex *)
- | MLcons (r,a) ->
- let j = constructor_index r in
- let (_,ids,c) = br.(j) in
+ (* iota redex *)
+ | MLcons (r,a) ->
+ let (_,ids,c) = br.(constructor_index r) in
let c' = List.fold_right (fun id t -> MLlam (id,t)) ids c in
betaiota (MLapp (c',a))
+ | MLcase(e',br') when (all_constr br') ->
+ let new_br=
+ Array.map
+ (function
+ | (n, i, MLcons (r,a))->
+ let (_,ids,c) = br.(constructor_index r) in
+ let c = ml_lift (List.length i) c in
+ let c' = List.fold_right (fun id t -> MLlam (id,t)) ids c in
+ (n,i,betaiota (MLapp (c',a)))
+ | _ -> assert false) br'
+ in MLcase(e', new_br)
| e' ->
let br' = Array.map (fun (n,l,t) -> (n,l,betaiota t)) br in
- try check_identity_case br'; e'
- with Impossible ->
- try check_constant_case br'
- with Impossible -> MLcase (e', br'))
+ try check_identity_case br'; e'
+ with Impossible ->
+ try check_constant_case br'
+ with Impossible -> MLcase (e', br'))
| MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) ->
(* expansion of a letin in special cases *)
betaiota (ml_subst c e)
@@ -289,23 +308,12 @@ let rec betaiota = function
let normalize a = betaiota (merge_app a)
+let optional_normalize a = a (* TODO *)
+
let normalize_decl = function
| Dglob (id, a) -> Dglob (id, normalize a)
| d -> d
-(*s Extraction parameters *)
-
-module Refset =
- Set.Make(struct type t = global_reference let compare = compare end)
-
-type extraction_params = {
- modular : bool; (* modular extraction *)
- module_name : string; (* module name if [modular] *)
- optimization : bool; (* we need optimization *)
- to_keep : Refset.t; (* globals to keep *)
- to_expand : Refset.t; (* globals to expand *)
-}
-
(*s Utility functions used for the decision of expansion *)
let rec ml_size = function
@@ -344,7 +352,7 @@ exception Toplevel
let lift n l = List.map ((+) n) l
-let pop n l = List.map (fun x -> if x-n<0 then raise Toplevel else x-n) l
+let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l
(* This function returns a list of de Bruijn indices of non-strict variables,
or raises [Toplevel] if it has an internal non-strict variable.
@@ -361,10 +369,11 @@ let rec non_stricts add cand = function
pop 1 (non_stricts add cand t)
| MLrel n ->
List.filter ((<>) n) cand
-(*i old particular case
| MLapp (MLrel n, _) ->
- List.filter ((<>) n) cand
- (* In [(x y)] we say that only x is strict. (WHY?) *) i*)
+ List.filter ((<>) n) cand
+ (* In [(x y)] we say that only x is strict. Cf [sig_rec].
+ We may gain something if x is replaced by a function like
+ a projection *)
| MLapp (t,l)->
let cand = non_stricts false cand t in
List.fold_left (non_stricts false) cand l
@@ -412,30 +421,31 @@ let is_not_strict t =
If we could expand [t] (the user said nothing special),
should we expand ?
- We don't expand fixpoints, but always inductive constructors.
- Last case of expansion is a term not to big with at least one
- non-strict variable (i.e. a variable that may not be evaluated). *)
+ We don't expand fixpoints, but always inductive constructors
+ and small terms.
+ Last case of expansion is a term with at least one non-strict
+ variable (i.e. a variable that may not be evaluated). *)
let expansion_test t =
(not (is_fix t))
&&
- ((is_constr t)
- ||
- (ml_size t < 10 && is_not_strict t))
+ ((is_constr t) ||
+ (ml_size t < 3) ||
+ ((ml_size t < 12) && (is_not_strict t)))
(* If the user doesn't say he wants to keep [t], we expand in two cases:
\begin{itemize}
\item the user explicitly requests it
\item [expansion_test] answers that the expansion is a good idea, and
- we are free to act (no [noopt] given as argument)
+ we are free to act (AutoInline is set)
\end{itemize} *)
-let expand prm r t =
- (not (Refset.mem r prm.to_keep)) (* the user DOES want to keep it *)
+let expand strict_lang r t =
+ (not (to_keep r)) (* the user DOES want to keep it *)
&&
- (Refset.mem r prm.to_expand (* the user DOES want to expand it *)
+ ((to_inline r) (* the user DOES want to expand it *)
||
- (prm.optimization && expansion_test t))
+ (auto_inline () && strict_lang && expansion_test t))
(*s Optimization *)
@@ -450,178 +460,47 @@ let subst_glob_decl r m = function
| Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
| d -> d
-let warning_expansion r =
+let warning_expansion r t=
wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
- Printer.pr_global r; 'sPC; 'sTR "is expanded." >])
+ Printer.pr_global r;
+ 'sTR (" of size "^ (string_of_int (ml_size t))^" ");
+ 'sPC; 'sTR "is expanded." >])
+
+type extraction_params =
+ { strict : bool ;
+ modular : bool ;
+ module_name : string ;
+ to_appear : global_reference list }
+
+let print_ml_decl prm (r,_) =
+ not (to_inline r) || List.mem r prm.to_appear
+
+let add_ml_decls prm decls =
+ let l = sorted_ml_extractions () in
+ let l = List.filter (print_ml_decl prm) l in
+ let l = List.map (fun (r,s)-> Dcustom (r,s)) l in
+ (List.rev l @ decls)
let rec optimize prm = function
| [] ->
[]
- | (Dtype _ | Dabbrev _) as d :: l ->
+ | (Dtype _ | Dabbrev _ | Dcustom _) as d :: l ->
d :: (optimize prm l)
| Dglob (r, MLprop) as d :: l ->
- if Refset.mem r prm.to_keep then
+ if List.mem r prm.to_appear then
d :: (optimize prm l)
else optimize prm l
- (*i
- | Dglob(id,(MLexn _ as t)) as d :: l ->
- let l' = List.map (expand (id,t)) l in optimize prm l'
- i*)
| Dglob (r,t) :: l ->
let t = normalize t in
- let b = expand prm r t in
+ let t = if optim() then optional_normalize t else t in
+ let b = expand prm.strict r t in
let l = if b then
begin
- if_verbose warning_expansion r;
+ (*i if_verbose i*) warning_expansion r t;
List.map (subst_glob_decl r t) l
end
else l in
- if prm.modular || l = [] || not b then
+ if prm.modular || List.mem r prm.to_appear || not b then
Dglob (r,t) :: (optimize prm l)
else
optimize prm l
-
-(*s Table for direct ML extractions. *)
-
-module Refmap =
- Map.Make(struct type t = global_reference let compare = compare end)
-
-let empty_extractions = (Refmap.empty, Refset.empty)
-
-let extractions = ref empty_extractions
-
-let ml_extractions () = snd !extractions
-
-let add_ml_extraction r s =
- let (map,set) = !extractions in
- extractions := (Refmap.add r s map, Refset.add r set)
-
-let is_ml_extraction r = Refset.mem r (snd !extractions)
-
-let find_ml_extraction r = Refmap.find r (fst !extractions)
-
-(*s Registration of operations for rollback. *)
-
-let (in_ml_extraction,_) =
- declare_object ("ML extractions",
- { cache_function = (fun (_,(r,s)) -> add_ml_extraction r s);
- load_function = (fun (_,(r,s)) -> add_ml_extraction r s);
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) })
-
-(*s Registration of the table for rollback. *)
-
-open Summary
-
-let _ = declare_summary "ML extractions"
- { freeze_function = (fun () -> !extractions);
- unfreeze_function = ((:=) extractions);
- init_function = (fun () -> extractions := empty_extractions);
- survive_section = true }
-
-(*s List of Extract Constant directives *)
-
-let cst_extractions = ref ([],[])
-
-let ml_cst_extractions () = !cst_extractions
-
-let add_ml_cst_extraction r s =
- let l,l' = !cst_extractions in
- cst_extractions := r::l,s::l'
-
-let (in_ml_cst_extraction,_) =
- declare_object ("ML constants extractions",
- { cache_function = (fun (_,(r,s)) -> add_ml_cst_extraction r s);
- load_function = (fun (_,(r,s)) -> add_ml_cst_extraction r s);
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) })
-
-let _ = declare_summary "ML constants extractions"
- { freeze_function = (fun () -> !cst_extractions);
- unfreeze_function = ((:=) cst_extractions);
- init_function = (fun () -> cst_extractions := [],[]);
- survive_section = true }
-
-(*s Grammar entries. *)
-
-open Vernacinterp
-
-let string_of_varg = function
- | VARG_IDENTIFIER id -> string_of_id id
- | VARG_STRING s -> s
- | _ -> assert false
-
-let no_such_reference q =
- errorlabstrm "reference_of_varg"
- [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
-
-let reference_of_varg = function
- | VARG_QUALID q ->
- (try Nametab.locate q with Not_found -> no_such_reference q)
- | _ -> assert false
-
-(*s \verb!Extract Constant qualid => string! *)
-
-let extract_constant r s = match r with
- | ConstRef sp ->
- let rs = string_of_id (basename sp) in
- add_anonymous_leaf (in_ml_cst_extraction (r,s));
- add_anonymous_leaf (in_ml_extraction (r,rs))
- | _ ->
- errorlabstrm "extract_constant"
- [< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
-
-let _ =
- vinterp_add "EXTRACT_CONSTANT"
- (function
- | [id; s] ->
- (fun () ->
- extract_constant
- (reference_of_varg id)
- (string_of_varg s))
- | _ -> assert false)
-
-(*s \verb!Extract Inlined Constant qualid => string! *)
-
-let extract_inlined_constant r s = match r with
- | ConstRef _ ->
- add_anonymous_leaf (in_ml_extraction (r,s))
- | _ ->
- errorlabstrm "extract_constant"
- [< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
-
-let _ =
- vinterp_add "EXTRACT_INLINED_CONSTANT"
- (function
- | [id; s] ->
- (fun () ->
- extract_inlined_constant
- (reference_of_varg id)
- (string_of_varg s))
- | _ -> assert false)
-
-(*s \verb!Extract Inductive qualid => string [ string ... string ]! *)
-
-let extract_inductive r (id2,l2) = match r with
- | IndRef ((sp,i) as ip) ->
- let mib = Global.lookup_mind sp in
- let n = Array.length mib.mind_packets.(i).mind_consnames in
- if n <> List.length l2 then
- error "not the right number of constructors";
- add_anonymous_leaf (in_ml_extraction (r,id2));
- list_iter_i
- (fun j s ->
- add_anonymous_leaf
- (in_ml_extraction (ConstructRef (ip,succ j),s))) l2
- | _ ->
- errorlabstrm "extract_inductive"
- [< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
-
-let _ =
- vinterp_add "EXTRACT_INDUCTIVE"
- (function
- | [q1; VARG_VARGLIST (id2 :: l2)] ->
- (fun () ->
- extract_inductive (reference_of_varg q1)
- (string_of_varg id2, List.map string_of_varg l2))
- | _ -> assert false)
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 6f7168ed07..27608c46fe 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -50,30 +50,17 @@ val subst_glob_ast : global_reference -> ml_ast -> ml_ast -> ml_ast
val normalize : ml_ast -> ml_ast
val normalize_decl : ml_decl -> ml_decl
-(*s Extraction parameters *)
-
-module Refset : Set.S with type elt = global_reference
-
-type extraction_params = {
- modular : bool; (* modular extraction *)
- module_name : string; (* module name if [modular] *)
- optimization : bool; (* we need optimization *)
- to_keep : Refset.t; (* globals to keep *)
- to_expand : Refset.t; (* globals to expand *)
-}
-
(*s Optimization. *)
-val optimize : extraction_params -> ml_decl list -> ml_decl list
-
-(*s Table for direct extractions to ML values. *)
-
-val is_ml_extraction : global_reference -> bool
-val find_ml_extraction : global_reference -> string
+type extraction_params =
+ { strict : bool;
+ modular : bool;
+ module_name : string;
+ to_appear : global_reference list }
-val ml_extractions : unit -> Refset.t
+val add_ml_decls :
+ extraction_params -> ml_decl list -> ml_decl list
-(* List of Extract Constant directives *)
+val optimize :
+ extraction_params -> ml_decl list -> ml_decl list
-val ml_cst_extractions :
- unit -> global_reference list * string list
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 81d77741b0..e50b087442 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -15,6 +15,7 @@ open Util
open Names
open Term
open Miniml
+open Table
open Mlutil
open Options
@@ -92,8 +93,10 @@ let module_option r =
else (String.capitalize (string_of_id m)) ^ "."
let check_ml r d =
- try find_ml_extraction r
- with Not_found -> d
+ if to_inline r then d else
+ try
+ find_ml_extraction r
+ with Not_found -> d
(*s de Bruijn environments for programs *)
@@ -233,9 +236,9 @@ let rec pp_expr par env args =
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
- | MLexn id ->
- [< open_par par; 'sTR "failwith"; 'sPC;
- 'qS (string_of_id id); close_par par >]
+ | MLexn str ->
+ [< open_par par; 'sTR "assert false"; 'sPC;
+ 'sTR ("(* "^str^" *)"); close_par par >]
| MLprop ->
string "prop"
| MLarity ->
@@ -258,10 +261,7 @@ and pp_pat env pv =
end;
'sTR " ->"; 'sPC; pp_expr par env' [] t >]
in
- if pv = [||] then
- [< 'sTR "_ -> assert false (* empty inductive *)" >]
- else
- [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
+ [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
(*s names of the functions ([ids]) are already pushed in [env],
and passed here just for convenience. *)
@@ -367,6 +367,9 @@ let pp_decl = function
| Dglob (r, a) ->
hOV 0 [< 'sTR "let ";
pp_function (empty_env ()) (pp_global r) a; 'fNL >]
+ | Dcustom (r,s) ->
+ hOV 0 [< 'sTR "let "; 'sTR (string_of_r r);
+ 'sTR " ="; 'sPC; 'sTR s; 'fNL >]
let pp_type = pp_type false
@@ -461,23 +464,11 @@ let ocaml_preamble () =
'sTR "type arity = unit"; 'fNL;
'sTR "let arity = ()"; 'fNL; 'fNL >]
-
-let ocaml_header ft b ml_decls =
- let l,l' = ml_cst_extractions () in
- List.iter2
- (fun r s ->
- if (not b) or (Some (module_of_r r) = !current_module) then
- pP_with ft (hV 0
- [< 'sTR "let "; 'sTR (string_of_r r); 'sTR " ="; 'sPC; 'sTR s; 'fNL ; 'fNL >]))
- ((List.rev l) @ ml_decls)
- ((List.rev l') @ (List.map find_ml_extraction ml_decls))
-
-let extract_to_file f prm decls ml_decls =
+let extract_to_file f prm decls =
let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
let cout = open_out f in
let ft = Pp_control.with_output_to cout in
pP_with ft (hV 0 (ocaml_preamble ()));
- ocaml_header ft prm.modular ml_decls;
begin
try
List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index e1325d4814..58ee9b662f 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -43,6 +43,6 @@ module Make : functor(P : Mlpp_param) -> Mlpp
val current_module : Names.identifier option ref
val extract_to_file :
- string -> extraction_params -> ml_decl list -> global_reference list -> unit
+ string -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
new file mode 100644
index 0000000000..85f1887e2a
--- /dev/null
+++ b/contrib/extraction/table.ml
@@ -0,0 +1,203 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Summary
+open Goptions
+open Vernacinterp
+open Names
+open Util
+open Pp
+open Libobject
+open Term
+open Declarations
+open Lib
+
+(*s Set and Map over global reference *)
+
+module Refset =
+ Set.Make(struct type t = global_reference let compare = compare end)
+
+module Refmap =
+ Map.Make(struct type t = global_reference let compare = compare end)
+
+(*s Auxiliary functions *)
+
+let check_constant r = match r with
+ | ConstRef sp -> r
+ | _ -> errorlabstrm "extract_constant"
+ [< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
+
+let string_of_varg = function
+ | VARG_IDENTIFIER id -> string_of_id id
+ | VARG_STRING s -> s
+ | _ -> assert false
+
+let no_such_reference q =
+ errorlabstrm "reference_of_varg"
+ [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
+
+let reference_of_varg = function
+ | VARG_QUALID q ->
+ (try Nametab.locate q with Not_found -> no_such_reference q)
+ | _ -> assert false
+
+let refs_of_vargl = List.map reference_of_varg
+
+
+(*s AutoInline parameter *)
+
+let auto_inline_params =
+ {optsyncname = "Extraction AutoInline";
+ optsynckey = SecondaryTable ("Extraction", "AutoInline");
+ optsyncdefault = true}
+
+let auto_inline = declare_sync_bool_option auto_inline_params
+
+(*s Optimize parameter *)
+
+let optim_params =
+ {optsyncname = "Extraction Optimize";
+ optsynckey = SecondaryTable ("Extraction", "Optimize");
+ optsyncdefault = true}
+
+let optim = declare_sync_bool_option optim_params
+
+
+(*s Table for custom inlining *)
+
+let empty_inline_table = (Refset.empty,Refset.empty)
+
+let inline_table = ref empty_inline_table
+
+let to_inline r = Refset.mem r (fst !inline_table)
+
+let to_keep r = Refset.mem r (snd !inline_table)
+
+let add_inline_entries b l =
+ let f b = if b then Refset.add else Refset.remove in
+ let i,k = !inline_table in
+ inline_table :=
+ (List.fold_right (f b) l i),
+ (List.fold_right (f (not b)) l k)
+
+
+(*s Registration of operations for rollback. *)
+
+let (inline_extraction,_) =
+ declare_object ("Extraction Inline",
+ { cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
+ load_function = (fun (_,(b,l)) -> add_inline_entries b l);
+ open_function = (fun _ -> ());
+ export_function = (fun x -> Some x) })
+
+let _ = declare_summary "Extraction Inline"
+ { freeze_function = (fun () -> !inline_table);
+ unfreeze_function = ((:=) inline_table);
+ init_function = (fun () -> inline_table := empty_inline_table);
+ survive_section = true }
+
+(*s Grammar entries. *)
+
+let _ =
+ vinterp_add "ExtractionInline"
+ (fun vl () ->
+ let refs = List.map check_constant (refs_of_vargl vl) in
+ add_anonymous_leaf (inline_extraction (true,refs)))
+
+let _ =
+ vinterp_add "ExtractionNoInline"
+ (fun vl () ->
+ let refs = List.map check_constant (refs_of_vargl vl) in
+ add_anonymous_leaf (inline_extraction (false,refs)))
+
+
+(*s Table for direct ML extractions. *)
+
+let empty_extractions = (Refmap.empty, Refset.empty, [])
+
+let extractions = ref empty_extractions
+
+let ml_extractions () = let (_,set,_) = !extractions in set
+
+let sorted_ml_extractions () = let (_,_,l) = !extractions in l
+
+let add_ml_extraction r s =
+ let (map,set,list) = !extractions in
+ extractions := (Refmap.add r s map, Refset.add r set, (r,s)::list)
+
+let is_ml_extraction r =
+ let (_,set,_) = !extractions in Refset.mem r set
+
+let find_ml_extraction r =
+ let (map,_,_) = !extractions in Refmap.find r map
+
+(*s Registration of operations for rollback. *)
+
+let (in_ml_extraction,_) =
+ declare_object ("ML extractions",
+ { cache_function = (fun (_,(r,s)) -> add_ml_extraction r s);
+ load_function = (fun (_,(r,s)) -> add_ml_extraction r s);
+ open_function = (fun _ -> ());
+ export_function = (fun x -> Some x) })
+
+let _ = declare_summary "ML extractions"
+ { freeze_function = (fun () -> !extractions);
+ unfreeze_function = ((:=) extractions);
+ init_function = (fun () -> extractions := empty_extractions);
+ survive_section = true }
+
+
+(*s Grammar entries. *)
+
+let _ =
+ vinterp_add "ExtractConstant"
+ (function
+ | [id; vs] ->
+ (fun () ->
+ let r = check_constant (reference_of_varg id) in
+ let s = string_of_varg vs in
+ add_anonymous_leaf (in_ml_extraction (r,s)))
+ | _ -> assert false)
+
+let _ =
+ vinterp_add "ExtractInlinedConstant"
+ (function
+ | [id; vs] ->
+ (fun () ->
+ let r = check_constant (reference_of_varg id) in
+ let s = string_of_varg vs in
+ add_anonymous_leaf (inline_extraction (true,[r]));
+ add_anonymous_leaf (in_ml_extraction (r,s)))
+ | _ -> assert false)
+
+
+let extract_inductive r (id2,l2) = match r with
+ | IndRef ((sp,i) as ip) ->
+ let mib = Global.lookup_mind sp in
+ let n = Array.length mib.mind_packets.(i).mind_consnames in
+ if n <> List.length l2 then
+ error "not the right number of constructors";
+ add_anonymous_leaf (in_ml_extraction (r,id2));
+ list_iter_i
+ (fun j s ->
+ add_anonymous_leaf
+ (in_ml_extraction (ConstructRef (ip,succ j),s))) l2
+ | _ ->
+ errorlabstrm "extract_inductive"
+ [< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
+
+let _ =
+ vinterp_add "ExtarctInductive"
+ (function
+ | [q1; VARG_VARGLIST (id2 :: l2)] ->
+ (fun () ->
+ extract_inductive (reference_of_varg q1)
+ (string_of_varg id2, List.map string_of_varg l2))
+ | _ -> assert false)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
new file mode 100644
index 0000000000..7efbc0faaa
--- /dev/null
+++ b/contrib/extraction/table.mli
@@ -0,0 +1,49 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Summary
+open Goptions
+open Vernacinterp
+open Names
+
+(*s Set and Map over global reference *)
+
+module Refset : Set.S with type elt = global_reference
+
+(*s Auxiliary functions *)
+
+val check_constant : global_reference -> global_reference
+
+val refs_of_vargl : vernac_arg list -> global_reference list
+
+(*s AutoInline parameter *)
+
+val auto_inline : unit -> bool
+
+(*s Optimize parameter *)
+
+val optim : unit -> bool
+
+(* Table for custom inlining *)
+
+val to_inline : global_reference -> bool
+
+val to_keep : global_reference -> bool
+
+(*s Table for direct ML extractions. *)
+
+val is_ml_extraction : global_reference -> bool
+
+val find_ml_extraction : global_reference -> string
+
+val ml_extractions : unit -> Refset.t
+
+val sorted_ml_extractions : unit -> (global_reference * string) list
+
diff --git a/contrib/extraction/test/addReals b/contrib/extraction/test/addReals
index 86e9a79947..601592091a 100644
--- a/contrib/extraction/test/addReals
+++ b/contrib/extraction/test/addReals
@@ -22,4 +22,4 @@ let rec int_to_Z i =
else
Fast_integer.NEG (int_to_positive (-i))
-let my_ceil x = int_to_Z (int_of_float (ceil x))
+let my_ceil x = int_to_Z (succ (int_of_float (floor x)))
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 02:49:59 +0000