From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta
---
checker/check.ml | 32 ++++++++++----------------------
1 file changed, 10 insertions(+), 22 deletions(-)
(limited to 'checker/check.ml')
diff --git a/checker/check.ml b/checker/check.ml
index 40119a7e..bb42b949 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,18 +1,15 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
-let is_in_load_paths phys_dir =
- let dir = canonical_path_name phys_dir in
- let lp = get_load_paths () in
- let check_p = fun p -> (String.compare dir p) == 0 in
- List.exists check_p lp
-
let remove_load_path dir =
load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
@@ -191,13 +182,9 @@ let add_load_path (phys_path,coq_path) =
load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
-let physical_paths (dp,lp) = dp
-
let load_paths_of_dir_path dir =
fst (list_filter2 (fun p d -> d = dir) !load_paths)
-let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
-
(************************************************************************)
(*s Locate absolute or partially qualified library names in the path *)
@@ -269,8 +256,8 @@ let try_locate_qualified_library qid =
(*s Loading from disk to cache (preparation phase) *)
-let (raw_extern_library, raw_intern_library) =
- System.raw_extern_intern Coq_config.vo_magic_number ".vo"
+let raw_intern_library =
+ snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
let with_magic_number_check f a =
try f a
@@ -283,10 +270,10 @@ let with_magic_number_check f a =
(************************************************************************)
(* Internalise libraries *)
-let mk_library md f digest = {
+let mk_library md f table digest = {
library_name = md.md_name;
library_filename = f;
- library_compiled = md.md_compiled;
+ library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled;
library_deps = md.md_deps;
library_digest = digest }
@@ -300,20 +287,21 @@ let depgraph = ref LibraryMap.empty
let intern_from_file (dir, f) =
Flags.if_verbose msg (str"[intern "++str f++str" ...");
- let (md,digest) =
+ let (md,table,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
let (md:library_disk) = System.marshal_in ch in
let digest = System.marshal_in ch in
+ let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
close_in ch;
if dir <> md.md_name then
errorlabstrm "load_physical_library"
(name_clash_message dir md.md_name f);
Flags.if_verbose msgnl(str" done]");
- md,digest
+ md,table,digest
with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
- mk_library md f digest
+ mk_library md f table digest
let get_deps (dir, f) =
try LibraryMap.find dir !depgraph
--
cgit v1.2.3
From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg
---
.gitignore | 5 +-
CHANGES | 166 +-
COMPATIBILITY | 47 +-
INSTALL | 2 +-
INSTALL.macosx | 20 -
Makefile | 36 +-
Makefile.build | 33 +-
Makefile.common | 23 +-
TODO | 53 +
checker/check.ml | 2 +-
checker/check_stat.ml | 2 +-
checker/check_stat.mli | 2 +-
checker/checker.ml | 2 +-
checker/closure.ml | 2 +-
checker/closure.mli | 2 +-
checker/indtypes.ml | 2 +-
checker/indtypes.mli | 2 +-
checker/inductive.ml | 2 +-
checker/inductive.mli | 2 +-
checker/mod_checking.mli | 2 +-
checker/modops.ml | 2 +-
checker/modops.mli | 2 +-
checker/reduction.ml | 2 +-
checker/reduction.mli | 2 +-
checker/safe_typing.ml | 2 +-
checker/safe_typing.mli | 2 +-
checker/subtyping.ml | 2 +-
checker/subtyping.mli | 2 +-
checker/term.ml | 2 +-
checker/type_errors.ml | 2 +-
checker/type_errors.mli | 2 +-
checker/typeops.ml | 2 +-
checker/typeops.mli | 2 +-
checker/validate.ml | 2 +-
config/Makefile.template | 154 --
config/coq_config.mli | 2 +-
configure | 478 ++---
dev/db_printers.ml | 2 +-
dev/header | 2 +-
dev/macosify_accel.sh | 3 +
dev/top_printers.ml | 4 +-
doc/refman/RefMan-sch.tex | 418 -----
doc/stdlib/index-list.html.template | 6 +
ide/command_windows.ml | 2 +-
ide/command_windows.mli | 2 +-
ide/config_lexer.mll | 2 +-
ide/coq.ml | 2 +-
ide/coq.mli | 2 +-
ide/coq_commands.ml | 2 +-
ide/coq_lex.mll | 2 +-
ide/coqide.ml | 13 +-
ide/coqide.mli | 2 +-
ide/coqide_main.ml4 | 2 +-
ide/gtk_parsing.ml | 2 +-
ide/ide_mac_stubs.c | 10 +-
ide/ideproof.ml | 40 +-
ide/ideutils.ml | 2 +-
ide/ideutils.mli | 2 +-
ide/mac_default_accel_map | 726 ++++----
ide/minilib.ml | 55 +-
ide/preferences.ml | 4 +-
ide/preferences.mli | 2 +-
ide/project_file.ml4 | 2 +-
ide/tags.ml | 2 +-
ide/tags.mli | 2 +-
ide/typed_notebook.ml | 2 +-
ide/undo.ml | 2 +-
ide/undo_lablgtk_ge212.mli | 2 +-
ide/undo_lablgtk_ge26.mli | 2 +-
ide/undo_lablgtk_lt26.mli | 2 +-
ide/utf8_convert.mll | 2 +-
interp/constrextern.ml | 58 +-
interp/constrextern.mli | 4 +-
interp/constrintern.ml | 31 +-
interp/constrintern.mli | 2 +-
interp/coqlib.ml | 2 +-
interp/coqlib.mli | 2 +-
interp/dumpglob.ml | 2 +-
interp/dumpglob.mli | 2 +-
interp/genarg.ml | 2 +-
interp/genarg.mli | 2 +-
interp/implicit_quantifiers.ml | 2 +-
interp/implicit_quantifiers.mli | 2 +-
interp/modintern.ml | 2 +-
interp/modintern.mli | 2 +-
interp/notation.ml | 35 +-
interp/notation.mli | 2 +-
interp/ppextend.ml | 2 +-
interp/ppextend.mli | 2 +-
interp/reserve.ml | 2 +-
interp/reserve.mli | 2 +-
interp/smartlocate.ml | 2 +-
interp/smartlocate.mli | 2 +-
interp/syntax_def.ml | 66 +-
interp/syntax_def.mli | 12 +-
interp/topconstr.ml | 2 +-
interp/topconstr.mli | 2 +-
kernel/cbytecodes.ml | 2 +-
kernel/cbytecodes.mli | 4 +-
kernel/cbytegen.ml | 2 +-
kernel/cemitcodes.ml | 2 +-
kernel/closure.ml | 2 +-
kernel/closure.mli | 2 +-
kernel/conv_oracle.ml | 2 +-
kernel/conv_oracle.mli | 2 +-
kernel/cooking.ml | 8 +-
kernel/cooking.mli | 5 +-
kernel/csymtable.ml | 2 +-
kernel/csymtable.mli | 4 +-
kernel/declarations.ml | 2 +-
kernel/declarations.mli | 2 +-
kernel/entries.ml | 2 +-
kernel/entries.mli | 2 +-
kernel/environ.ml | 2 +-
kernel/environ.mli | 2 +-
kernel/esubst.ml | 2 +-
kernel/esubst.mli | 2 +-
kernel/indtypes.ml | 2 +-
kernel/indtypes.mli | 2 +-
kernel/inductive.ml | 2 +-
kernel/inductive.mli | 2 +-
kernel/mod_subst.ml | 2 +-
kernel/mod_subst.mli | 2 +-
kernel/mod_typing.ml | 2 +-
kernel/mod_typing.mli | 2 +-
kernel/modops.ml | 2 +-
kernel/modops.mli | 2 +-
kernel/names.ml | 2 +-
kernel/names.mli | 2 +-
kernel/pre_env.ml | 2 +-
kernel/pre_env.mli | 2 +-
kernel/reduction.ml | 2 +-
kernel/reduction.mli | 2 +-
kernel/retroknowledge.ml | 2 +-
kernel/retroknowledge.mli | 2 +-
kernel/safe_typing.ml | 2 +-
kernel/safe_typing.mli | 2 +-
kernel/sign.ml | 2 +-
kernel/sign.mli | 2 +-
kernel/subtyping.ml | 2 +-
kernel/subtyping.mli | 2 +-
kernel/term.ml | 3 +-
kernel/term.mli | 3 +-
kernel/term_typing.ml | 5 +-
kernel/term_typing.mli | 2 +-
kernel/type_errors.ml | 2 +-
kernel/type_errors.mli | 2 +-
kernel/typeops.ml | 2 +-
kernel/typeops.mli | 2 +-
kernel/univ.ml | 2 +-
kernel/univ.mli | 2 +-
kernel/vconv.mli | 2 +-
kernel/vm.ml | 2 +-
lib/bigint.ml | 355 ++--
lib/bigint.mli | 11 +-
lib/compat.ml4 | 2 +-
lib/dnet.ml | 2 +-
lib/dnet.mli | 2 +-
lib/dyn.ml | 2 +-
lib/dyn.mli | 2 +-
lib/envars.ml | 10 +-
lib/envars.mli | 2 +-
lib/explore.ml | 2 +-
lib/explore.mli | 2 +-
lib/flags.ml | 17 +-
lib/flags.mli | 7 +-
lib/gmap.ml | 2 +-
lib/gmap.mli | 2 +-
lib/gmapl.ml | 2 +-
lib/gmapl.mli | 2 +-
lib/hashcons.ml | 2 +-
lib/hashcons.mli | 2 +-
lib/hashtbl_alt.ml | 2 +-
lib/hashtbl_alt.mli | 2 +-
lib/heap.ml | 2 +-
lib/heap.mli | 2 +-
lib/option.ml | 2 +-
lib/option.mli | 2 +-
lib/pp.ml4 | 13 +-
lib/pp.mli | 6 +-
lib/pp_control.ml | 2 +-
lib/pp_control.mli | 2 +-
lib/profile.ml | 2 +-
lib/profile.mli | 2 +-
lib/rtree.ml | 2 +-
lib/rtree.mli | 2 +-
lib/system.ml | 2 +-
lib/system.mli | 2 +-
lib/tries.ml | 2 +-
lib/unionfind.ml | 2 +-
lib/unionfind.mli | 2 +-
lib/util.mli | 2 +-
lib/xml_lexer.mll | 6 +
library/assumptions.ml | 2 +-
library/assumptions.mli | 2 +-
library/decl_kinds.ml | 2 +-
library/decl_kinds.mli | 2 +-
library/declare.ml | 2 +-
library/declare.mli | 2 +-
library/declaremods.ml | 2 +-
library/declaremods.mli | 2 +-
library/decls.ml | 2 +-
library/decls.mli | 2 +-
library/dischargedhypsmap.ml | 2 +-
library/dischargedhypsmap.mli | 2 +-
library/global.ml | 2 +-
library/global.mli | 2 +-
library/goptions.ml | 2 +-
library/goptions.mli | 2 +-
library/goptionstyp.mli | 2 +-
library/heads.ml | 2 +-
library/heads.mli | 2 +-
library/impargs.ml | 2 +-
library/impargs.mli | 2 +-
library/lib.ml | 2 +-
library/lib.mli | 2 +-
library/libnames.ml | 2 +-
library/libnames.mli | 2 +-
library/libobject.ml | 2 +-
library/libobject.mli | 2 +-
library/library.ml | 2 +-
library/library.mli | 2 +-
library/nameops.ml | 2 +-
library/nameops.mli | 2 +-
library/nametab.ml | 2 +-
library/nametab.mli | 2 +-
library/states.ml | 2 +-
library/states.mli | 2 +-
library/summary.ml | 2 +-
library/summary.mli | 2 +-
parsing/argextend.ml4 | 2 +-
parsing/egrammar.ml | 2 +-
parsing/egrammar.mli | 2 +-
parsing/extend.ml | 2 +-
parsing/extend.mli | 2 +-
parsing/extrawit.ml | 2 +-
parsing/extrawit.mli | 2 +-
parsing/g_constr.ml4 | 2 +-
parsing/g_ltac.ml4 | 3 +-
parsing/g_prim.ml4 | 2 +-
parsing/g_proofs.ml4 | 2 +-
parsing/g_tactic.ml4 | 58 +-
parsing/g_vernac.ml4 | 19 +-
parsing/g_xml.ml4 | 2 +-
parsing/lexer.ml4 | 2 +-
parsing/lexer.mli | 2 +-
parsing/pcoq.ml4 | 2 +-
parsing/pcoq.mli | 2 +-
parsing/ppconstr.ml | 30 +-
parsing/ppconstr.mli | 9 +-
parsing/pptactic.ml | 31 +-
parsing/pptactic.mli | 2 +-
parsing/ppvernac.ml | 22 +-
parsing/ppvernac.mli | 4 +-
parsing/prettyp.ml | 14 +-
parsing/prettyp.mli | 2 +-
parsing/printer.ml | 119 +-
parsing/printer.mli | 6 +-
parsing/printmod.ml | 6 +-
parsing/printmod.mli | 2 +-
parsing/q_constr.ml4 | 2 +-
parsing/q_coqast.ml4 | 24 +-
parsing/q_util.ml4 | 2 +-
parsing/q_util.mli | 2 +-
parsing/tacextend.ml4 | 8 +-
parsing/tactic_printer.ml | 2 +-
parsing/tactic_printer.mli | 2 +-
parsing/tok.ml | 2 +-
parsing/tok.mli | 2 +-
parsing/vernacextend.ml4 | 13 +-
plugins/cc/ccalgo.ml | 2 +-
plugins/cc/ccalgo.mli | 2 +-
plugins/cc/ccproof.ml | 2 +-
plugins/cc/ccproof.mli | 2 +-
plugins/cc/cctac.ml | 8 +-
plugins/cc/cctac.mli | 2 +-
plugins/cc/g_congruence.ml4 | 2 +-
plugins/decl_mode/decl_expr.mli | 2 +-
plugins/decl_mode/decl_interp.ml | 2 +-
plugins/decl_mode/decl_interp.mli | 2 +-
plugins/decl_mode/decl_mode.ml | 2 +-
plugins/decl_mode/decl_mode.mli | 2 +-
plugins/decl_mode/decl_proof_instr.ml | 2 +-
plugins/decl_mode/decl_proof_instr.mli | 2 +-
plugins/decl_mode/g_decl_mode.ml4 | 2 +-
plugins/decl_mode/ppdecl_proof.ml | 2 +-
plugins/extraction/ExtrOcamlBasic.v | 2 +-
plugins/extraction/ExtrOcamlBigIntConv.v | 2 +-
plugins/extraction/ExtrOcamlIntConv.v | 2 +-
plugins/extraction/ExtrOcamlNatBigInt.v | 2 +-
plugins/extraction/ExtrOcamlNatInt.v | 2 +-
plugins/extraction/ExtrOcamlString.v | 2 +-
plugins/extraction/ExtrOcamlZBigInt.v | 8 +-
plugins/extraction/ExtrOcamlZInt.v | 4 +-
plugins/extraction/big.ml | 2 +-
plugins/extraction/common.ml | 4 +-
plugins/extraction/common.mli | 2 +-
plugins/extraction/extract_env.ml | 6 +-
plugins/extraction/extract_env.mli | 2 +-
plugins/extraction/extraction.ml | 2 +-
plugins/extraction/extraction.mli | 2 +-
plugins/extraction/g_extraction.ml4 | 2 +-
plugins/extraction/haskell.ml | 2 +-
plugins/extraction/haskell.mli | 2 +-
plugins/extraction/miniml.mli | 2 +-
plugins/extraction/mlutil.ml | 2 +-
plugins/extraction/mlutil.mli | 2 +-
plugins/extraction/modutil.ml | 2 +-
plugins/extraction/modutil.mli | 2 +-
plugins/extraction/ocaml.ml | 2 +-
plugins/extraction/ocaml.mli | 2 +-
plugins/extraction/scheme.ml | 2 +-
plugins/extraction/scheme.mli | 2 +-
plugins/extraction/table.ml | 3 +-
plugins/extraction/table.mli | 2 +-
plugins/field/LegacyField.v | 2 +-
plugins/field/LegacyField_Compl.v | 2 +-
plugins/field/LegacyField_Tactic.v | 22 +-
plugins/field/LegacyField_Theory.v | 182 +-
plugins/field/field.ml4 | 2 +-
plugins/firstorder/formula.ml | 2 +-
plugins/firstorder/formula.mli | 2 +-
plugins/firstorder/g_ground.ml4 | 2 +-
plugins/firstorder/ground.ml | 2 +-
plugins/firstorder/ground.mli | 2 +-
plugins/firstorder/instances.ml | 2 +-
plugins/firstorder/instances.mli | 2 +-
plugins/firstorder/rules.ml | 2 +-
plugins/firstorder/rules.mli | 2 +-
plugins/firstorder/sequent.ml | 2 +-
plugins/firstorder/sequent.mli | 2 +-
plugins/firstorder/unify.ml | 2 +-
plugins/firstorder/unify.mli | 2 +-
plugins/fourier/Fourier.v | 2 +-
plugins/fourier/Fourier_util.v | 34 +-
plugins/fourier/fourier.ml | 2 +-
plugins/fourier/fourierR.ml | 2 +-
plugins/fourier/g_fourier.ml4 | 2 +-
plugins/funind/Recdef.v | 2 +-
plugins/funind/functional_principles_types.ml | 6 -
plugins/funind/g_indfun.ml4 | 2 +-
plugins/funind/invfun.ml | 2 +-
plugins/funind/merge.ml | 2 +-
plugins/funind/recdef.ml | 2 +-
plugins/micromega/CheckerMaker.v | 2 +-
plugins/micromega/Env.v | 153 +-
plugins/micromega/EnvRing.v | 1257 +++++--------
plugins/micromega/MExtraction.v | 4 +-
plugins/micromega/OrderedRing.v | 2 +-
plugins/micromega/Psatz.v | 8 +-
plugins/micromega/QMicromega.v | 10 +-
plugins/micromega/RMicromega.v | 30 +-
plugins/micromega/Refl.v | 2 +-
plugins/micromega/RingMicromega.v | 50 +-
plugins/micromega/Tauto.v | 2 +-
plugins/micromega/VarMap.v | 2 +-
plugins/micromega/ZCoeff.v | 16 +-
plugins/micromega/ZMicromega.v | 216 ++-
plugins/micromega/certificate.ml | 2 +-
plugins/micromega/coq_micromega.ml | 23 +-
plugins/micromega/csdpcert.ml | 2 +-
plugins/micromega/g_micromega.ml4 | 2 +-
plugins/micromega/mutils.ml | 2 +-
plugins/micromega/persistent_cache.ml | 32 +-
plugins/micromega/polynomial.ml | 2 +-
plugins/micromega/sos.mli | 2 +-
plugins/micromega/sos_types.ml | 2 +-
plugins/nsatz/Nsatz.v | 40 +-
plugins/nsatz/ideal.ml | 2 +-
plugins/nsatz/nsatz.ml4 | 2 +-
plugins/nsatz/polynom.ml | 2 +-
plugins/nsatz/polynom.mli | 2 +-
plugins/omega/Omega.v | 8 +-
plugins/omega/OmegaLemmas.v | 266 ++-
plugins/omega/OmegaPlugin.v | 2 +-
plugins/omega/PreOmega.v | 353 ++--
plugins/omega/coq_omega.ml | 59 +-
plugins/omega/g_omega.ml4 | 2 +-
plugins/omega/omega.ml | 2 +-
plugins/quote/Quote.v | 4 +-
plugins/quote/g_quote.ml4 | 2 +-
plugins/quote/quote.ml | 2 +-
plugins/ring/LegacyArithRing.v | 8 +-
plugins/ring/LegacyNArithRing.v | 25 +-
plugins/ring/LegacyRing.v | 6 +-
plugins/ring/LegacyRing_theory.v | 42 +-
plugins/ring/LegacyZArithRing.v | 8 +-
plugins/ring/Ring_abstract.v | 90 +-
plugins/ring/Ring_normalize.v | 142 +-
plugins/ring/Setoid_ring.v | 2 +-
plugins/ring/Setoid_ring_normalize.v | 122 +-
plugins/ring/Setoid_ring_theory.v | 4 +-
plugins/ring/g_ring.ml4 | 2 +-
plugins/ring/ring.ml | 8 +-
plugins/romega/ReflOmegaCore.v | 505 +++--
plugins/rtauto/Bintree.v | 16 +-
plugins/rtauto/Rtauto.v | 2 +-
plugins/rtauto/g_rtauto.ml4 | 2 +-
plugins/rtauto/proof_search.ml | 2 +-
plugins/rtauto/proof_search.mli | 2 +-
plugins/rtauto/refl_tauto.ml | 4 +-
plugins/rtauto/refl_tauto.mli | 2 +-
plugins/setoid_ring/ArithRing.v | 10 +-
plugins/setoid_ring/BinList.v | 77 +-
plugins/setoid_ring/Cring.v | 27 +-
plugins/setoid_ring/Field.v | 2 +-
plugins/setoid_ring/Field_tac.v | 6 +-
plugins/setoid_ring/Field_theory.v | 415 ++---
plugins/setoid_ring/InitialRing.v | 108 +-
plugins/setoid_ring/Integral_domain.v | 5 +-
plugins/setoid_ring/NArithRing.v | 2 +-
plugins/setoid_ring/Ncring.v | 35 +-
plugins/setoid_ring/Ncring_initial.v | 56 +-
plugins/setoid_ring/Ncring_polynom.v | 111 +-
plugins/setoid_ring/Ncring_tac.v | 10 +-
plugins/setoid_ring/RealField.v | 64 +-
plugins/setoid_ring/Ring.v | 4 +-
plugins/setoid_ring/Ring_base.v | 2 +-
plugins/setoid_ring/Ring_polynom.v | 1310 +++++--------
plugins/setoid_ring/Ring_tac.v | 7 +-
plugins/setoid_ring/Ring_theory.v | 293 ++-
plugins/setoid_ring/Rings_Z.v | 2 +-
plugins/setoid_ring/ZArithRing.v | 6 +-
plugins/setoid_ring/newring.ml4 | 2 +-
plugins/subtac/eterm.mli | 2 +-
plugins/subtac/g_subtac.ml4 | 2 +-
plugins/subtac/subtac.ml | 2 +-
plugins/subtac/subtac_cases.ml | 2 +-
plugins/subtac/subtac_cases.mli | 2 +-
plugins/subtac/subtac_classes.ml | 2 +-
plugins/subtac/subtac_classes.mli | 2 +-
plugins/subtac/subtac_coercion.ml | 2 +-
plugins/subtac/subtac_command.ml | 9 +-
plugins/subtac/subtac_pretyping.ml | 2 +-
plugins/subtac/subtac_pretyping_F.ml | 2 +-
plugins/syntax/nat_syntax.ml | 6 +-
plugins/syntax/numbers_syntax.ml | 96 +-
plugins/syntax/r_syntax.ml | 2 +-
plugins/syntax/z_syntax.ml | 2 +-
plugins/xml/dumptree.ml4 | 2 +-
pretyping/arguments_renaming.ml | 2 +-
pretyping/arguments_renaming.mli | 2 +-
pretyping/cases.ml | 2 +-
pretyping/cases.mli | 2 +-
pretyping/cbv.ml | 2 +-
pretyping/cbv.mli | 2 +-
pretyping/classops.ml | 2 +-
pretyping/classops.mli | 2 +-
pretyping/coercion.ml | 2 +-
pretyping/coercion.mli | 2 +-
pretyping/detyping.ml | 2 +-
pretyping/detyping.mli | 2 +-
pretyping/evarconv.ml | 36 +-
pretyping/evarconv.mli | 2 +-
pretyping/evarutil.ml | 85 +-
pretyping/evarutil.mli | 24 +-
pretyping/evd.ml | 2 +-
pretyping/evd.mli | 2 +-
pretyping/glob_term.ml | 2 +-
pretyping/glob_term.mli | 2 +-
pretyping/indrec.ml | 2 +-
pretyping/indrec.mli | 2 +-
pretyping/inductiveops.ml | 2 +-
pretyping/inductiveops.mli | 2 +-
pretyping/matching.ml | 2 +-
pretyping/matching.mli | 2 +-
pretyping/namegen.ml | 2 +-
pretyping/namegen.mli | 2 +-
pretyping/pattern.ml | 2 +-
pretyping/pattern.mli | 2 +-
pretyping/pretype_errors.ml | 2 +-
pretyping/pretype_errors.mli | 2 +-
pretyping/pretyping.ml | 16 +-
pretyping/pretyping.mli | 2 +-
pretyping/recordops.ml | 2 +-
pretyping/recordops.mli | 2 +-
pretyping/reductionops.ml | 2 +-
pretyping/reductionops.mli | 2 +-
pretyping/retyping.ml | 2 +-
pretyping/retyping.mli | 2 +-
pretyping/tacred.ml | 2 +-
pretyping/tacred.mli | 2 +-
pretyping/term_dnet.ml | 2 +-
pretyping/term_dnet.mli | 2 +-
pretyping/termops.ml | 2 +-
pretyping/termops.mli | 2 +-
pretyping/typeclasses.ml | 2 +-
pretyping/typeclasses.mli | 2 +-
pretyping/typeclasses_errors.ml | 2 +-
pretyping/typeclasses_errors.mli | 2 +-
pretyping/typing.ml | 2 +-
pretyping/typing.mli | 2 +-
pretyping/unification.ml | 26 +-
pretyping/unification.mli | 2 +-
pretyping/vnorm.ml | 2 +-
pretyping/vnorm.mli | 2 +-
proofs/clenv.ml | 2 +-
proofs/clenv.mli | 2 +-
proofs/clenvtac.ml | 6 +-
proofs/clenvtac.mli | 2 +-
proofs/evar_refiner.ml | 2 +-
proofs/evar_refiner.mli | 2 +-
proofs/goal.ml | 2 +-
proofs/goal.mli | 2 +-
proofs/logic.ml | 2 +-
proofs/logic.mli | 2 +-
proofs/pfedit.ml | 5 +-
proofs/pfedit.mli | 2 +-
proofs/proof.ml | 18 +-
proofs/proof.mli | 11 +-
proofs/proof_global.ml | 2 +-
proofs/proof_global.mli | 2 +-
proofs/proof_type.ml | 2 +-
proofs/proof_type.mli | 2 +-
proofs/proofview.ml | 7 +-
proofs/proofview.mli | 20 +-
proofs/redexpr.ml | 2 +-
proofs/redexpr.mli | 2 +-
proofs/refiner.ml | 2 +-
proofs/refiner.mli | 2 +-
proofs/tacexpr.ml | 14 +-
proofs/tacmach.ml | 2 +-
proofs/tacmach.mli | 2 +-
proofs/tactic_debug.ml | 2 +-
proofs/tactic_debug.mli | 2 +-
scripts/coqc.ml | 2 +-
scripts/coqmktop.ml | 41 +-
states/MakeInitial.v | 2 +-
tactics/auto.ml | 26 +-
tactics/auto.mli | 2 +-
tactics/autorewrite.ml | 2 +-
tactics/autorewrite.mli | 2 +-
tactics/btermdn.ml | 2 +-
tactics/btermdn.mli | 2 +-
tactics/class_tactics.ml4 | 2 +-
tactics/contradiction.ml | 2 +-
tactics/contradiction.mli | 2 +-
tactics/eauto.ml4 | 2 +-
tactics/eauto.mli | 2 +-
tactics/elim.ml | 2 +-
tactics/elim.mli | 2 +-
tactics/elimschemes.ml | 2 +-
tactics/elimschemes.mli | 2 +-
tactics/eqdecide.ml4 | 2 +-
tactics/eqschemes.ml | 2 +-
tactics/eqschemes.mli | 2 +-
tactics/equality.ml | 2 +-
tactics/equality.mli | 2 +-
tactics/evar_tactics.ml | 2 +-
tactics/evar_tactics.mli | 2 +-
tactics/extraargs.ml4 | 2 +-
tactics/extraargs.mli | 2 +-
tactics/extratactics.ml4 | 8 +-
tactics/extratactics.mli | 2 +-
tactics/hiddentac.ml | 25 +-
tactics/hiddentac.mli | 21 +-
tactics/hipattern.ml4 | 2 +-
tactics/hipattern.mli | 2 +-
tactics/inv.ml | 2 +-
tactics/inv.mli | 2 +-
tactics/leminv.ml | 2 +-
tactics/nbtermdn.ml | 2 +-
tactics/nbtermdn.mli | 2 +-
tactics/refine.ml | 2 +-
tactics/refine.mli | 2 +-
tactics/rewrite.ml4 | 247 ++-
tactics/tacinterp.ml | 65 +-
tactics/tacinterp.mli | 3 +-
tactics/tactic_option.ml | 2 +-
tactics/tactic_option.mli | 2 +-
tactics/tacticals.ml | 2 +-
tactics/tacticals.mli | 2 +-
tactics/tactics.ml | 21 +-
tactics/tactics.mli | 6 +-
tactics/tauto.ml4 | 2 +-
tactics/termdn.ml | 2 +-
tactics/termdn.mli | 2 +-
test-suite/bench/lists-100.v | 2 +-
test-suite/bench/lists_100.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1414.v | 4 +-
test-suite/bugs/closed/shouldsucceed/1784.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1844.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1935.v | 2 +-
test-suite/bugs/closed/shouldsucceed/2127.v | 4 +-
test-suite/bugs/closed/shouldsucceed/2817.v | 9 +
test-suite/bugs/closed/shouldsucceed/2836.v | 39 +
test-suite/complexity/ring2.v | 7 +-
test-suite/failure/Tauto.v | 2 +-
test-suite/failure/Uminus.v | 4 +-
test-suite/failure/clash_cons.v | 2 +-
test-suite/failure/fixpoint1.v | 2 +-
test-suite/failure/guard.v | 2 +-
test-suite/failure/illtype1.v | 2 +-
test-suite/failure/pattern.v | 2 +-
test-suite/failure/positivity.v | 2 +-
test-suite/failure/redef.v | 2 +-
test-suite/failure/search.v | 2 +-
test-suite/failure/subtyping2.v | 20 +-
test-suite/failure/universes-buraliforti-redef.v | 20 +-
test-suite/failure/universes-buraliforti.v | 20 +-
test-suite/ideal-features/Apply.v | 2 +-
test-suite/ideal-features/eapply_evar.v | 2 +-
test-suite/micromega/example.v | 10 +-
test-suite/micromega/square.v | 18 +-
test-suite/misc/berardi_test.v | 14 +-
test-suite/modules/PO.v | 4 +-
test-suite/modules/Przyklad.v | 14 +-
test-suite/output/Notations.out | 5 +
test-suite/output/Notations.v | 9 +
test-suite/output/ZSyntax.out | 14 +-
test-suite/success/Check.v | 2 +-
test-suite/success/Field.v | 2 +-
test-suite/success/Funind.v | 22 +-
test-suite/success/Hints.v | 26 +-
test-suite/success/LegacyField.v | 2 +-
test-suite/success/MatchFail.v | 4 +-
test-suite/success/Mod_type.v | 12 +
test-suite/success/Notations.v | 5 +
test-suite/success/OmegaPre.v | 16 +-
test-suite/success/ProgramWf.v | 6 +-
test-suite/success/ROmegaPre.v | 16 +-
test-suite/success/RecTutorial.v | 10 +-
test-suite/success/Reg.v | 8 +-
test-suite/success/Scopes.v | 2 +-
test-suite/success/Tauto.v | 2 +-
test-suite/success/TestRefine.v | 2 +-
test-suite/success/Try.v | 2 +-
test-suite/success/apply.v | 6 +-
test-suite/success/change.v | 6 +-
test-suite/success/decl_mode.v | 10 +-
test-suite/success/dependentind.v | 2 +-
test-suite/success/eauto.v | 2 +-
test-suite/success/eqdecide.v | 2 +-
test-suite/success/extraction.v | 2 +-
test-suite/success/fix.v | 8 +-
test-suite/success/inds_type_sec.v | 2 +-
test-suite/success/induct.v | 2 +-
test-suite/success/ltac.v | 8 +-
test-suite/success/mutual_ind.v | 2 +-
test-suite/success/proof_using.v | 6 +
test-suite/success/remember.v | 2 +-
test-suite/success/searchabout.v | 2 +-
test-suite/success/setoid_test.v | 20 +-
test-suite/success/specialize.v | 28 +-
test-suite/success/unfold.v | 2 +-
test-suite/success/unicode_utf8.v | 2 +-
test-suite/success/univers.v | 4 +-
test-suite/typeclasses/NewSetoid.v | 2 +-
theories/Arith/Arith.v | 2 +-
theories/Arith/Arith_base.v | 2 +-
theories/Arith/Between.v | 8 +-
theories/Arith/Bool_nat.v | 4 +-
theories/Arith/Compare.v | 8 +-
theories/Arith/Compare_dec.v | 10 +-
theories/Arith/Div2.v | 18 +-
theories/Arith/EqNat.v | 18 +-
theories/Arith/Euclid.v | 20 +-
theories/Arith/Even.v | 6 +-
theories/Arith/Factorial.v | 8 +-
theories/Arith/Gt.v | 16 +-
theories/Arith/Le.v | 8 +-
theories/Arith/Lt.v | 12 +-
theories/Arith/Max.v | 2 +-
theories/Arith/Min.v | 4 +-
theories/Arith/Minus.v | 32 +-
theories/Arith/Mult.v | 24 +-
theories/Arith/Peano_dec.v | 6 +-
theories/Arith/Plus.v | 32 +-
theories/Arith/Wf_nat.v | 22 +-
theories/Bool/Bool.v | 8 +-
theories/Bool/BoolEq.v | 6 +-
theories/Bool/Bvector.v | 4 +-
theories/Bool/DecBool.v | 2 +-
theories/Bool/IfProp.v | 2 +-
theories/Bool/Sumbool.v | 2 +-
theories/Bool/Zerob.v | 4 +-
theories/Classes/EquivDec.v | 4 +-
theories/Classes/Equivalence.v | 6 +-
theories/Classes/Init.v | 2 +-
theories/Classes/Morphisms.v | 4 +-
theories/Classes/Morphisms_Prop.v | 2 +-
theories/Classes/Morphisms_Relations.v | 2 +-
theories/Classes/RelationClasses.v | 4 +-
theories/Classes/SetoidClass.v | 2 +-
theories/Classes/SetoidDec.v | 4 +-
theories/Classes/SetoidTactics.v | 4 +-
theories/FSets/FMapAVL.v | 20 +-
theories/FSets/FMapFullAVL.v | 4 +-
theories/FSets/FMapPositive.v | 2 +-
theories/FSets/FSetBridge.v | 148 +-
theories/FSets/FSetEqProperties.v | 8 +-
theories/FSets/FSetFacts.v | 6 +-
theories/FSets/FSetProperties.v | 2 +-
theories/Init/Datatypes.v | 24 +-
theories/Init/Logic.v | 24 +-
theories/Init/Logic_Type.v | 12 +-
theories/Init/Notations.v | 2 +-
theories/Init/Peano.v | 26 +-
theories/Init/Prelude.v | 2 +-
theories/Init/Specif.v | 28 +-
theories/Init/Tactics.v | 12 +-
theories/Init/Wf.v | 4 +-
theories/Lists/List.v | 48 +-
theories/Lists/ListSet.v | 78 +-
theories/Lists/ListTactics.v | 4 +-
theories/Lists/SetoidList.v | 90 +-
theories/Lists/SetoidPermutation.v | 125 ++
theories/Lists/StreamMemo.v | 29 +-
theories/Lists/Streams.v | 14 +-
theories/Lists/vo.itarget | 1 +
theories/Logic/Berardi.v | 14 +-
theories/Logic/ChoiceFacts.v | 6 +-
theories/Logic/Classical.v | 2 +-
theories/Logic/ClassicalChoice.v | 2 +-
theories/Logic/ClassicalDescription.v | 4 +-
theories/Logic/ClassicalEpsilon.v | 2 +-
theories/Logic/ClassicalFacts.v | 38 +-
theories/Logic/ClassicalUniqueChoice.v | 2 +-
theories/Logic/Classical_Pred_Set.v | 2 +-
theories/Logic/Classical_Pred_Type.v | 10 +-
theories/Logic/Classical_Prop.v | 10 +-
theories/Logic/Classical_Type.v | 2 +-
theories/Logic/ConstructiveEpsilon.v | 6 +-
theories/Logic/Decidable.v | 2 +-
theories/Logic/Description.v | 2 +-
theories/Logic/Diaconescu.v | 16 +-
theories/Logic/Epsilon.v | 2 +-
theories/Logic/Eqdep.v | 2 +-
theories/Logic/EqdepFacts.v | 14 +-
theories/Logic/Eqdep_dec.v | 32 +-
theories/Logic/ExtensionalityFacts.v | 2 +-
theories/Logic/FunctionalExtensionality.v | 2 +-
theories/Logic/Hurkens.v | 6 +-
theories/Logic/IndefiniteDescription.v | 2 +-
theories/Logic/JMeq.v | 2 +-
theories/Logic/ProofIrrelevance.v | 2 +-
theories/Logic/ProofIrrelevanceFacts.v | 4 +-
theories/Logic/RelationalChoice.v | 2 +-
theories/Logic/SetIsType.v | 2 +-
theories/MSets/MSetEqProperties.v | 8 +-
theories/MSets/MSetInterface.v | 2 +-
theories/MSets/MSetList.v | 6 +-
theories/MSets/MSetPositive.v | 4 +-
theories/MSets/MSetProperties.v | 2 +-
theories/MSets/MSetRBT.v | 104 +-
theories/MSets/MSetWeakList.v | 6 +-
theories/NArith/BinNat.v | 220 +--
theories/NArith/BinNatDef.v | 94 +-
theories/NArith/NArith.v | 2 +-
theories/NArith/Ndec.v | 443 ++---
theories/NArith/Ndigits.v | 207 +--
theories/NArith/Ndist.v | 104 +-
theories/NArith/Ndiv_def.v | 14 +-
theories/NArith/Ngcd_def.v | 2 +-
theories/NArith/Nnat.v | 56 +-
theories/NArith/Nsqrt_def.v | 12 +-
theories/Numbers/BigNumPrelude.v | 163 +-
theories/Numbers/BinNums.v | 2 +-
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 46 +-
theories/Numbers/Cyclic/Abstract/NZCyclic.v | 14 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 50 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 115 +-
.../Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 30 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 272 +--
theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 80 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 186 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 88 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 393 ++--
theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v | 26 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 4 +-
theories/Numbers/Cyclic/Int31/Cyclic31.v | 609 +++---
theories/Numbers/Cyclic/Int31/Int31.v | 18 +-
theories/Numbers/Cyclic/Int31/Ring31.v | 4 +-
theories/Numbers/Cyclic/ZModulo/ZModulo.v | 191 +-
theories/Numbers/Integer/Abstract/ZAdd.v | 2 +-
theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 +-
theories/Numbers/Integer/Abstract/ZAxioms.v | 2 +-
theories/Numbers/Integer/Abstract/ZBase.v | 2 +-
theories/Numbers/Integer/Abstract/ZBits.v | 4 +-
theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +-
theories/Numbers/Integer/Abstract/ZDivFloor.v | 4 +-
theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +-
theories/Numbers/Integer/Abstract/ZGcd.v | 2 +-
theories/Numbers/Integer/Abstract/ZLcm.v | 2 +-
theories/Numbers/Integer/Abstract/ZLt.v | 2 +-
theories/Numbers/Integer/Abstract/ZMaxMin.v | 2 +-
theories/Numbers/Integer/Abstract/ZMul.v | 2 +-
theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 +-
theories/Numbers/Integer/Abstract/ZParity.v | 2 +-
theories/Numbers/Integer/Abstract/ZPow.v | 13 +-
theories/Numbers/Integer/Abstract/ZProperties.v | 2 +-
theories/Numbers/Integer/Abstract/ZSgnAbs.v | 2 +-
theories/Numbers/Integer/BigZ/BigZ.v | 10 +-
theories/Numbers/Integer/BigZ/ZMake.v | 454 ++---
theories/Numbers/Integer/Binary/ZBinary.v | 4 +-
theories/Numbers/Integer/NatPairs/ZNatPairs.v | 4 +-
theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 +-
theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 6 +-
theories/Numbers/NaryFunctions.v | 2 +-
theories/Numbers/NatInt/NZAdd.v | 2 +-
theories/Numbers/NatInt/NZAddOrder.v | 2 +-
theories/Numbers/NatInt/NZAxioms.v | 4 +-
theories/Numbers/NatInt/NZBase.v | 2 +-
theories/Numbers/NatInt/NZBits.v | 2 +-
theories/Numbers/NatInt/NZDiv.v | 2 +-
theories/Numbers/NatInt/NZDomain.v | 2 +-
theories/Numbers/NatInt/NZGcd.v | 2 +-
theories/Numbers/NatInt/NZLog.v | 2 +-
theories/Numbers/NatInt/NZMul.v | 2 +-
theories/Numbers/NatInt/NZMulOrder.v | 6 +-
theories/Numbers/NatInt/NZOrder.v | 2 +-
theories/Numbers/NatInt/NZParity.v | 2 +-
theories/Numbers/NatInt/NZPow.v | 2 +-
theories/Numbers/NatInt/NZProperties.v | 2 +-
theories/Numbers/NatInt/NZSqrt.v | 2 +-
theories/Numbers/Natural/Abstract/NAdd.v | 2 +-
theories/Numbers/Natural/Abstract/NAddOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NAxioms.v | 2 +-
theories/Numbers/Natural/Abstract/NBase.v | 2 +-
theories/Numbers/Natural/Abstract/NBits.v | 4 +-
theories/Numbers/Natural/Abstract/NDefOps.v | 4 +-
theories/Numbers/Natural/Abstract/NDiv.v | 2 +-
theories/Numbers/Natural/Abstract/NGcd.v | 2 +-
theories/Numbers/Natural/Abstract/NIso.v | 2 +-
theories/Numbers/Natural/Abstract/NLcm.v | 2 +-
theories/Numbers/Natural/Abstract/NLog.v | 2 +-
theories/Numbers/Natural/Abstract/NMaxMin.v | 2 +-
theories/Numbers/Natural/Abstract/NMulOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NParity.v | 2 +-
theories/Numbers/Natural/Abstract/NPow.v | 2 +-
theories/Numbers/Natural/Abstract/NProperties.v | 2 +-
theories/Numbers/Natural/Abstract/NSqrt.v | 2 +-
theories/Numbers/Natural/Abstract/NStrongRec.v | 2 +-
theories/Numbers/Natural/Abstract/NSub.v | 2 +-
theories/Numbers/Natural/BigN/BigN.v | 4 +-
theories/Numbers/Natural/BigN/NMake.v | 364 ++--
theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +-
theories/Numbers/Natural/BigN/Nbasic.v | 120 +-
theories/Numbers/Natural/Binary/NBinary.v | 6 +-
theories/Numbers/Natural/Peano/NPeano.v | 2 +-
theories/Numbers/Natural/SpecViaZ/NSig.v | 2 +-
theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 10 +-
theories/Numbers/NumPrelude.v | 2 +-
theories/Numbers/Rational/BigQ/BigQ.v | 10 +-
theories/Numbers/Rational/BigQ/QMake.v | 485 +++--
theories/Numbers/Rational/SpecViaQ/QSig.v | 2 +-
theories/PArith/BinPos.v | 364 ++--
theories/PArith/BinPosDef.v | 5 +-
theories/PArith/PArith.v | 2 +-
theories/PArith/POrderedType.v | 2 +-
theories/PArith/Pnat.v | 81 +-
theories/Program/Basics.v | 4 +-
theories/Program/Combinators.v | 2 +-
theories/Program/Equality.v | 12 +-
theories/Program/Program.v | 2 +-
theories/Program/Subset.v | 6 +-
theories/Program/Syntax.v | 2 +-
theories/Program/Tactics.v | 4 +-
theories/Program/Utils.v | 2 +-
theories/Program/Wf.v | 6 +-
theories/QArith/QArith.v | 2 +-
theories/QArith/QArith_base.v | 255 ++-
theories/QArith/QOrderedType.v | 2 +-
theories/QArith/Qabs.v | 26 +-
theories/QArith/Qcanon.v | 22 +-
theories/QArith/Qfield.v | 6 +-
theories/QArith/Qminmax.v | 2 +-
theories/QArith/Qpower.v | 88 +-
theories/QArith/Qreals.v | 62 +-
theories/QArith/Qreduction.v | 166 +-
theories/QArith/Qring.v | 2 +-
theories/QArith/Qround.v | 26 +-
theories/Reals/Alembert.v | 254 +--
theories/Reals/AltSeries.v | 122 +-
theories/Reals/ArithProp.v | 50 +-
theories/Reals/Binomial.v | 68 +-
theories/Reals/Cauchy_prod.v | 28 +-
theories/Reals/Cos_plus.v | 194 +-
theories/Reals/Cos_rel.v | 92 +-
theories/Reals/DiscrR.v | 10 +-
theories/Reals/Exp_prop.v | 230 ++-
theories/Reals/Integration.v | 2 +-
theories/Reals/LegacyRfield.v | 6 +-
theories/Reals/MVT.v | 102 +-
theories/Reals/Machin.v | 168 ++
theories/Reals/NewtonInt.v | 158 +-
theories/Reals/PSeries_reg.v | 62 +-
theories/Reals/PartSum.v | 142 +-
theories/Reals/RIneq.v | 266 +--
theories/Reals/RList.v | 232 +--
theories/Reals/ROrderedType.v | 2 +-
theories/Reals/R_Ifp.v | 80 +-
theories/Reals/R_sqr.v | 36 +-
theories/Reals/R_sqrt.v | 56 +-
theories/Reals/Ranalysis.v | 775 +-------
theories/Reals/Ranalysis1.v | 362 ++--
theories/Reals/Ranalysis2.v | 92 +-
theories/Reals/Ranalysis3.v | 162 +-
theories/Reals/Ranalysis4.v | 106 +-
theories/Reals/Ranalysis5.v | 1348 ++++++++++++++
theories/Reals/Ranalysis_reg.v | 800 ++++++++
theories/Reals/Ratan.v | 1602 ++++++++++++++++
theories/Reals/Raxioms.v | 8 +-
theories/Reals/Rbase.v | 2 +-
theories/Reals/Rbasic_fun.v | 102 +-
theories/Reals/Rcomplete.v | 50 +-
theories/Reals/Rdefinitions.v | 4 +-
theories/Reals/Rderiv.v | 114 +-
theories/Reals/Reals.v | 2 +-
theories/Reals/Rfunctions.v | 119 +-
theories/Reals/Rgeom.v | 32 +-
theories/Reals/RiemannInt.v | 898 ++++-----
theories/Reals/RiemannInt_SF.v | 954 +++++-----
theories/Reals/Rlimit.v | 106 +-
theories/Reals/Rlogic.v | 10 +-
theories/Reals/Rminmax.v | 2 +-
theories/Reals/Rpow_def.v | 2 +-
theories/Reals/Rpower.v | 168 +-
theories/Reals/Rprod.v | 20 +-
theories/Reals/Rseries.v | 44 +-
theories/Reals/Rsigma.v | 34 +-
theories/Reals/Rsqrt_def.v | 216 +--
theories/Reals/Rtopology.v | 694 +++----
theories/Reals/Rtrigo.v | 1796 +-----------------
theories/Reals/Rtrigo1.v | 1933 ++++++++++++++++++++
theories/Reals/Rtrigo_alt.v | 163 +-
theories/Reals/Rtrigo_calc.v | 112 +-
theories/Reals/Rtrigo_def.v | 108 +-
theories/Reals/Rtrigo_fun.v | 30 +-
theories/Reals/Rtrigo_reg.v | 308 +---
theories/Reals/SeqProp.v | 270 +--
theories/Reals/SeqSeries.v | 98 +-
theories/Reals/SplitAbsolu.v | 4 +-
theories/Reals/SplitRmult.v | 2 +-
theories/Reals/Sqrt_reg.v | 150 +-
theories/Reals/vo.itarget | 5 +
theories/Relations/Operators_Properties.v | 8 +-
theories/Relations/Relation_Definitions.v | 2 +-
theories/Relations/Relation_Operators.v | 8 +-
theories/Relations/Relations.v | 8 +-
theories/Setoids/Setoid.v | 2 +-
theories/Sets/Classical_sets.v | 18 +-
theories/Sets/Constructive_sets.v | 18 +-
theories/Sets/Cpo.v | 2 +-
theories/Sets/Ensembles.v | 2 +-
theories/Sets/Finite_sets.v | 6 +-
theories/Sets/Finite_sets_facts.v | 20 +-
theories/Sets/Image.v | 12 +-
theories/Sets/Infinite_sets.v | 14 +-
theories/Sets/Integers.v | 24 +-
theories/Sets/Multiset.v | 18 +-
theories/Sets/Partial_Order.v | 20 +-
theories/Sets/Permut.v | 2 +-
theories/Sets/Powerset.v | 28 +-
theories/Sets/Powerset_Classical_facts.v | 42 +-
theories/Sets/Powerset_facts.v | 36 +-
theories/Sets/Relations_1.v | 2 +-
theories/Sets/Relations_1_facts.v | 20 +-
theories/Sets/Relations_2.v | 2 +-
theories/Sets/Relations_2_facts.v | 14 +-
theories/Sets/Relations_3.v | 2 +-
theories/Sets/Relations_3_facts.v | 28 +-
theories/Sets/Uniset.v | 30 +-
theories/Sorting/Heap.v | 22 +-
theories/Sorting/Mergesort.v | 4 +-
theories/Sorting/PermutEq.v | 2 +-
theories/Sorting/PermutSetoid.v | 12 +-
theories/Sorting/Permutation.v | 2 +-
theories/Sorting/Sorted.v | 2 +-
theories/Sorting/Sorting.v | 2 +-
theories/Strings/Ascii.v | 16 +-
theories/Strings/String.v | 130 +-
theories/Structures/DecidableTypeEx.v | 6 +-
theories/Structures/OrderedTypeEx.v | 160 +-
theories/Structures/OrdersAlt.v | 6 +-
theories/Unicode/Utf8.v | 4 +-
theories/Unicode/Utf8_core.v | 2 +-
theories/Vectors/VectorDef.v | 2 +-
theories/Wellfounded/Disjoint_Union.v | 4 +-
theories/Wellfounded/Inclusion.v | 4 +-
theories/Wellfounded/Inverse_Image.v | 6 +-
.../Wellfounded/Lexicographic_Exponentiation.v | 28 +-
theories/Wellfounded/Lexicographic_Product.v | 10 +-
theories/Wellfounded/Transitive_Closure.v | 6 +-
theories/Wellfounded/Union.v | 6 +-
theories/Wellfounded/Well_Ordering.v | 8 +-
theories/Wellfounded/Wellfounded.v | 2 +-
theories/ZArith/BinInt.v | 804 ++++----
theories/ZArith/BinIntDef.v | 253 +--
theories/ZArith/Int.v | 16 +-
theories/ZArith/Wf_Z.v | 12 +-
theories/ZArith/ZArith.v | 2 +-
theories/ZArith/ZArith_base.v | 2 +-
theories/ZArith/ZArith_dec.v | 93 +-
theories/ZArith/Zabs.v | 56 +-
theories/ZArith/Zbool.v | 16 +-
theories/ZArith/Zcompare.v | 34 +-
theories/ZArith/Zcomplements.v | 14 +-
theories/ZArith/Zdigits.v | 58 +-
theories/ZArith/Zdiv.v | 86 +-
theories/ZArith/Zeuclid.v | 2 +-
theories/ZArith/Zeven.v | 22 +-
theories/ZArith/Zgcd_alt.v | 241 ++-
theories/ZArith/Zhints.v | 95 +-
theories/ZArith/Zlogarithm.v | 104 +-
theories/ZArith/Zmax.v | 121 +-
theories/ZArith/Zmin.v | 92 +-
theories/ZArith/Zminmax.v | 16 +-
theories/ZArith/Zmisc.v | 11 +-
theories/ZArith/Znat.v | 162 +-
theories/ZArith/Znumtheory.v | 385 ++--
theories/ZArith/Zorder.v | 100 +-
theories/ZArith/Zpow_alt.v | 4 +-
theories/ZArith/Zpow_def.v | 14 +-
theories/ZArith/Zpow_facts.v | 42 +-
theories/ZArith/Zpower.v | 14 +-
theories/ZArith/Zquot.v | 351 ++--
theories/ZArith/Zsqrt_compat.v | 63 +-
theories/ZArith/Zwf.v | 27 +-
theories/ZArith/auxiliary.v | 2 +-
tools/compat5.ml | 2 +-
tools/compat5.mlp | 2 +-
tools/compat5b.ml | 2 +-
tools/compat5b.mlp | 2 +-
tools/coq_makefile.ml | 6 +-
tools/coq_tex.ml4 | 2 +-
tools/coqdep.ml | 2 +-
tools/coqdep_boot.ml | 2 +-
tools/coqdep_common.ml | 2 +-
tools/coqdep_common.mli | 2 +-
tools/coqdep_lexer.mli | 2 +-
tools/coqdep_lexer.mll | 2 +-
tools/coqdoc/alpha.ml | 2 +-
tools/coqdoc/alpha.mli | 2 +-
tools/coqdoc/cdglobals.ml | 2 +-
tools/coqdoc/cpretty.mli | 2 +-
tools/coqdoc/cpretty.mll | 71 +-
tools/coqdoc/index.ml | 13 +-
tools/coqdoc/index.mli | 2 +-
tools/coqdoc/main.ml | 2 +-
tools/coqdoc/output.ml | 151 +-
tools/coqdoc/output.mli | 13 +-
tools/coqdoc/tokens.ml | 2 +-
tools/coqdoc/tokens.mli | 2 +-
tools/coqwc.mll | 2 +-
tools/escape_string.ml | 1 +
tools/fake_ide.ml | 2 +-
tools/gallina.ml | 2 +-
tools/gallina_lexer.mll | 2 +-
tools/mingwpath.ml | 15 +
toplevel/auto_ind_decl.ml | 2 +-
toplevel/auto_ind_decl.mli | 2 +-
toplevel/autoinstance.ml | 2 +-
toplevel/autoinstance.mli | 2 +-
toplevel/backtrack.ml | 22 +-
toplevel/backtrack.mli | 10 +-
toplevel/cerrors.ml | 2 +-
toplevel/cerrors.mli | 2 +-
toplevel/class.ml | 2 +-
toplevel/class.mli | 2 +-
toplevel/classes.ml | 2 +-
toplevel/classes.mli | 2 +-
toplevel/command.ml | 9 +-
toplevel/command.mli | 2 +-
toplevel/coqinit.ml | 10 +-
toplevel/coqinit.mli | 4 +-
toplevel/coqtop.ml | 21 +-
toplevel/coqtop.mli | 2 +-
toplevel/discharge.ml | 2 +-
toplevel/discharge.mli | 2 +-
toplevel/himsg.ml | 57 +-
toplevel/himsg.mli | 2 +-
toplevel/ide_intf.ml | 43 +-
toplevel/ide_intf.mli | 2 +-
toplevel/ide_slave.ml | 45 +-
toplevel/ide_slave.mli | 2 +-
toplevel/ind_tables.ml | 2 +-
toplevel/ind_tables.mli | 2 +-
toplevel/indschemes.ml | 2 +-
toplevel/indschemes.mli | 2 +-
toplevel/interface.mli | 16 +-
toplevel/lemmas.ml | 2 +-
toplevel/lemmas.mli | 2 +-
toplevel/libtypes.ml | 2 +-
toplevel/libtypes.mli | 2 +-
toplevel/metasyntax.ml | 20 +-
toplevel/metasyntax.mli | 4 +-
toplevel/mltop.ml4 | 135 +-
toplevel/mltop.mli | 25 +-
toplevel/record.ml | 2 +-
toplevel/record.mli | 2 +-
toplevel/search.ml | 2 +-
toplevel/search.mli | 2 +-
toplevel/toplevel.ml | 2 +-
toplevel/toplevel.mli | 2 +-
toplevel/usage.ml | 4 +-
toplevel/usage.mli | 2 +-
toplevel/vernac.ml | 39 +-
toplevel/vernac.mli | 2 +-
toplevel/vernacentries.ml | 141 +-
toplevel/vernacentries.mli | 4 +-
toplevel/vernacexpr.ml | 18 +-
toplevel/vernacinterp.ml | 2 +-
toplevel/vernacinterp.mli | 2 +-
toplevel/whelp.ml4 | 2 +-
toplevel/whelp.mli | 2 +-
1107 files changed, 21802 insertions(+), 18994 deletions(-)
delete mode 100644 INSTALL.macosx
create mode 100644 TODO
delete mode 100644 config/Makefile.template
create mode 100755 dev/macosify_accel.sh
delete mode 100644 doc/refman/RefMan-sch.tex
create mode 100644 test-suite/bugs/closed/shouldsucceed/2817.v
create mode 100644 test-suite/bugs/closed/shouldsucceed/2836.v
create mode 100644 theories/Lists/SetoidPermutation.v
create mode 100644 theories/Reals/Machin.v
create mode 100644 theories/Reals/Ranalysis5.v
create mode 100644 theories/Reals/Ranalysis_reg.v
create mode 100644 theories/Reals/Ratan.v
create mode 100644 theories/Reals/Rtrigo1.v
create mode 100644 tools/escape_string.ml
create mode 100644 tools/mingwpath.ml
(limited to 'checker/check.ml')
diff --git a/.gitignore b/.gitignore
index 32a40af6..e0be678c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -63,11 +63,12 @@ doc/refman/csdp.cache
doc/refman/trace
doc/refman/Reference-Manual.pdf
doc/refman/Reference-Manual.ps
+doc/refman/Reference-Manual.html
+doc/refman/Reference-Manual.out
+doc/refman/Reference-Manual.sh
doc/refman/cover.html
doc/refman/styles.hva
-doc/refman/Reference-Manual.html
doc/common/version.tex
-doc/refman/Reference-Manual.sh
doc/refman/coqide-queries.eps
doc/refman/coqide.eps
doc/refman/euclid.ml
diff --git a/CHANGES b/CHANGES
index c245fb25..1c094584 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,29 +1,66 @@
-Changes from V8.4beta to V8.4
-=============================
+Changes from V8.4beta2 to V8.4
+==============================
+
+Vernacular commands
+
+- The "Reset" command is now supported again in files given to coqc or Load.
+- "Show Script" now indents again the displayed scripts. It can also work
+ correctly across Load'ed files if the option "Unset Atomic Load" is used.
+- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full
+ scope name (e.g. Z_scope).
+
+Notations
+
+- Most compatibility notations of the standard library are now tagged as
+ (compat xyz), where xyz is a former Coq version, for instance "8.3".
+ These notations behave as (only parsing) notations, except that they may
+ triggers warnings (or errors) when used while Coq is not in a corresponding
+ -compat mode.
+- To activate these compatibility warnings, use "Set Verbose Compat Notations"
+ or the command-line flag -verbose-compat-notations.
+- For a strict mode without these compatibility notations, use
+ "Unset Compat Notations" or the command-line flag -no-compat-notations.
+
+Tactics
+
+- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
+ or "induction" to make it generate equations in the spirit of "case_eq".
+ The former syntax "_eqn" is discontinued.
+- The name of the hypothesis introduced by tactic "remember" can be
+ set via the new syntax "remember t as x eqn:H" (wish #2489).
+
+Libraries
+
+- Reals: changed definition of PI, no more axiom about sin(PI/2).
+- SetoidPermutation: a notion of permutation for lists modulo a setoid equality.
+- BigN: fixed the ocaml code doing the parsing/printing of big numbers.
+
+Changes from V8.4beta to V8.4beta2
+==================================
Vernacular commands
-- Undo and UndoTo are now handling the proof states. They may
- perform some extra steps of backtrack to avoid states where
- the proof state is unavailable (typically a closed proof).
-- The commands Suspend and Resume have been removed.
+- Commands "Back" and "BackTo" are now handling the proof states. They may
+ perform some extra steps of backtrack to avoid states where the proof
+ state is unavailable (typically a closed proof).
+- The commands "Suspend" and "Resume" have been removed.
- A basic Show Script has been reintroduced (no indentation).
- New command "Set Parsing Explicit" for deactivating parsing (and printing)
of implicit arguments (useful for teaching).
-- New command "Grab Existential Variables" to transform the unresolved evars at
- the end of a proof into goals.
+- New command "Grab Existential Variables" to transform the unresolved evars
+ at the end of a proof into goals.
Tactics
-- Still no general "info" tactical, but new specific tactics
- info_auto, info_eauto, info_trivial which provides information
- on the proofs found by auto/eauto/trivial. Display of these
- details could also be activated by Set Info Auto/Eauto/Trivial.
-- Details on everything tried by auto/eauto/trivial during
- a proof search could be obtained by "debug auto", "debug eauto",
- "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
-- New command "r string" that interprets "idtac string" as a breakpoint
- and jumps to its next use in Ltac debugger.
+- Still no general "info" tactical, but new specific tactics info_auto,
+ info_eauto, info_trivial which provides information on the proofs found
+ by auto/eauto/trivial. Display of these details could also be activated by
+ "Set Info Auto"/"Set Info Eauto"/"Set Info Trivial".
+- Details on everything tried by auto/eauto/trivial during a proof search
+ could be obtained by "debug auto", "debug eauto", "debug trivial" or by a
+ global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial".
+- New command "r string" in Ltac debugger that interprets "idtac
+ string" in Ltac code as a breakpoint and jumps to its next use.
- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
harvey, zenon, gwhy) have been removed, since Why2 has not been
maintained for the last few years. The Why3 plugin should be a suitable
@@ -31,28 +68,28 @@ Tactics
Libraries
-- MSetRBT : a new implementation of MSets via Red-Black trees (initial
+- MSetRBT: a new implementation of MSets via Red-Black trees (initial
contribution by Andrew Appel).
-- MSetAVL : for maximal sharing with the new MSetRBT, the argument order
- of Node has changed (this should be transparent to regular MSets users).
+- MSetAVL: for maximal sharing with the new MSetRBT, the argument order
+ of Node has changed (this should be transparent to regular MSets users).
Module System
- The names of modules (and module types) are now in a fully separated
- namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+ namespace from ordinary definitions: "Definition E:=0. Module E. End E."
is now accepted.
CoqIDE
-- Coqide now supports the Restart command, and Undo (with a warning).
- Better support for Abort.
+- Coqide now supports the "Restart" command, and "Undo" (with a warning).
+ Better support for "Abort".
Changes from V8.3 to V8.4beta
=============================
Logic
-- Standard eta-conversion now supported (dependent product only). (DOC TO DO)
+- Standard eta-conversion now supported (dependent product only).
- Guard condition improvement: subterm property is propagated through beta-redex
blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x";
this allows for instance to use "rewrite ... in ..." without breaking
@@ -69,10 +106,6 @@ Specification language and notations
- Structure/Record printing can be disable by "Unset Printing Records".
In addition, it can be controlled on type by type basis using
"Add Printing Record" or "Add Printing Constructor".
-- In a pattern containing a "match", a final "| _ => _" branch could be used
- now instead of enumerating all remaining constructors. Moreover, the pattern
- "match _ with _ => _ end" now allows to match any "match". A "in" annotation
- can also be added to restrict to a precise inductive type.
- Pattern-matching compilation algorithm: in "match x, y with ... end",
possible dependencies of x (or of the indices of its type) in the type
of y are now taken into account.
@@ -81,11 +114,11 @@ Tactics
- New proof engine.
- Scripts can now be structured thanks to bullets - * + and to subgoal
- delimitation via { }. Note: for use with ProofGeneral, a cvs version of
- ProofGeneral no older than mid-July 2011 is currently required. DOC TODO.
+ delimitation via { }. Note: for use with Proof General, a cvs version of
+ Proof General no older than mid-July 2011 is currently required.
- Support for tactical "info" is suspended.
- Support for command "Show Script" is suspended.
-- New tactics constr_eq, is_evar and has_evar.
+- New tactics constr_eq, is_evar and has_evar for use in Ltac.
- Removed the two-argument variant of "decide equality".
- New experimental tactical "timeout ". Since is a time
in second for the moment, this feature should rather be avoided
@@ -98,14 +131,14 @@ Tactics
?f x y = g(x,y) (compatibility ensured by using
"Unset Tactic Pattern Unification"). It also supports (full) betaiota.
- Tactic autorewrite does no longer instantiate pre-existing
- existential variables (theoretical source of possible incompatibility).
+ existential variables (theoretical source of possible incompatibilities).
- Tactic "dependent rewrite" now supports equality in "sig".
- Tactic omega now understands Zpred (wish #1912) and can prove any goal
from a context containing an arithmetical contradiction (wish #2236).
- Using "auto with nocore" disables the use of the "core" database (wish #2188).
This pseudo-database "nocore" can also be used with trivial and eauto.
- Tactics "set", "destruct" and "induction" accepts incomplete terms and
- use the goal to complete the pattern assuming it is no ambiguous.
+ use the goal to complete the pattern assuming it is non ambiguous.
- When used on arguments with a dependent type, tactics such as
"destruct", "induction", "case", "elim", etc. now try to abstract
automatically the dependencies over the arguments of the types
@@ -118,18 +151,25 @@ Tactics
- When applying destruct or inversion on a fixpoint hiding an inductive
type, recursive calls to the fixpoint now remain folded by default (rare
source of incompatibility generally solvable by adding a call to simpl).
-- The behavior of the simpl tactic can be tuned using the new "Arguments"
- vernacular.
+- In an ltac pattern containing a "match", a final "| _ => _" branch could be
+ used now instead of enumerating all remaining constructors. Moreover, the
+ pattern "match _ with _ => _ end" now allows to match any "match". A "in"
+ annotation can also be added to restrict to a precise inductive type.
+- The behavior of "simpl" can be tuned using the "Arguments" vernacular.
+ In particular constants can be marked so that they are always/never unfolded
+ by "simpl", or unfolded only when a set of arguments evaluates to a
+ constructor. Last one can mark a constant so that it is unfolded only if the
+ simplified term does not expose a match in head position.
Vernacular commands
- It is now mandatory to have a space (or tabulation or newline or end-of-file)
after a "." ending a sentence.
- In SearchAbout, the [ ] delimiters are now optional.
-- New command "Add/Remove Search Blacklist ..." :
+- New command "Add/Remove Search Blacklist ...":
a Search or SearchAbout or similar query will never mention lemmas
whose qualified names contain any of the declared substrings.
- The default blacklisted substrings are "_admitted" "_subproof" "Private_". DOC TODO
+ The default blacklisted substrings are "_admitted" "_subproof" "Private_".
- When the output file of "Print Universes" ends in ".dot" or ".gv",
the universe graph is printed in the DOT language, and can be
processed by Graphviz tools.
@@ -141,7 +181,11 @@ Vernacular commands
to avoid conversion at Qed time to go into a very long computation.
- New command "Show Goal ident" to display the statement of a goal, even
a closed one (available from Proof General).
-- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope".
+- Command "Proof" accept a new modifier "using" to force generalization
+ over a given list of section variables at section ending.
+- New command "Arguments" generalizing "Implicit Arguments" and
+ "Arguments Scope" and that also allows to rename the parameters of a
+ definition and to tune the behavior of the tactic "simpl".
Module System
@@ -155,8 +199,8 @@ Module System
are lower or equal than XX will be inlined.
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
- the flag "Set Inline Level ..." to set a level. TODO: DOC!
-- Print Assumptions should now handle correctly opaque modules (#2168)
+ the flag "Set Inline Level ..." to set a level.
+- Print Assumptions should now handle correctly opaque modules (#2168).
- Print Module (Type) now tries to print more details, such as types and
bodies of the module elements. Note that Print Module Type could be
used on a module to display only its interface. The option
@@ -166,9 +210,9 @@ Module System
Libraries
- Extension of the abstract part of Numbers, which now provide axiomatizations
- and results about many more integer functions, such as pow, gcd, lcm, sqrt, log2
- and bitwise functions. These functions are implemented for nat N BigN Z BigZ.
- See in particular file NPeano for new functions about nat.
+ and results about many more integer functions, such as pow, gcd, lcm, sqrt,
+ log2 and bitwise functions. These functions are implemented for nat, N, BigN,
+ Z, BigZ. See in particular file NPeano for new functions about nat.
- The definition of types positive, N, Z is now in file BinNums.v
- Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains
an internal module Z implementing the Numbers interface for integers.
@@ -207,15 +251,15 @@ Libraries
may introduce incompatibilities. In particular, the order of the arguments
for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now
comes first. By default, the power function now takes two BigN.
-- Creation of Vector, an independant library for list indiced by their length.
- Vectors' names overwrite lists' one so you shouldn't "Import" the library.
- All old names change: functions' name become the CaML one and for example
- Vcons become Vector.cons. You can use notations by importing
+- Creation of Vector, an independent library for lists indexed by their length.
+ Vectors' names overwrite lists' one so you should not "Import" the library.
+ All old names changed: function names follow the ocaml ones and, for example,
+ Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing
Vector.VectorNotations.
- Removal of TheoryList. Requiring List instead should work most of the time.
-- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
+- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
eq_rect_r (available by importing module EqNotations).
-- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument)
+- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument).
Internal infrastructure
@@ -230,8 +274,8 @@ Internal infrastructure
for both make and ocamlbuild, etc.
- Support of cross-compilation via mingw from unix toward Windows,
contact P. Letouzey for more informations.
-- new Makefile rules mli-doc to make html of mli in dev/doc/html and
- full-stdlib to get a HUGE pdf with all the stdlib.
+- New Makefile rules mli-doc to make html of mli in dev/doc/html and
+ full-stdlib to get a (huge) pdf reflecting the whole standard library.
Extraction
@@ -243,9 +287,8 @@ Extraction
- A new command "Separate Extraction cst1 cst2 ..." that mixes a
minimal extracted environment a la "Recursive Extraction" and the
production of several files (one per coq source) a la "Extraction Library".
- DOC TODO.
- New option "Set/Unset Extraction KeepSingleton" for preventing the
- extraction to optimize singleton container types. DOC TODO
+ extraction to optimize singleton container types.
- The extraction now identifies and properly rejects a particular case of
universe polymorphism it cannot handle yet (the pair (I,I) being Prop).
- Support of anonymous fields in record (#2555).
@@ -257,10 +300,9 @@ CoqIDE
(cf button "Restart Coq", ex-"Go to Start"). For allowing such
interrupts, the Windows version of coqide now requires Windows >= XP
SP1.
-- The communication between CoqIDE and Coqtop is now done via a dialect
- of XML (DOC TODO).
-- The backtrack engine of CoqIDE has been reworked, it now used the
- "Backtrack" command similarly to ProofGeneral.
+- The communication between CoqIDE and Coqtop is now done via a dialect of XML.
+- The backtrack engine of CoqIDE has been reworked, it now uses the
+ "Backtrack" command similarly to Proof General.
- The Coqide parsing of sentences has be reworked and now supports
tactic delimitation via { }.
- Coqide now accepts the Abort command (wish #2357).
@@ -274,15 +316,15 @@ Tools
- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
$XDG_DATA_DIRS/coq, and user-contribs before the standard library.
- Coq rc file has moved to $XDG_CONFIG_HOME/coq.
-- coq_makefile major cleanup.
- * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work
+- Major changes to coq_makefile:
+ * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work;
* mlihtml generates doc of mli, install-doc install the html doc in DOCDIR
- with the same policy as vo in COQLIB
+ with the same policy as vo in COQLIB;
* More variables are given by coqtop -config, others are defined only if the
users doesn't have defined them elsewhere. Consequently, generated makefile
- should work directly on any architecture.
+ should work directly on any architecture;
* Packagers can take advantage of $(DSTROOT) introduction. Installation can
- be made in $XDG_DATA_HOME/coq.
+ be made in $XDG_DATA_HOME/coq;
* -arg option allows to send option as argument to coqc.
Changes from V8.2 to V8.3
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 0849b64f..41474202 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -3,4 +3,49 @@ Potential sources of incompatibilities between Coq V8.3 and V8.4
(see also file CHANGES)
-TO BE DONE
+The main known incompatibilities between 8.3 and 8.4 are consequences
+of the following changes:
+
+- The reorganization of the library of numbers:
+
+ Several definitions have new names or are defined in modules of
+ different names, but a special care has been taken to have this
+ renaming transparent for the user thanks to compatibility notations.
+
+ However some definitions have changed, what might require some
+ adaptations. The most noticeable examples are:
+ - The "?=" notation which now bind to Pos.compare rather than former
+ Pcompare (now Pos.compare_cont).
+ - Changes in names may induce different automatically generated
+ names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
+ - Z.add has a new definition, hence, applying "simpl" on subterms of
+ its body might give different results than before.
+ - BigN.shiftl and BigN.shiftr have reversed arguments order, the
+ power function in BigN now takes two BigN.
+
+- Other changes in libraries:
+
+ - The definition of functions over "vectors" (list of fixed length)
+ have changed.
+ - TheoryList.v has been removed.
+
+- Slight changes in tactics:
+
+ - Less unfolding of fixpoints when applying destruct or inversion on
+ a fixpoint hiding an inductive type (add an extra call to simpl to
+ preserve compatibility).
+ - Less unexpected local definitions when applying "destruct"
+ (incompatibilities solvable by adapting name hypotheses).
+ - Tactic "apply" might succeed more often, e.g. by now solving
+ pattern-matching of the form ?f x y = g(x,y) (compatibility
+ ensured by using "Unset Tactic Pattern Unification"), but also
+ because it supports (full) betaiota (using "simple apply" might
+ then help).
+ - Tactic autorewrite does no longer instantiate pre-existing
+ existential variables.
+ - Tactic "info" is now available only for auto, eauto and trivial.
+
+- Miscellaneous changes:
+
+ - The command "Load" is now atomic for backtracking (use "Unset
+ Atomic Load" for compatibility).
diff --git a/INSTALL b/INSTALL
index 5ee00613..02c9eb9b 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,5 +1,5 @@
- INSTALLATION PROCEDURES FOR THE COQ V8.3 SYSTEM
+ INSTALLATION PROCEDURES FOR THE COQ V8.4 SYSTEM
-----------------------------------------------
diff --git a/INSTALL.macosx b/INSTALL.macosx
deleted file mode 100644
index cc1317b1..00000000
--- a/INSTALL.macosx
+++ /dev/null
@@ -1,20 +0,0 @@
-INSTALLATION PROCEDURE FOR THE PRECOMPILED COQ V8.1 SYSTEM UNDER MACOS X
-------------------------------------------------------------------------
-
-You can also use fink, or the MacOS X package prepared by the Coq
-team. To use the MacOS X package,:
-
-1) Download archive coq-8.1-macosx-ppc.dmg (for PowerPC-base computer)
- or coq-8.1-macosx-i386.dmg (for Pentium-based computer).
-
-2) Double-click on its icon; it mounts a disk volume named "Coq V8.1".
-
-3) Open volume "Coq 8.1" and double-click on coq-8.1.pkg to launch the
- installer (you'll need administrator permissions).
-
-4) Coq installs in /usr/local/bin, which should be in your PATH, and
- can be used from a Terminal window: the interactive toplevel is
- named coqtop and the compiler is coqc.
-
-If you have any trouble with this installation, please contact:
-coq-bugs@pauillac.inria.fr.
diff --git a/Makefile b/Makefile
index 0ff72856..bb5ec3bc 100644
--- a/Makefile
+++ b/Makefile
@@ -39,9 +39,13 @@
# File lists
###########################################################################
+# NB: due to limitations in Win32, please refrain using 'export' too much
+# to communicate between make sub-calls (in Win32, 8kb max per env variable,
+# 32kb total)
+
# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !!
-export FIND_VCS_CLAUSE:='(' \
+FIND_VCS_CLAUSE:='(' \
-name '{arch}' -o \
-name '.svn' -o \
-name '_darcs' -o \
@@ -58,8 +62,8 @@ endef
## Files in the source tree
-export YACCFILES:=$(call find, '*.mly')
-export LEXFILES := $(call find, '*.mll')
+YACCFILES:=$(call find, '*.mly')
+LEXFILES := $(call find, '*.mll')
export MLLIBFILES := $(call find, '*.mllib')
export ML4FILES := $(call find, '*.ml4')
export CFILES := $(call find, '*.c')
@@ -73,13 +77,13 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+GENML4FILES:= $(ML4FILES:.ml4=.ml)
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
scripts/tolink.ml kernel/copcodes.ml
-export GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
-export GENML4FILES:= $(ML4FILES:.ml4=.ml)
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
# NB: all files in $(GENFILES) can be created initially, while
@@ -92,12 +96,9 @@ define diff
$(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
endef
-export MLSTATICFILES := \
- $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
-export MLFILES := \
- $(sort $(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
+export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
-export MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
include Makefile.common
@@ -276,3 +277,14 @@ ifdef COQ_CONFIGURED
else
@echo "Please run ./configure first" >&2; exit 1
endif
+
+# Useful to check that the exported variables are within the win32 limits
+
+printenv:
+ @env
+ @echo
+ @echo -n "Maxsize (win32 limit is 8k) : "
+ @env | wc -L
+ @echo -n "Total (win32 limit is 32k) : "
+ @env | wc -m
+
diff --git a/Makefile.build b/Makefile.build
index 41dfabbf..fe99f3b0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -36,10 +36,12 @@ endif
# of include, and they will then be automatically deleted, leading to an
# infinite loop.
-ALLDEPS=$(addsuffix .d, \
+MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)
+
+ALLDEPS:=$(addsuffix .d, \
$(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
-.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES)
+.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
# NOTA: the -include below will lauch the build of all .d. Some of them
# will _fail_ at first, this is to be expected (no grammar.cma initially).
@@ -82,12 +84,15 @@ HIDE := $(if $(VERBOSE),,@)
LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB)
OCAMLC += $(CAMLFLAGS)
OCAMLOPT += $(CAMLFLAGS)
BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
+COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
+COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
DEPFLAGS= -slash $(LOCALINCLUDES)
define bestocaml
@@ -96,7 +101,7 @@ $(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
endef
-CAMLP4DEPS=`sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<`
+CAMLP4DEPS=`LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<`
ifeq ($(CAMLP4),camlp5)
CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
else
@@ -169,10 +174,12 @@ CINCLUDES= -I $(CAMLHLIB)
# libcoqrun.a, dllcoqrun.so
+# NB: We used to do a ranlib after ocamlmklib, but it seems that
+# ocamlmklib is already doing it
+
$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
cd $(dir $(LIBCOQRUN)) && \
$(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
- $(RANLIB) $(LIBCOQRUN)
#coq_jumptbl.h is required only if you have GCC 2.0 or later
kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
@@ -201,12 +208,12 @@ states:: states/initial.coq
$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@
+ $(HIDE)$(BESTCOQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@
$(STRIP) $@
$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@
+ $(HIDE)$(BESTCOQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@
$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
@@ -544,9 +551,9 @@ $(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BEST
ifeq ($(CAMLP4),camlp4)
tools/compat5.cmo: tools/compat5.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
tools/compat5b.cmo: tools/compat5b.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
else
tools/compat5.cmo: tools/compat5.ml
$(OCAMLC) -c $<
@@ -729,7 +736,7 @@ dev/printers.cma: | dev/printers.mllib.d
parsing/grammar.cma: | parsing/grammar.mllib.d
$(SHOW)'Testing $@'
@touch test.ml4
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
@@ -846,6 +853,12 @@ COND_OPTFLAGS= \
HACKMLI = $(if $(wildcard $)
+
+Theories:
+
+- Rendre transparent tous les theoremes prouvant {A}+{B}
+- Faire demarrer PolyList.nth a` l'indice 0
+ Renommer l'actuel nth en nth1 ??
+
+Doc:
+
+- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
+- Documenter le filtrage sur les types inductifs avec let-ins (dont la
+ compatibilite V6)
+
+- Ajouter let dans les règles du CIC
+ -> FAIT, mais reste a documenter le let dans les inductifs
+ et les champs manifestes dans les Record
+- revoir le chapitre sur les tactiques utilisateur
+- faut-il mieux spécifier la sémantique de Simpl (??)
+
+- Préciser la clarification syntaxique de IntroPattern
+- preciser que Goal vient en dernier dans une clause pattern list et
+ qu'il doit apparaitre si il y a un "in"
+
+- Omega Time debranche mais Omega System et Omega Action remarchent ?
+- Ajout "Replace in" (mais TODO)
+- Syntaxe Conditional tac Rewrite marche, à documenter
+- Documenter Dependent Rewrite et CutRewrite ?
+- Ajouter les motifs sous-termes de ltac
+
+- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
+- mettre à jour la doc de induction (arguments multiples) (Pierre C.)
+- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
+--> mettre à jour le CHANGES (vers la ligne 72)
+
+
diff --git a/checker/check.ml b/checker/check.ml
index bb42b949..237eb079 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* "
- echo "-with-ar "
- echo "-with-ranlib "
- printf "\tTells configure where to find gcc/ar/ranlib executables\n"
echo "-byte-only"
printf "\tCompiles only bytecode version of Coq\n"
echo "-debug"
@@ -119,10 +115,6 @@ best_compiler=opt
cflags="-fno-defer-pop -Wall -Wno-unused"
natdynlink=yes
-gcc_exec=gcc
-ar_exec=ar
-ranlib_exec=ranlib
-
local=false
coqrunbyteflags_spec=no
coqtoolsbyteflags_spec=no
@@ -254,18 +246,6 @@ while : ; do
no) with_geoproof=false;;
esac
shift;;
- -with-cc|-with-gcc|--with-cc|--with-gcc)
- gcc_spec=yes
- gcc_exec=$2
- shift;;
- -with-ar|--with-ar)
- ar_spec=yes
- ar_exec=$2
- shift;;
- -with-ranlib|--with-ranlib)
- ranlib_spec=yes
- ranlib_exec=$2
- shift;;
-makecmd|--makecmd) makecmd="$2"
shift;;
-byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
@@ -292,17 +272,19 @@ case $DATEPGM in
"") echo "I can't find the program \"date\" in your path."
echo "Please give me the current date"
read COMPILEDATE;;
- *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;;
+ *) COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;;
esac
# Architecture
case $arch_spec in
no)
- # First we test if we are running a Cygwin system
+ # First we test if we are running a Cygwin or Mingw/Msys system
if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
ARCH="win32"
CYGWIN=yes
+ elif [ `uname -s | cut -c -7` = "MINGW32" ]; then
+ ARCH="win32"
else
# If not, we determine the architecture
if test -x /bin/uname ; then
@@ -437,12 +419,26 @@ if test ! -f "$CAMLC" ; then
exit 1
fi
-# Under Windows, OCaml only understands Windows filenames (C:\...)
-case $ARCH in
- win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
+# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml)
+# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept
+
+mk_win_path () {
+ case $ARCH,$CYGWIN in
+ win32,yes) cygpath -m "$1" ;;
+ win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;;
+ *) echo "$1" ;;
+ esac
+}
+
+case $ARCH,$src_spec in
+ win32,yes) echo "Error: the -src option is currently not supported on Windows"
+ exit 1;;
+ win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;;
esac
-CAMLVERSION=`"$bytecamlc" -version`
+# Beware of the final \r in Win32
+CAMLVERSION=`"$CAMLC" -version | tr -d "\r"`
+CAMLLIB=`"$CAMLC" -where | tr -d "\r"`
case $CAMLVERSION in
1.*|2.*|3.0*|3.10*|3.11.[01])
@@ -454,7 +450,7 @@ case $CAMLVERSION in
echo " Configuration script failed!"
exit 1
fi;;
- 3.11.2|3.12*)
+ 3.11.2|3.12*|4.*)
CAMLP4COMPAT="-loc loc"
echo "You have Objective-Caml $CAMLVERSION. Good!";;
*)
@@ -468,16 +464,9 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
# For coqmktop & bytecode compiler
-case $ARCH in
- win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
- CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
- *)
- CAMLLIB=`"$CAMLC" -where`
-esac
-
if [ "$coq_debug_flag" = "-g" ]; then
case $CAMLTAG in
- OCAML31*)
+ OCAML31*|OCAML4*)
# Compilation debug flag
coq_debug_flag_opt="-g"
;;
@@ -485,7 +474,7 @@ if [ "$coq_debug_flag" = "-g" ]; then
fi
# Native dynlink
-if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
+if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
HASNATDYNLINK=true
else
HASNATDYNLINK=false
@@ -520,7 +509,8 @@ esac
# (this should become configurable some day)
CAMLP4BIN=${CAMLBIN}
-if [ "$usecamlp5" = "yes" ]; then
+case $usecamlp5 in
+ yes)
CAMLP4=camlp5
CAMLP4MOD=gramlib
if [ "$camlp5dir" != "" ]; then
@@ -539,38 +529,47 @@ if [ "$usecamlp5" = "yes" ]; then
CAMLP4LIB=+site-lib/camlp5
FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
else
- echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
- echo "Configuration script failed!"
- exit 1
+ echo "No Camlp5 installation found. Looking for Camlp4 instead..."
+ usecamlp5=no
fi
+esac
- camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
- case `$camlp4oexec -v 2>&1` in
- *4.0*|*5.00*)
+# If we're (still...) going to use Camlp5, let's check its version
+
+case $usecamlp5 in
+ yes)
+ camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
+ case `"$camlp4oexec" -v 2>&1` in
+ *"version 4.0"*|*5.00*)
echo "Camlp5 version < 5.01 not supported."
echo "Configuration script failed!"
exit 1;;
esac
+esac
+
+# We might now try to use Camlp4, either by explicit choice or
+# by lack of proper Camlp5 installation
-else # let's use camlp4
+case $usecamlp5 in
+ no)
CAMLP4=camlp4
CAMLP4MOD=camlp4lib
CAMLP4LIB=+camlp4
FULLCAMLP4LIB=${CAMLLIB}/camlp4
if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
- echo "Objective Caml $CAMLVERSION found but no Camlp4 installed."
+ echo "No Camlp4 installation found."
echo "Configuration script failed!"
exit 1
fi
camlp4oexec=${camlp4oexec}rf
- if [ "`$camlp4oexec 2>&1`" != "" ]; then
+ if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
echo "Error: $camlp4oexec not found or not executable."
echo "Configuration script failed!"
exit 1
fi
-fi
+esac
# do we have a native compiler: test of ocamlopt and its version
@@ -595,18 +594,17 @@ fi
# OS dependent libraries
-case $ARCH in
+OSDEPLIBS="-cclib -lunix"
+case $ARCH,$CYGWIN in
sun4*) OS=`uname -r`
case $OS in
5*) OS="Sun Solaris $OS"
- OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
+ OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
*) OS="Sun OS $OS"
- OSDEPLIBS="-cclib -lunix"
esac;;
- win32) OS="Win32"
- OSDEPLIBS="-cclib -lunix"
+ win32,yes) OS="Win32 (Cygwin)"
cflags="-mno-cygwin $cflags";;
- *) OSDEPLIBS="-cclib -lunix"
+ win32,*) OS="Win32 (MinGW)";;
esac
# lablgtk2 and CoqIDE
@@ -628,11 +626,11 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
echo "CoqIde disabled as requested."
else
case $lablgtkdir_spec in
- no)
- if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
+ no)
+ if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then
+ lablgtkdir_spec=yes
+ elif [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
lablgtkdir=${CAMLLIB}/lablgtk2
- elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
- lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
fi;;
yes)
if [ ! -f "$lablgtkdir/glib.mli" ]; then
@@ -656,10 +654,10 @@ else
else
echo "LablGtk2 found, native threads: native CoqIde will be available."
COQIDE=opt
- if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration;
+ if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration;
then
- cflags=$cflags" `pkg-config --cflags ige-mac-integration`"
- IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
+ cflags=$cflags" `pkg-config --cflags gtk-mac-integration`"
+ IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"'
IDEARCHFILE=ide/ide_mac_stubs.o
IDEARCHDEF=QUARTZ
elif [ "$ARCH" = "win32" ];
@@ -685,9 +683,6 @@ esac
# strip command
case $ARCH in
- win32)
- # true -> strip : it exists under cygwin !
- STRIPCOMMAND="strip";;
Darwin) if [ "$HASNATDYNLINK" = "true" ]
then
STRIPCOMMAND="true"
@@ -703,13 +698,6 @@ case $ARCH in
fi
esac
-# mktexlsr
-#MKTEXLSR=`which mktexlsr`
-#case $MKTEXLSR in
-# "") MKTEXLSR=true;;
-#esac
-
-# "
### Test if documentation can be compiled (latex, hevea)
if test "$with_doc" = "all"
@@ -727,26 +715,28 @@ fi
###########################################
# bindir, libdir, mandir, docdir, etc.
-case $src_spec in
- no) COQTOP=${COQSRC}
-esac
-
# OCaml only understand Windows filenames (C:\...)
case $ARCH in
- win32) COQTOP=`cygpath -m ${COQTOP}`
+ win32) COQSRC=`mk_win_path "$COQSRC"`
+ CAMLBIN=`mk_win_path "$CAMLBIN"`
+ CAMLP4BIN=`mk_win_path "$CAMLP4BIN"`
+esac
+
+case $src_spec in
+ no) COQTOP=${COQSRC}
esac
case $ARCH$CYGWIN in
win32)
- W32PREF='C:\\coq\\'
- bindir_def=${W32PREF}bin
- libdir_def=${W32PREF}lib
- configdir_def=${W32PREF}config
- datadir_def=${W32PREF}share
- mandir_def=${W32PREF}man
- docdir_def=${W32PREF}doc
- emacslib_def=${W32PREF}emacs
- coqdocdir_def=${W32PREF}latex;;
+ W32PREF='C:\coq\'
+ bindir_def="${W32PREF}bin"
+ libdir_def="${W32PREF}lib"
+ configdir_def="${W32PREF}config"
+ datadir_def="${W32PREF}share"
+ mandir_def="${W32PREF}man"
+ docdir_def="${W32PREF}doc"
+ emacslib_def="${W32PREF}emacs"
+ coqdocdir_def="${W32PREF}latex";;
*)
bindir_def=/usr/local/bin
libdir_def=/usr/local/lib/coq
@@ -755,7 +745,7 @@ case $ARCH$CYGWIN in
mandir_def=/usr/local/share/man
docdir_def=/usr/local/share/doc/coq
emacslib_def=/usr/local/share/emacs/site-lisp
- coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
+ coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
esac
emacs_def=emacs
@@ -764,7 +754,7 @@ case $bindir_spec/$prefix_spec/$local in
yes/*/*) BINDIR=$bindir ;;
*/yes/*) BINDIR=$prefix/bin ;;
*/*/true) BINDIR=$COQTOP/bin ;;
- *) printf "Where should I install the Coq binaries [$bindir_def]? "
+ *) printf "Where should I install the Coq binaries [%s]? " "$bindir_def"
read BINDIR
case $BINDIR in
"") BINDIR=$bindir_def;;
@@ -781,7 +771,7 @@ case $libdir_spec/$prefix_spec/$local in
*) LIBDIR=$prefix/lib/coq ;;
esac ;;
*/*/true) LIBDIR=$COQTOP ;;
- *) printf "Where should I install the Coq library [$libdir_def]? "
+ *) printf "Where should I install the Coq library [%s]? " "$libdir_def"
read LIBDIR
libdir_spec=yes
case $LIBDIR in
@@ -790,11 +780,6 @@ case $libdir_spec/$prefix_spec/$local in
esac;;
esac
-case $libdir_spec in
- yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
- *) LIBDIR_OPTION="None";;
-esac
-
case $configdir_spec/$prefix_spec/$local in
yes/*/*) CONFIGDIR=$configdir;;
*/yes/*) configdir_spec=yes
@@ -804,7 +789,7 @@ case $configdir_spec/$prefix_spec/$local in
esac;;
*/*/true) CONFIGDIR=$COQTOP/ide
configdir_spec=yes;;
- *) printf "Where should I install the Coqide configuration files [$configdir_def]? "
+ *) printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def"
read CONFIGDIR
case $CONFIGDIR in
"") CONFIGDIR=$configdir_def;;
@@ -812,17 +797,12 @@ case $configdir_spec/$prefix_spec/$local in
esac;;
esac
-case $configdir_spec in
- yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
- *) CONFIGDIR_OPTION="None";;
-esac
-
case $datadir_spec/$prefix_spec/$local in
yes/*/*) DATADIR=$datadir;;
*/yes/*) DATADIR=$prefix/share/coq;;
*/*/true) DATADIR=$COQTOP/ide
datadir_spec=yes;;
- *) printf "Where should I install the Coqide data files [$datadir_def]? "
+ *) printf "Where should I install the Coqide data files [%s]? " "$datadir_def"
read DATADIR
case $DATADIR in
"") DATADIR=$datadir_def;;
@@ -830,17 +810,11 @@ case $datadir_spec/$prefix_spec/$local in
esac;;
esac
-case $datadir_spec in
- yes) DATADIR_OPTION="Some \"$DATADIR\"";;
- *) DATADIR_OPTION="None";;
-esac
-
-
case $mandir_spec/$prefix_spec/$local in
yes/*/*) MANDIR=$mandir;;
*/yes/*) MANDIR=$prefix/share/man ;;
*/*/true) MANDIR=$COQTOP/man ;;
- *) printf "Where should I install the Coq man pages [$mandir_def]? "
+ *) printf "Where should I install the Coq man pages [%s]? " "$mandir_def"
read MANDIR
case $MANDIR in
"") MANDIR=$mandir_def;;
@@ -852,7 +826,7 @@ case $docdir_spec/$prefix_spec/$local in
yes/*/*) DOCDIR=$docdir;;
*/yes/*) DOCDIR=$prefix/share/doc/coq;;
*/*/true) DOCDIR=$COQTOP/doc;;
- *) printf "Where should I install the Coq documentation [$docdir_def]? "
+ *) printf "Where should I install the Coq documentation [%s]? " "$docdir_def"
read DOCDIR
case $DOCDIR in
"") DOCDIR=$docdir_def;;
@@ -868,7 +842,7 @@ case $emacslib_spec/$prefix_spec/$local in
*) EMACSLIB=$prefix/share/emacs/site-lisp ;;
esac ;;
*/*/true) EMACSLIB=$COQTOP/tools/emacs ;;
- *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
+ *) printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def"
read EMACSLIB
case $EMACSLIB in
"") EMACSLIB=$emacslib_def;;
@@ -884,7 +858,7 @@ case $coqdocdir_spec/$prefix_spec/$local in
*) COQDOCDIR=$prefix/share/emacs/site-lisp ;;
esac ;;
*/*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
- *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
+ *) printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def"
read COQDOCDIR
case $COQDOCDIR in
"") COQDOCDIR=$coqdocdir_def;;
@@ -914,14 +888,14 @@ case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
esac
# case $emacs_spec in
-# no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
+# no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def"
# read EMACS
# case $EMACS in
-# "") EMACS=$emacs_def;;
+# "") EMACS="$emacs_def";;
# *) true;;
# esac;;
-# yes) EMACS=$emacs;;
+# yes) EMACS="$emacs";;
# esac
@@ -1016,51 +990,63 @@ config_template="$COQSRC/config/Makefile.template"
### After this line, be careful when using variables,
### since some of them (e.g. $COQSRC) will be escaped
-
-# An escaped version of a variable
-escape_var () {
-"$ocamlexec" 2>&1 1>/dev/null < "$config_file"
+cat << END_OF_MAKEFILE > $config_file
+###### config/Makefile : Configuration file for Coq ##############
+# #
+# This file is generated by the script "configure" #
+# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! #
+# If something is wrong below, then rerun the script "configure" #
+# with the good options (see the file INSTALL). #
+# #
+##################################################################
+
+#Variable used to detect whether ./configure has run successfully.
+COQ_CONFIGURED=yes
+
+# Local use (no installation)
+LOCAL=$local
+
+# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
+COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS
+$BUILDLDPATH
+
+# Paths for true installation
+# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
+# do_Makefile will reside
+# LIBDIR=path where the Coq library will reside
+# MANDIR=path where to install manual pages
+# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+BINDIR="$BINDIR"
+COQLIBINSTALL="$LIBDIR"
+CONFIGDIR="$CONFIGDIR"
+DATADIR="$DATADIR"
+MANDIR="$MANDIR"
+DOCDIR="$DOCDIR"
+EMACSLIB="$EMACSLIB"
+EMACS=$EMACS
+
+# Path to Coq distribution
+COQSRC="$COQSRC"
+VERSION=$VERSION
+
+# Ocaml version number
+CAMLVERSION=$CAMLTAG
+
+# Ocaml libraries
+CAMLLIB="$CAMLLIB"
+
+# Ocaml .h directory
+CAMLHLIB="$CAMLLIB"
+
+# Camlp4 : flavor, binaries, libraries ...
+# NB : CAMLP4BIN can be empty if camlp4 is in the PATH
+# NB : avoid using CAMLP4LIB (conflict under Windows)
+CAMLP4BIN="$CAMLP4BIN"
+CAMLP4=$CAMLP4
+CAMLP4O=$camlp4oexec
+CAMLP4COMPAT=$CAMLP4COMPAT
+MYCAMLP4LIB="$CAMLP4LIB"
+
+# LablGTK
+COQIDEINCLUDES=$LABLGTKINCLUDES
+
+# Objective-Caml compile command
+OCAML="$ocamlexec"
+OCAMLC="$bytecamlc"
+OCAMLMKLIB="$ocamlmklibexec"
+OCAMLOPT="$nativecamlc"
+OCAMLDEP="$ocamldepexec"
+OCAMLDOC="$ocamldocexec"
+OCAMLLEX="$ocamllexexec"
+OCAMLYACC="$ocamlyaccexec"
+
+# Caml link command and Caml make top command
+CAMLLINK="$bytecamlc"
+CAMLOPTLINK="$nativecamlc"
+CAMLMKTOP="$ocamlmktopexec"
+
+# Caml flags
+CAMLFLAGS=-rectypes $coq_annotate_flag
+
+# Compilation debug flags
+CAMLDEBUG=$coq_debug_flag
+CAMLDEBUGOPT=$coq_debug_flag_opt
+
+# User compilation flag
+USERFLAGS=
+
+# Flags for GCC
+CFLAGS=$cflags
+
+# Compilation profile flag
+CAMLTIMEPROF=$coq_profile_flag
+
+# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
+BEST=$best_compiler
+
+# Your architecture
+# Can be obtain by UNIX command arch
+ARCH=$ARCH
+HASNATDYNLINK=$NATDYNLINKFLAG
+
+# Supplementary libs for some systems, currently:
+# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
+# . others : -cclib -lunix
+OSDEPLIBS=$OSDEPLIBS
+
+# executable files extension, currently:
+# Unix systems:
+# Win32 systems : .exe
+EXE=$EXE
+DLLEXT=$DLLEXT
+
+# the command MKDIR (try to replace it with mkdirhier if you have problems)
+MKDIR=mkdir -p
+
+# where to put the coqdoc.sty style file
+COQDOCDIR="$COQDOCDIR"
+
+#the command STRIP
+# Unix systems and profiling: true
+# Unix systems and no profiling: strip
+STRIP=$STRIPCOMMAND
+
+# CoqIde (no/byte/opt)
+HASCOQIDE=$COQIDE
+IDEOPTFLAGS=$IDEARCHFLAGS
+IDEOPTDEPS=$IDEARCHFILE
+IDEOPTINT=$IDEARCHDEF
+
+# Defining REVISION
+CHECKEDOUT=$checkedout
+
+# Option to control compilation and installation of the documentation
+WITHDOC=$with_doc
+
+# make or sed are bogus and believe lines not terminating by a return
+# are inexistent
+END_OF_MAKEFILE
chmod a-w "$config_file"
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index b3edd7d0..f54df8a8 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* \(.*\)$/\1\2/
+s/^;\{0,1\} *\(.*\)\(.*\)$/\1\2/
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3116cbf2..0038e78a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* try pp(pr_ltype x) with e -> pp (str (Printexc.to_string
let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
-let ppbigint n = pp (Bigint.pr_bigint n);;
+let ppbigint n = pp (str (Bigint.to_string n));;
let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
let ppintset l = pp (prset int (Intset.elements l))
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
deleted file mode 100644
index 707ee824..00000000
--- a/doc/refman/RefMan-sch.tex
+++ /dev/null
@@ -1,418 +0,0 @@
-\chapter{Proof schemes}
-
-\section{Generation of induction principles with {\tt Scheme}}
-\label{Scheme}
-\index{Schemes}
-\comindex{Scheme}
-
-The {\tt Scheme} command is a high-level tool for generating
-automatically (possibly mutual) induction principles for given types
-and sorts. Its syntax follows the schema:
-\begin{quote}
-{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\\
- with {\ident$_m$} := Induction for {\ident'$_m$} Sort
- {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
-identifiers belonging to the same package of mutual inductive
-definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
-to be mutually recursive definitions. Each term {\ident$_i$} proves a
-general principle of mutual induction for objects in type {\term$_i$}.
-
-\begin{Variants}
-\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\ \\
- with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
- {\sort$_m$}}
-
- Same as before but defines a non-dependent elimination principle more
- natural in case of inductively defined relations.
-
-\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
-
- Tries to generate a boolean equality and a proof of the
- decidability of the usual equality. If \ident$_i$ involves
- some other inductive types, their equality has to be defined first.
-
-\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\\
- with Induction for {\ident$_m$} Sort
- {\sort$_m$}}
-
- If you do not provide the name of the schemes, they will be automatically
- computed from the sorts involved (works also with Minimality).
-
-\end{Variants}
-\label{Scheme-examples}
-
-\firstexample
-\example{Induction scheme for \texttt{tree} and \texttt{forest}}
-
-The definition of principle of mutual induction for {\tt tree} and
-{\tt forest} over the sort {\tt Set} is defined by the command:
-
-\begin{coq_eval}
-Reset Initial.
-Variables A B : Set.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive tree : Set :=
- node : A -> forest -> tree
-with forest : Set :=
- | leaf : B -> forest
- | cons : tree -> forest -> forest.
-
-Scheme tree_forest_rec := Induction for tree Sort Set
- with forest_tree_rec := Induction for forest Sort Set.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_forest\_rec}:
-
-\begin{coq_example}
-Check tree_forest_rec.
-\end{coq_example}
-
-This principle involves two different predicates for {\tt trees} and
-{\tt forests}; it also has three premises each one corresponding to a
-constructor of one of the inductive definitions.
-
-The principle {\tt forest\_tree\_rec} shares exactly the same
-premises, only the conclusion now refers to the property of forests.
-
-\begin{coq_example}
-Check forest_tree_rec.
-\end{coq_example}
-
-\example{Predicates {\tt odd} and {\tt even} on naturals}
-
-Let {\tt odd} and {\tt even} be inductively defined as:
-
-% Reset Initial.
-\begin{coq_eval}
-Open Scope nat_scope.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive odd : nat -> Prop :=
- oddS : forall n:nat, even n -> odd (S n)
-with even : nat -> Prop :=
- | evenO : even 0
- | evenS : forall n:nat, odd n -> even (S n).
-\end{coq_example*}
-
-The following command generates a powerful elimination
-principle:
-
-\begin{coq_example}
-Scheme odd_even := Minimality for odd Sort Prop
- with even_odd := Minimality for even Sort Prop.
-\end{coq_example}
-
-The type of {\tt odd\_even} for instance will be:
-
-\begin{coq_example}
-Check odd_even.
-\end{coq_example}
-
-The type of {\tt even\_odd} shares the same premises but the
-conclusion is {\tt (n:nat)(even n)->(Q n)}.
-
-\subsection{Automatic declaration of schemes}
-\comindex{Set Equality Schemes}
-\comindex{Set Elimination Schemes}
-
-It is possible to deactivate the automatic declaration of the induction
- principles when defining a new inductive type with the
- {\tt Unset Elimination Schemes} command. It may be
-reactivated at any time with {\tt Set Elimination Schemes}.
-\\
-
-You can also activate the automatic declaration of those boolean equalities
-(see the second variant of {\tt Scheme}) with the {\tt Set Equality Schemes}
- command. However you have to be careful with this option since
-\Coq~ may now reject well-defined inductive types because it cannot compute
-a boolean equality for them.
-
-\subsection{\tt Combined Scheme}
-\label{CombinedScheme}
-\comindex{Combined Scheme}
-
-The {\tt Combined Scheme} command is a tool for combining
-induction principles generated by the {\tt Scheme} command.
-Its syntax follows the schema :
-\begin{quote}
-{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}
-\end{quote}
-where
-\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
-the same package of mutual inductive principle definitions. This command
-generates {\ident$_0$} to be the conjunction of the principles: it is
-built from the common premises of the principles and concluded by the
-conjunction of their conclusions.
-
-\Example
-We can define the induction principles for trees and forests using:
-\begin{coq_example}
-Scheme tree_forest_ind := Induction for tree Sort Prop
- with forest_tree_ind := Induction for forest Sort Prop.
-\end{coq_example}
-
-Then we can build the combined induction principle which gives the
-conjunction of the conclusions of each individual principle:
-\begin{coq_example}
-Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
-\end{coq_example}
-
-The type of {\tt tree\_forest\_mutrec} will be:
-\begin{coq_example}
-Check tree_forest_mutind.
-\end{coq_example}
-
-\section{Generation of induction principles with {\tt Functional Scheme}}
-\label{FunScheme}
-\comindex{Functional Scheme}
-
-The {\tt Functional Scheme} command is a high-level experimental
-tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions. Its
-syntax follows the schema:
-\begin{quote}
-{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\ \\
- with {\ident$_m$} := Induction for {\ident'$_m$} Sort
- {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
-names (they must be in the same order as when they were defined).
-This command generates the induction principles
-\ident$_1$\dots\ident$_m$, following the recursive structure and case
-analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
-
-\Rem
-There is a difference between obtaining an induction scheme by using
-\texttt{Functional Scheme} on a function defined by \texttt{Function}
-or not. Indeed \texttt{Function} generally produces smaller
-principles, closer to the definition written by the user.
-
-\firstexample
-\example{Induction scheme for \texttt{div2}}
-\label{FunScheme-examples}
-
-We define the function \texttt{div2} as follows:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Require Import Arith.
-Fixpoint div2 (n:nat) : nat :=
- match n with
- | O => 0
- | S O => 0
- | S (S n') => S (div2 n')
- end.
-\end{coq_example*}
-
-The definition of a principle of induction corresponding to the
-recursive structure of \texttt{div2} is defined by the command:
-
-\begin{coq_example}
-Functional Scheme div2_ind := Induction for div2 Sort Prop.
-\end{coq_example}
-
-You may now look at the type of {\tt div2\_ind}:
-
-\begin{coq_example}
-Check div2_ind.
-\end{coq_example}
-
-We can now prove the following lemma using this principle:
-
-\begin{coq_example*}
-Lemma div2_le' : forall n:nat, div2 n <= n.
-intro n.
- pattern n , (div2 n).
-\end{coq_example*}
-
-\begin{coq_example}
-apply div2_ind; intros.
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-simpl; auto with arith.
-Qed.
-\end{coq_example*}
-
-We can use directly the \texttt{functional induction}
-(\ref{FunInduction}) tactic instead of the pattern/apply trick:
-\tacindex{functional induction}
-
-\begin{coq_example*}
-Reset div2_le'.
-Lemma div2_le : forall n:nat, div2 n <= n.
-intro n.
-\end{coq_example*}
-
-\begin{coq_example}
-functional induction (div2 n).
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-auto with arith.
-Qed.
-\end{coq_example*}
-
-\Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (see Section~\ref{Function}) and by
-using \texttt{Functional Scheme} after a normal definition using
-\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
-details.
-
-
-\example{Induction scheme for \texttt{tree\_size}}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-We define trees by the following mutual inductive type:
-
-\begin{coq_example*}
-Variable A : Set.
-Inductive tree : Set :=
- node : A -> forest -> tree
-with forest : Set :=
- | empty : forest
- | cons : tree -> forest -> forest.
-\end{coq_example*}
-
-We define the function \texttt{tree\_size} that computes the size
-of a tree or a forest. Note that we use \texttt{Function} which
-generally produces better principles.
-
-\begin{coq_example*}
-Function tree_size (t:tree) : nat :=
- match t with
- | node A f => S (forest_size f)
- end
- with forest_size (f:forest) : nat :=
- match f with
- | empty => 0
- | cons t f' => (tree_size t + forest_size f')
- end.
-\end{coq_example*}
-
-\Rem \texttt{Function} generates itself non mutual induction
-principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
-
-\begin{coq_example}
-Check tree_size_ind.
-\end{coq_example}
-
-The definition of mutual induction principles following the recursive
-structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
-by the command:
-
-\begin{coq_example*}
-Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
-with forest_size_ind2 := Induction for forest_size Sort Prop.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_size\_ind2}:
-
-\begin{coq_example}
-Check tree_size_ind2.
-\end{coq_example}
-
-\section{Generation of inversion principles with \tt Derive Inversion}
-\label{Derive-Inversion}
-\comindex{Derive Inversion}
-
-The syntax of {\tt Derive Inversion} follows the schema:
-\begin{quote}
-{\tt Derive Inversion {\ident} with forall
- $(\vec{x} : \vec{T})$, $I~\vec{t}$ Sort \sort}
-\end{quote}
-
-This command generates an inversion principle for the
-\texttt{inversion \dots\ using} tactic.
-\tacindex{inversion \dots\ using}
-Let $I$ be an inductive predicate and $\vec{x}$ the variables
-occurring in $\vec{t}$. This command generates and stocks the
-inversion lemma for the sort \sort~ corresponding to the instance
-$\forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf
-global} environment. When applied, it is equivalent to having inverted
-the instance with the tactic {\tt inversion}.
-
-\begin{Variants}
-\item \texttt{Derive Inversion\_clear {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Inversion\_clear}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{inversion}
- replaced by the tactic \texttt{inversion\_clear}.
-\item \texttt{Derive Dependent Inversion {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Dependent Inversion}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{dependent inversion}.
-\item \texttt{Derive Dependent Inversion\_clear {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Dependent Inversion\_clear}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{dependent inversion\_clear}.
-\end{Variants}
-
-\Example
-
-Let us consider the relation \texttt{Le} over natural numbers and the
-following variable:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive Le : nat -> nat -> Set :=
- | LeO : forall n:nat, Le 0 n
- | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-Variable P : nat -> nat -> Prop.
-\end{coq_example*}
-
-To generate the inversion lemma for the instance
-\texttt{(Le (S n) m)} and the sort \texttt{Prop}, we do:
-
-\begin{coq_example*}
-Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
-\end{coq_example*}
-
-\begin{coq_example}
-Check leminv.
-\end{coq_example}
-
-Then we can use the proven inversion lemma:
-
-\begin{coq_eval}
-Lemma ex : forall n m:nat, Le (S n) m -> P n m.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-\begin{coq_example}
-inversion H using leminv.
-\end{coq_example}
-
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0ee101c8..833b5c4c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -400,6 +400,7 @@ through the Require Import command.
theories/Lists/List.v
theories/Lists/ListSet.v
theories/Lists/SetoidList.v
+ theories/Lists/SetoidPermutation.v
theories/Lists/Streams.v
theories/Lists/StreamMemo.v
theories/Lists/ListTactics.v
@@ -523,7 +524,10 @@ through the Require Import command.
theories/Reals/Rsigma.v
theories/Reals/R_sqr.v
theories/Reals/Rtrigo_fun.v
+ theories/Reals/Rtrigo1.v
theories/Reals/Rtrigo.v
+ theories/Reals/Ratan.v
+ theories/Reals/Machin.v
theories/Reals/SplitAbsolu.v
theories/Reals/SplitRmult.v
theories/Reals/Alembert.v
@@ -544,6 +548,8 @@ through the Require Import command.
theories/Reals/Ranalysis2.v
theories/Reals/Ranalysis3.v
theories/Reals/Ranalysis4.v
+ theories/Reals/Ranalysis5.v
+ theories/Reals/Ranalysis_reg.v
theories/Reals/Rcomplete.v
theories/Reals/RiemannInt.v
theories/Reals/RiemannInt_SF.v
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index a34e5ebe..470bd5b4 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*
let path = match status.Interface.status_path with
- | None -> ""
- | Some p -> " in " ^ p
+ | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+ | _ :: l -> " in " ^ String.concat "." l
in
let name = match status.Interface.status_proofname with
| None -> ""
@@ -2449,13 +2449,13 @@ let main files =
try configure ~apply:update_notebook_pos ()
with _ -> flash_info "Cannot save preferences"
end;
- reset_revert_timer ()) ~stock:`PREFERENCES;
+ reset_revert_timer ()) ~accel:"," ~stock:`PREFERENCES;
(* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
GAction.add_actions view_actions [
GAction.add_action "View" ~label:"_View";
- GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("Left") ~stock:`GO_BACK
+ GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("Left") ~stock:`GO_BACK
~callback:(fun _ -> session_notebook#previous_page ());
- GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("Right") ~stock:`GO_FORWARD
+ GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("Right") ~stock:`GO_FORWARD
~callback:(fun _ -> session_notebook#next_page ());
GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar"
~active:(!current.show_toolbar) ~callback:
@@ -2624,6 +2624,7 @@ let main files =
Coqide_ui.ui_m#insert_action_group windows_actions 0;
Coqide_ui.ui_m#insert_action_group help_actions 0;
w#add_accel_group Coqide_ui.ui_m#get_accel_group ;
+ GtkMain.Rc.parse_string "gtk-can-change-accels = 1";
if Coq_config.gtk_platform <> `QUARTZ
then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar");
let tbar = GtkButton.Toolbar.cast ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 57158a6a..18df1f6a 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*
#include
#include
-#include
+#include
GtkOSXApplication *theApp;
value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item;
@@ -76,10 +76,10 @@ CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about)
caml_register_generational_global_root(&about_item);
/* gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/
gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar));
- about_grp = gtk_osxapplication_add_app_menu_group(theApp);
- pref_grp = gtk_osxapplication_add_app_menu_group(theApp);
- gtk_osxapplication_add_app_menu_item(theApp,about_grp,check_cast(GTK_MENU_ITEM,about_item));
- gtk_osxapplication_add_app_menu_item(theApp,pref_grp,check_cast(GTK_MENU_ITEM,pref_item));
+ gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,about_item),1);
+ gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),2);
+ gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,pref_item),3);
+ gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),4);
gtk_osxapplication_ready(theApp);
CAMLreturn(Val_unit);
}
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index b79d6469..697e7f4f 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* []
+| (lg, rg) :: l ->
+ let inner = flatten l in
+ List.rev_append lg inner @ rg
+
let display mode (view:GText.view) goals hints evars =
let () = view#buffer#set_text "" in
match goals with
| None -> ()
(* No proof in progress *)
- | Some { Interface.fg_goals = []; Interface.bg_goals = [] } ->
- (* A proof has been finished, but not concluded *)
- begin match evars with
- | Some evs when evs <> [] ->
+ | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+ let bg = flatten (List.rev bg) in
+ let evars = match evars with None -> [] | Some evs -> evs in
+ begin match (bg, evars) with
+ | [], [] ->
+ view#buffer#insert "No more subgoals."
+ | [], _ :: _ ->
+ (* A proof has been finished, but not concluded *)
view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
let iter evar =
let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
view#buffer#insert msg
in
- List.iter iter evs
- | _ ->
- view#buffer#insert "No more subgoals."
+ List.iter iter evars
+ | _, _ ->
+ (* No foreground proofs, but still unfocused ones *)
+ view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
+ let iter goal =
+ let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+ view#buffer#insert msg
+ in
+ List.iter iter bg
end
- | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
- (* No foreground proofs, but still unfocused ones *)
- view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
- let iter goal =
- let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
- view#buffer#insert msg
- in
- List.iter iter bg
| Some { Interface.fg_goals = fg } ->
mode view fg hints
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a208ad0e..164c837a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* /C_anonical Structure/" "")
-; (gtk_accel_path "/M_odule Type/" "")
-; (gtk_accel_path "/c_ompute/" "")
-; (gtk_accel_path "/Templates/_E.../" "")
-(gtk_accel_path "/Templates/match" "c")
-; (gtk_accel_path "/D_erive Inversion/" "")
-; (gtk_accel_path "/Queries/Check" "F3")
-; (gtk_accel_path "/i_dtac/" "")
-; (gtk_accel_path "/L_oad/" "")
-; (gtk_accel_path "/a_ssert/" "")
-; (gtk_accel_path "/f_irstorder using/" "")
-; (gtk_accel_path "/s_olve/" "")
-; (gtk_accel_path "/Tactics/_l.../" "")
-(gtk_accel_path "/Templates/Inductive" "i")
-; (gtk_accel_path "/a_ssert (__:__)/" "")
-; (gtk_accel_path "/T_est Printing Synth/" "")
-; (gtk_accel_path "/Templates/_R.../" "")
-; (gtk_accel_path "/Help/Browse Coq Library" "")
-; (gtk_accel_path "/U_nset Extraction Optimize/" "")
-; (gtk_accel_path "/s_imple inversion/" "")
-(gtk_accel_path "/Edit/Copy" "c")
-; (gtk_accel_path "/E_xtract Inductive/" "")
-(gtk_accel_path "/Edit/Cut" "x")
-; (gtk_accel_path "/i_nfo/" "")
-; (gtk_accel_path "/R_emove Printing If/" "")
-; (gtk_accel_path "/e_apply/" "")
-; (gtk_accel_path "/F_ixpoint/" "")
-; (gtk_accel_path "/c_hange __ in/" "")
-; (gtk_accel_path "/l_apply/" "")
-; (gtk_accel_path "/s_imple induction/" "")
-; (gtk_accel_path "/f_ail/" "")
-; (gtk_accel_path "/e_lim/" "")
-; (gtk_accel_path "/r_ewrite <- __ in/" "")
-; (gtk_accel_path "/A_dd Printing Let/" "")
-; (gtk_accel_path "/T_ransparent/" "")
-; (gtk_accel_path "/Tactics/_d.../" "")
-(gtk_accel_path "/Tactics/Wizard" "dollar")
+; (gtk_accel_path "/Templates/Template Read Module" "")
+; (gtk_accel_path "/Tactics/Tactic pattern" "")
+(gtk_accel_path "/Templates/Definition" "d")
+; (gtk_accel_path "/Templates/Template Program Lemma" "")
+(gtk_accel_path "/Templates/Lemma" "l")
+; (gtk_accel_path "/Templates/Template Fact" "")
+(gtk_accel_path "/Tactics/auto" "a")
+; (gtk_accel_path "/Tactics/Tactic fold" "")
+; (gtk_accel_path "/Help/About Coq" "")
+; (gtk_accel_path "/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "")
+; (gtk_accel_path "/Templates/Template Hypothesis" "")
+; (gtk_accel_path "/Tactics/Tactic repeat" "")
+; (gtk_accel_path "/Templates/Template Unset Extraction Optimize" "")
+; (gtk_accel_path "/Templates/Template Add Printing Constructor" "")
; (gtk_accel_path "/Windows/Detach View" "")
-; (gtk_accel_path "/T_heorem/" "")
-(gtk_accel_path "/Templates/Scheme" "s")
-; (gtk_accel_path "/R_emark/" "")
-; (gtk_accel_path "/Compile/Compile" "")
-; (gtk_accel_path "/A_dd Relation/" "")
-; (gtk_accel_path "/r_ename __ into/" "")
-; (gtk_accel_path "/File/Save as" "")
-; (gtk_accel_path "/f_irstorder/" "")
-; (gtk_accel_path "/G_rammar/" "")
-; (gtk_accel_path "/f_irstorder with/" "")
-; (gtk_accel_path "/r_ed/" "")
-; (gtk_accel_path "/D_efinition/" "")
-; (gtk_accel_path "/R_equire Import/" "")
-; (gtk_accel_path "/d_iscriminate/" "")
-; (gtk_accel_path "/i_ntro after/" "")
-; (gtk_accel_path "/Export/Latex" "")
-; (gtk_accel_path "/j_p/" "")
-; (gtk_accel_path "/a_uto with/" "")
-; (gtk_accel_path "/S_ection/" "")
-; (gtk_accel_path "/r_ewrite/" "")
-; (gtk_accel_path "/Export/Html" "")
-; (gtk_accel_path "/Tactics/_i.../" "")
-; (gtk_accel_path "/a_utorewrite/" "")
-; (gtk_accel_path "/F_ocus/" "")
-; (gtk_accel_path "/Templates/_O.../" "")
-; (gtk_accel_path "/l_azy in/" "")
-; (gtk_accel_path "/d_ependent inversion__clear __ with/" "")
-; (gtk_accel_path "/c_utrewrite/" "")
-(gtk_accel_path "/Edit/Undo" "u")
-; (gtk_accel_path "/c_onstructor __ with/" "")
-; (gtk_accel_path "/r_ing/" "")
-; (gtk_accel_path "/d_ependent rewrite <-/" "")
-; (gtk_accel_path "/e_limtype/" "")
-(gtk_accel_path "/Tactics/simpl" "s")
-; (gtk_accel_path "/H_int/" "")
-; (gtk_accel_path "/H_int Rewrite/" "")
-; (gtk_accel_path "/V_ariable/" "")
-; (gtk_accel_path "/U_nset Implicit Arguments/" "")
-; (gtk_accel_path "/s_implify__eq/" "")
-; (gtk_accel_path "/Compile/Next error" "F7")
-; (gtk_accel_path "/Edit/Edit" "")
-; (gtk_accel_path "/S_et Extraction Optimize/" "")
-; (gtk_accel_path "/H_ypothesis/" "")
-; (gtk_accel_path "/E_nd Silent./" "")
-; (gtk_accel_path "/S_yntax/" "")
-; (gtk_accel_path "/d_ecide equality/" "")
-; (gtk_accel_path "/O_paque/" "")
-; (gtk_accel_path "/Templates/_T.../" "")
-; (gtk_accel_path "/Tactics/_a.../" "")
-; (gtk_accel_path "/Templates/_G.../" "")
-; (gtk_accel_path "/c_ase/" "")
-(gtk_accel_path "/Navigation/Backward" "Up")
-; (gtk_accel_path "/C_oFixpoint/" "")
-; (gtk_accel_path "/P_rogram Fixpoint/" "")
-; (gtk_accel_path "/d_ependent inversion__clear/" "")
-; (gtk_accel_path "/c_ase __ with/" "")
-; (gtk_accel_path "/a_ssumption/" "")
-; (gtk_accel_path "/t_ransitivity/" "")
-; (gtk_accel_path "/i_ntros until/" "")
-; (gtk_accel_path "/s_plit/" "")
-; (gtk_accel_path "/e_xists/" "")
-(gtk_accel_path "/Templates/Theorem" "t")
-; (gtk_accel_path "/Navigation/Navigation" "")
-; (gtk_accel_path "/H_int Unfold/" "")
-; (gtk_accel_path "/I_mplicit Arguments/" "")
-; (gtk_accel_path "/Help/Help" "")
-; (gtk_accel_path "/d_ecompose sum/" "")
-; (gtk_accel_path "/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "")
-; (gtk_accel_path "/Te_mplates/" "")
-(gtk_accel_path "/Edit/Find in buffer" "f")
-; (gtk_accel_path "/r_eplace __ with/" "")
-(gtk_accel_path "/Tactics/omega" "o")
-; (gtk_accel_path "/S_cheme/" "")
-; (gtk_accel_path "/L_emma/" "")
-; (gtk_accel_path "/i_nversion__clear __ in/" "")
-; (gtk_accel_path "/E_xtraction Inline/" "")
-; (gtk_accel_path "/S_yntactic Definition/" "")
-; (gtk_accel_path "/i_nstantiate (__:=__)/" "")
-; (gtk_accel_path "/C_hapter/" "")
-; (gtk_accel_path "/Templates/_L.../" "")
-; (gtk_accel_path "/Tactics/_f.../" "")
-; (gtk_accel_path "/Queries/Queries" "")
-; (gtk_accel_path "/T_est Printing Wildcard/" "")
-(gtk_accel_path "/File/Open" "o")
-; (gtk_accel_path "/f_old __ in/" "")
-(gtk_accel_path "/Navigation/Go to" "Right")
+; (gtk_accel_path "/Tactics/Tactic inversion" "")
+; (gtk_accel_path "/Templates/Template Write State" "")
; (gtk_accel_path "/Export/Export to" "")
-; (gtk_accel_path "/c_ongruence/" "")
-; (gtk_accel_path "/c_learbody/" "")
-(gtk_accel_path "/File/Close buffer" "w")
-; (gtk_accel_path "/a_pply/" "")
-; (gtk_accel_path "/Queries/SearchAbout" "F2")
-; (gtk_accel_path "/i_ntro/" "")
-; (gtk_accel_path "/H_int Immediate/" "")
-; (gtk_accel_path "/p_ose __:=__)/" "")
-; (gtk_accel_path "/U_nset Undo/" "")
-; (gtk_accel_path "/Tactics/_s.../" "")
-; (gtk_accel_path "/P_rogram Definition/" "")
-; (gtk_accel_path "/R_equire/" "")
-; (gtk_accel_path "/c_ompare/" "")
-; (gtk_accel_path "/s_ymmetry in/" "")
-(gtk_accel_path "/Display/Display coercions" "c")
-(gtk_accel_path "/Navigation/Previous" "less")
-(gtk_accel_path "/Display/Display all low-level contents" "l")
-; (gtk_accel_path "/C_oercion Local/" "")
-; (gtk_accel_path "/f_ix __ with/" "")
-; (gtk_accel_path "/A_dd ML Path/" "")
-; (gtk_accel_path "/A_xiom/" "")
-; (gtk_accel_path "/Templates/Templates" "")
-; (gtk_accel_path "/a_bstract/" "")
-; (gtk_accel_path "/Edit/Clear Undo Stack" "")
-(gtk_accel_path "/File/New" "n")
-; (gtk_accel_path "/Tactics/_hnf/" "")
-; (gtk_accel_path "/d_o/" "")
-; (gtk_accel_path "/E_xtract Constant/" "")
-; (gtk_accel_path "/E_nd/" "")
-; (gtk_accel_path "/Templates/_Qed./" "")
-; (gtk_accel_path "/A_dd Rec ML Path/" "")
-; (gtk_accel_path "/Templates/_D.../" "")
-(gtk_accel_path "/Navigation/Hide" "h")
-; (gtk_accel_path "/c_ofix/" "")
-; (gtk_accel_path "/_Try Tactics/" "")
-; (gtk_accel_path "/S_et Printing Wildcard/" "")
-; (gtk_accel_path "/i_nversion__clear/" "")
-; (gtk_accel_path "/Templates/_V.../" "")
+(gtk_accel_path "/Tactics/auto with *" "asterisk")
+; (gtk_accel_path "/Tactics/Tactic inversion--clear" "")
+; (gtk_accel_path "/Templates/Template Implicit Arguments" "")
+(gtk_accel_path "/Edit/Find backwards" "b")
+; (gtk_accel_path "/Edit/Copy" "c")
+; (gtk_accel_path "/Tactics/Tactic inversion -- using" "")
+(gtk_accel_path "/View/Previous tab" "Left")
+; (gtk_accel_path "/Tactics/Tactic change -- in" "")
+; (gtk_accel_path "/Tactics/Tactic jp" "")
+; (gtk_accel_path "/Tactics/Tactic red" "")
+; (gtk_accel_path "/Templates/Template Coercion" "")
+; (gtk_accel_path "/Templates/Template CoFixpoint" "")
+; (gtk_accel_path "/Tactics/Tactic intros until" "")
+; (gtk_accel_path "/Templates/Template Derive Dependent Inversion" "")
+; (gtk_accel_path "/Tactics/Tactic eapply" "")
+; (gtk_accel_path "/View/View" "")
+; (gtk_accel_path "/Tactics/Tactic change" "")
+; (gtk_accel_path "/Tactics/Tactic firstorder using" "")
+; (gtk_accel_path "/Tactics/Tactic decompose sum" "")
+; (gtk_accel_path "/Tactics/Tactic cut" "")
+; (gtk_accel_path "/Templates/Template Remove Printing Let" "")
+; (gtk_accel_path "/Templates/Template Structure" "")
+; (gtk_accel_path "/Tactics/Tactic compute in" "")
+; (gtk_accel_path "/Queries/Locate" "")
+; (gtk_accel_path "/Templates/Template Save." "")
+; (gtk_accel_path "/Templates/Template Canonical Structure" "")
+; (gtk_accel_path "/Tactics/Tactic compare" "")
+; (gtk_accel_path "/Templates/Template Next Obligation" "")
+(gtk_accel_path "/View/Display notations" "n")
+; (gtk_accel_path "/Tactics/Tactic fail" "")
+; (gtk_accel_path "/Tactics/Tactic left" "")
+(gtk_accel_path "/Edit/Undo" "u")
+(gtk_accel_path "/Tactics/eauto with *" "