This is an automated email from the git hooks/post-receive script.

gareuselesinge pushed a change to branch upstream
in repository coq.

      from  cec4741   Imported Upstream version 8.5~beta1+dfsg
       new  0aa2544   Imported Upstream version 8.5~beta2+dfsg

The 1 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails.  The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.


Summary of changes:
 CHANGES                                           |  143 +-
 COMPATIBILITY                                     |   14 +
 INSTALL                                           |   48 +-
 INSTALL.ide                                       |  126 +-
 INSTALL.macosx                                    |   20 -
 Makefile                                          |    2 +-
 Makefile.build                                    |   10 +-
 Makefile.common                                   |   12 +-
 Makefile.doc                                      |   14 +-
 README.win                                        |   49 +-
 _tags                                             |    4 +-
 checker/check.ml                                  |    2 +-
 checker/checker.ml                                |    3 +-
 checker/cic.mli                                   |    2 +-
 checker/declarations.ml                           |    2 +-
 checker/indtypes.ml                               |    1 -
 checker/reduction.ml                              |   10 +-
 checker/safe_typing.ml                            |    3 +-
 checker/univ.ml                                   |   43 +-
 checker/values.ml                                 |   43 +-
 checker/votour.ml                                 |  154 +-
 configure.ml                                      |  177 +-
 dev/TODO                                          |   22 -
 dev/nsis/coq.nsi                                  |    4 +-
 dev/top_printers.ml                               |    5 +-
 doc/stdlib/index-list.html.template               |    7 +
 doc/whodidwhat/whodidwhat-8.4update.tex           |   20 +-
 grammar/vernacextend.ml4                          |   50 +-
 ide/MacOS/Info.plist.template                     |    2 +-
 ide/MacOS/default_accel_map                       |    1 -
 ide/coq.lang                                      |   59 +-
 ide/coqOps.ml                                     |   42 +-
 ide/coq_commands.ml                               |    2 -
 ide/coqide.ml                                     |   73 +-
 ide/coqide_ui.ml                                  |    1 -
 ide/gtk_parsing.ml                                |   13 +
 ide/ide_slave.ml                                  |    8 +-
 ide/ideutils.ml                                   |   50 +-
 ide/ideutils.mli                                  |    4 +-
 ide/preferences.ml                                |   39 +-
 ide/preferences.mli                               |    2 +
 ide/project_file.ml4                              |   22 +-
 ide/session.ml                                    |   41 +-
 ide/session.mli                                   |    1 +
 ide/tags.ml                                       |   26 +-
 ide/tags.mli                                      |   13 +-
 ide/wg_Find.ml                                    |   14 +-
 ide/wg_MessageView.ml                             |   31 +-
 ide/wg_MessageView.mli                            |    9 +
 ide/wg_ProofView.ml                               |    5 +
 ide/wg_ProofView.mli                              |    1 +
 ide/wg_ScriptView.ml                              |   13 +-
 ide/wg_Segment.ml                                 |   31 +-
 ide/wg_Segment.mli                                |    8 +
 interp/constrarg.ml                               |    3 +
 interp/constrarg.mli                              |    2 +
 interp/constrextern.ml                            |    2 +-
 interp/constrintern.ml                            |    1 -
 interp/constrintern.mli                           |    1 +
 interp/coqlib.ml                                  |    2 -
 interp/coqlib.mli                                 |    1 -
 interp/genintern.ml                               |    1 -
 interp/genintern.mli                              |    1 -
 interp/modintern.ml                               |    4 +-
 interp/notation.ml                                |   32 +-
 interp/notation.mli                               |    4 +
 interp/notation_ops.ml                            |   63 +
 interp/notation_ops.mli                           |    2 +
 intf/tacexpr.mli                                  |    2 -
 intf/vernacexpr.mli                               |    4 +-
 kernel/byterun/coq_fix_code.c                     |   11 +-
 kernel/byterun/coq_interp.c                       |   81 +-
 kernel/byterun/int64_native.h                     |   16 +-
 kernel/cbytecodes.ml                              |    3 +
 kernel/cbytecodes.mli                             |    1 +
 kernel/cbytegen.ml                                |  132 +-
 kernel/cbytegen.mli                               |    9 +-
 kernel/cemitcodes.ml                              |   90 +-
 kernel/closure.ml                                 |   20 +-
 kernel/constr.ml                                  |   95 +-
 kernel/constr.mli                                 |   17 +-
 kernel/csymtable.ml                               |   23 +-
 kernel/declarations.mli                           |    8 +-
 kernel/declareops.ml                              |    2 +-
 kernel/declareops.mli                             |    1 -
 kernel/environ.ml                                 |    2 +-
 kernel/environ.mli                                |    2 +-
 kernel/fast_typeops.mli                           |    5 -
 kernel/indtypes.ml                                |   21 +-
 kernel/inductive.ml                               |    9 +-
 kernel/mod_typing.ml                              |   27 +-
 kernel/modops.ml                                  |   57 +-
 kernel/names.ml                                   |   10 +-
 kernel/names.mli                                  |    6 +-
 kernel/nativecode.ml                              |    1 -
 kernel/nativelambda.ml                            |    9 +-
 kernel/nativelambda.mli                           |    1 -
 kernel/nativelib.ml                               |    5 +-
 kernel/nativelibrary.ml                           |    1 -
 kernel/nativevalues.ml                            |   12 +-
 kernel/opaqueproof.mli                            |    1 -
 kernel/reduction.ml                               |    8 -
 kernel/safe_typing.ml                             |    6 +-
 kernel/term_typing.ml                             |   17 +-
 kernel/term_typing.mli                            |    1 -
 kernel/typeops.ml                                 |   10 +-
 kernel/uint31.ml                                  |    4 +-
 kernel/uint31.mli                                 |    2 +-
 kernel/univ.ml                                    |   47 +-
 kernel/vconv.ml                                   |    5 +-
 kernel/vm.ml                                      |   18 +-
 kernel/vm.mli                                     |    2 +-
 lib/cArray.ml                                     |   28 +-
 lib/cArray.mli                                    |    5 +
 lib/cString.ml                                    |    9 +-
 lib/cThread.ml                                    |   41 +-
 lib/dyn.ml                                        |    2 +
 lib/dyn.mli                                       |    1 +
 lib/errors.ml                                     |    2 +-
 lib/errors.mli                                    |    2 +-
 lib/future.ml                                     |   72 +-
 lib/future.mli                                    |    5 +-
 lib/hashcons.ml                                   |    3 +
 lib/hashcons.mli                                  |    2 +
 lib/hashset.ml                                    |   26 +
 lib/hashset.mli                                   |    9 +
 lib/monad.ml                                      |    2 +-
 lib/pp.ml                                         |   13 +-
 lib/richpp.ml                                     |  215 +-
 lib/richpp.mli                                    |    4 +-
 lib/terminal.ml                                   |    3 +-
 library/assumptions.ml                            |  151 +-
 library/assumptions.mli                           |   15 +-
 library/declare.ml                                |   33 +-
 library/declare.mli                               |    2 +-
 library/global.mli                                |   18 +-
 library/globnames.ml                              |    1 -
 library/goptions.ml                               |   10 +-
 library/libnames.ml                               |    5 +
 library/libnames.mli                              |    2 +
 library/library.ml                                |  326 +--
 library/library.mli                               |   15 +-
 library/loadpath.ml                               |   83 +-
 library/loadpath.mli                              |   16 +-
 library/states.ml                                 |    1 +
 library/states.mli                                |    1 +
 library/summary.ml                                |    1 +
 library/universes.ml                              |    9 +-
 library/universes.mli                             |    3 -
 parsing/g_constr.ml4                              |    2 +-
 parsing/g_ltac.ml4                                |    8 +-
 parsing/g_proofs.ml4                              |   14 +-
 parsing/g_tactic.ml4                              |    2 +-
 parsing/g_vernac.ml4                              |    5 +-
 parsing/pcoq.ml4                                  |    2 +
 parsing/pcoq.mli                                  |    2 +
 plugins/cc/ccproof.mli                            |    1 -
 plugins/cc/cctac.ml                               |   20 +-
 plugins/decl_mode/decl_expr.mli                   |   32 +-
 plugins/decl_mode/decl_mode.ml                    |   26 +-
 plugins/decl_mode/decl_mode.mli                   |    4 +-
 plugins/decl_mode/decl_proof_instr.ml             |   39 +-
 plugins/decl_mode/g_decl_mode.ml4                 |   57 +-
 plugins/decl_mode/ppdecl_proof.ml                 |  169 +-
 plugins/decl_mode/ppdecl_proof.mli                |   14 +-
 plugins/derive/derive.ml                          |    4 +-
 plugins/extraction/ExtrHaskellBasic.v             |   15 +
 plugins/extraction/ExtrOcamlNatInt.v              |    1 +
 plugins/extraction/common.ml                      |    3 +-
 plugins/extraction/extract_env.ml                 |    6 +-
 plugins/extraction/extraction_plugin.mllib        |    1 +
 plugins/extraction/g_extraction.ml4               |    2 +
 plugins/extraction/haskell.ml                     |   36 +-
 plugins/extraction/json.ml                        |  278 +++
 plugins/extraction/json.mli                       |    1 +
 plugins/extraction/miniml.mli                     |    1 +
 plugins/extraction/ocaml.ml                       |   15 +-
 plugins/extraction/scheme.ml                      |    3 +-
 plugins/extraction/table.ml                       |    2 +-
 plugins/extraction/table.mli                      |    2 +-
 plugins/extraction/vo.itarget                     |    1 +
 plugins/firstorder/formula.mli                    |    1 -
 plugins/firstorder/instances.ml                   |   32 +-
 plugins/firstorder/sequent.ml                     |    2 +-
 plugins/fourier/fourierR.ml                       |    1 -
 plugins/funind/functional_principles_proofs.ml    |  123 +-
 plugins/funind/functional_principles_proofs.mli   |    1 +
 plugins/funind/functional_principles_types.ml     |  143 +-
 plugins/funind/functional_principles_types.mli    |    6 +-
 plugins/funind/g_indfun.ml4                       |    6 +-
 plugins/funind/glob_term_to_relation.ml           |   54 +-
 plugins/funind/glob_term_to_relation.mli          |    7 +-
 plugins/funind/indfun.ml                          |  221 +-
 plugins/funind/indfun_common.ml                   |    6 +-
 plugins/funind/indfun_common.mli                  |    2 +-
 plugins/funind/invfun.ml                          |  517 ++---
 plugins/funind/recdef.ml                          |  118 +-
 plugins/micromega/MExtraction.v                   |    2 +-
 plugins/omega/Omega.v                             |    8 +-
 plugins/omega/OmegaPlugin.v                       |    6 +
 toplevel/whelp.mli => plugins/omega/OmegaTactic.v |   15 +-
 plugins/omega/vo.itarget                          |    1 +
 plugins/quote/quote.ml                            |    4 +-
 pretyping/cases.ml                                |   33 +-
 pretyping/classops.ml                             |    6 +-
 pretyping/constr_matching.ml                      |   74 +-
 pretyping/detyping.ml                             |   11 +-
 pretyping/evarconv.ml                             |   26 +-
 pretyping/evarsolve.ml                            |  163 +-
 pretyping/evarutil.ml                             |   13 +-
 pretyping/evarutil.mli                            |   10 +
 pretyping/evd.ml                                  |   55 +-
 pretyping/evd.mli                                 |   14 +-
 pretyping/find_subterm.ml                         |    1 -
 pretyping/find_subterm.mli                        |    1 -
 pretyping/glob_ops.mli                            |    3 +
 pretyping/inductiveops.ml                         |   21 +-
 pretyping/inductiveops.mli                        |   10 +-
 pretyping/patternops.ml                           |   52 +-
 pretyping/patternops.mli                          |    3 +-
 pretyping/pretyping.ml                            |   10 +-
 pretyping/pretyping.mli                           |    2 +-
 pretyping/reductionops.ml                         |   52 +-
 pretyping/reductionops.mli                        |    7 +-
 pretyping/retyping.ml                             |    5 +-
 pretyping/tacred.ml                               |   14 +-
 pretyping/termops.ml                              |    1 -
 pretyping/termops.mli                             |    1 -
 pretyping/typeclasses.ml                          |   11 -
 pretyping/typeclasses.mli                         |    2 -
 pretyping/typeclasses_errors.ml                   |    1 -
 pretyping/typeclasses_errors.mli                  |    1 -
 pretyping/typing.mli                              |    1 -
 pretyping/unification.ml                          |   13 +-
 pretyping/vnorm.ml                                |   17 +-
 printing/ppconstrsig.mli                          |    2 -
 printing/pptactic.mli                             |    5 +-
 printing/pptacticsig.mli                          |    1 -
 printing/ppvernac.ml                              |   17 +-
 printing/prettyp.ml                               |   14 +-
 printing/printer.ml                               |   61 +-
 printing/printer.mli                              |    6 +-
 printing/richprinter.ml                           |    7 +-
 printing/richprinter.mli                          |    4 +-
 proofs/clenv.mli                                  |    1 -
 proofs/clenvtac.mli                               |    1 -
 proofs/goal.ml                                    |    2 -
 proofs/logic.ml                                   |   12 -
 proofs/pfedit.ml                                  |   35 +
 proofs/pfedit.mli                                 |    8 +
 proofs/proof.mli                                  |    2 +-
 proofs/proof_global.ml                            |   32 +-
 proofs/proof_global.mli                           |    6 +-
 proofs/proof_type.ml                              |    1 -
 proofs/proof_type.mli                             |    1 -
 proofs/proofview.ml                               |   72 +-
 proofs/proofview.mli                              |   10 +-
 proofs/redexpr.ml                                 |    2 +-
 stm/asyncTaskQueue.ml                             |    4 +-
 stm/asyncTaskQueue.mli                            |    2 +
 stm/lemmas.ml                                     |  101 +-
 stm/lemmas.mli                                    |    1 -
 stm/spawned.ml                                    |    5 +-
 stm/stm.ml                                        |  396 ++--
 stm/tQueue.ml                                     |    2 +-
 stm/tQueue.mli                                    |    4 +-
 stm/texmacspp.ml                                  |   31 +-
 stm/vernac_classifier.ml                          |    7 +-
 stm/vio_checking.ml                               |    2 +-
 tactics/auto.ml                                   |    5 +-
 tactics/auto.mli                                  |    1 -
 tactics/autorewrite.ml                            |    1 +
 tactics/btermdn.ml                                |    2 +-
 tactics/btermdn.mli                               |    2 +-
 tactics/class_tactics.ml                          |   32 +-
 tactics/contradiction.ml                          |    2 -
 tactics/coretactics.ml4                           |   30 +-
 tactics/dn.ml                                     |    2 +-
 tactics/dn.mli                                    |    2 +-
 tactics/dnet.ml                                   |   14 +-
 tactics/dnet.mli                                  |    2 +
 tactics/eauto.ml4                                 |   94 +-
 tactics/eauto.mli                                 |    1 -
 tactics/elim.ml                                   |    1 -
 tactics/equality.ml                               |   18 +-
 tactics/equality.mli                              |    1 -
 tactics/evar_tactics.ml                           |    7 +-
 tactics/evar_tactics.mli                          |    1 -
 tactics/extratactics.ml4                          |   30 +-
 tactics/hints.ml                                  |  227 +-
 tactics/hints.mli                                 |   20 +-
 tactics/hipattern.mli                             |    3 -
 tactics/inv.mli                                   |    1 -
 tactics/leminv.ml                                 |   14 +-
 tactics/leminv.mli                                |    1 -
 tactics/rewrite.ml                                |   47 +-
 tactics/taccoerce.ml                              |    7 +
 tactics/tacenv.ml                                 |    2 -
 tactics/tacintern.ml                              |   12 +-
 tactics/tacintern.mli                             |    1 -
 tactics/tacinterp.ml                              |  183 +-
 tactics/tacsubst.ml                               |   14 +-
 tactics/tacticals.ml                              |   24 +-
 tactics/tacticals.mli                             |    4 +-
 tactics/tactics.ml                                |  110 +-
 tactics/tactics.mli                               |    5 +-
 tactics/term_dnet.ml                              |   12 +
 tactics/term_dnet.mli                             |    2 +
 test-suite/Makefile                               |    1 +
 test-suite/_CoqProject                            |    1 +
 test-suite/bugs/closed/1704.v                     |    1 +
 test-suite/bugs/closed/2378.v                     |    1 +
 test-suite/bugs/closed/2406.v                     |    2 +-
 test-suite/bugs/closed/2473.v                     |    1 +
 test-suite/bugs/closed/2590.v                     |   20 +
 test-suite/bugs/closed/2602.v                     |    8 +
 test-suite/bugs/closed/2613.v                     |    1 +
 test-suite/bugs/closed/2615.v                     |    1 +
 test-suite/bugs/closed/2775.v                     |    6 +
 test-suite/bugs/closed/2830.v                     |    1 +
 test-suite/bugs/closed/2883.v                     |    1 +
 test-suite/bugs/closed/2946.v                     |    8 +
 test-suite/bugs/closed/2951.v                     |    2 +
 test-suite/bugs/closed/2969.v                     |    1 +
 test-suite/bugs/closed/2996.v                     |    1 +
 test-suite/bugs/closed/3068.v                     |    1 +
 test-suite/bugs/{opened => closed}/3071.v         |    2 +-
 test-suite/bugs/closed/3199.v                     |   18 +
 test-suite/bugs/closed/3210.v                     |   22 +
 test-suite/bugs/closed/3249.v                     |   11 +
 test-suite/bugs/closed/3258.v                     |    1 +
 test-suite/bugs/closed/3259.v                     |    1 +
 test-suite/bugs/{opened => closed}/3298.v         |    7 +-
 test-suite/bugs/closed/3309.v                     |   10 +-
 test-suite/bugs/closed/3314.v                     |    1 +
 test-suite/bugs/closed/3319.v                     |    1 +
 test-suite/bugs/closed/3321.v                     |    1 +
 test-suite/bugs/closed/3322.v                     |    1 +
 test-suite/bugs/closed/3323.v                     |    1 +
 test-suite/bugs/closed/3324.v                     |    1 +
 test-suite/bugs/closed/3329.v                     |    1 +
 test-suite/bugs/closed/3330.v                     |    1 +
 test-suite/bugs/closed/3344.v                     |    1 +
 test-suite/bugs/closed/3347.v                     |    1 +
 test-suite/bugs/closed/3350.v                     |    1 +
 test-suite/bugs/closed/3373.v                     |    1 +
 test-suite/bugs/closed/3374.v                     |    1 +
 test-suite/bugs/closed/3375.v                     |    1 +
 test-suite/bugs/closed/3382.v                     |    1 +
 test-suite/bugs/closed/3392.v                     |    8 +-
 test-suite/bugs/closed/3393.v                     |    1 +
 test-suite/bugs/closed/3422.v                     |    1 +
 test-suite/bugs/closed/3427.v                     |    1 +
 test-suite/bugs/closed/3439.v                     |    1 +
 test-suite/bugs/{opened => closed}/3467.v         |    2 +-
 test-suite/bugs/closed/3480.v                     |    1 +
 test-suite/bugs/closed/3484.v                     |    1 +
 test-suite/bugs/{opened => closed}/3490.v         |    0
 test-suite/bugs/closed/3491.v                     |    4 +
 test-suite/bugs/closed/3513.v                     |   76 +
 test-suite/bugs/closed/3531.v                     |    1 +
 test-suite/bugs/closed/3560.v                     |   15 +
 test-suite/bugs/closed/3561.v                     |    1 +
 test-suite/bugs/closed/3590.v                     |   12 +
 test-suite/bugs/closed/3596.v                     |    1 +
 test-suite/bugs/closed/3612.v                     |   47 +
 test-suite/bugs/closed/3625.v                     |    1 +
 test-suite/bugs/closed/3647.v                     |    1 +
 test-suite/bugs/closed/3649.v                     |   57 +
 test-suite/bugs/closed/3653.v                     |    1 +
 test-suite/bugs/closed/3658.v                     |    1 +
 test-suite/bugs/closed/3660.v                     |    1 +
 test-suite/bugs/closed/3664.v                     |    1 +
 test-suite/bugs/closed/3668.v                     |    1 +
 test-suite/bugs/{opened => closed}/3681.v         |    0
 test-suite/bugs/closed/3682.v                     |    1 +
 test-suite/bugs/closed/3684.v                     |    1 +
 test-suite/bugs/closed/3686.v                     |    1 +
 test-suite/bugs/closed/3690.v                     |   52 +
 test-suite/bugs/closed/3698.v                     |    1 +
 test-suite/bugs/closed/3699.v                     |    1 +
 test-suite/bugs/closed/3703.v                     |   32 +
 test-suite/bugs/closed/3709.v                     |    1 +
 test-suite/bugs/closed/3732.v                     |  105 +
 test-suite/bugs/closed/3755.v                     |   16 +
 test-suite/bugs/closed/3782.v                     |    1 +
 test-suite/bugs/closed/3783.v                     |   33 +
 test-suite/bugs/{opened => closed}/3786.v         |   13 +-
 test-suite/bugs/closed/3798.v                     |   12 +
 test-suite/bugs/closed/3808.v                     |    2 +
 test-suite/bugs/closed/3815.v                     |    9 +
 test-suite/bugs/closed/3854.v                     |    1 +
 test-suite/bugs/closed/3881.v                     |   35 +
 test-suite/bugs/closed/3900.v                     |   13 +
 test-suite/bugs/closed/3916.v                     |    3 +
 test-suite/bugs/closed/3922.v                     |   84 +
 test-suite/bugs/closed/3938.v                     |    8 +
 test-suite/bugs/closed/3944.v                     |    5 +
 test-suite/bugs/closed/3953.v                     |    5 +
 test-suite/bugs/closed/3960.v                     |   26 +
 test-suite/bugs/closed/3978.v                     |   27 +
 test-suite/bugs/closed/3993.v                     |    3 +
 test-suite/bugs/closed/4001.v                     |   18 +
 test-suite/bugs/closed/4012.v                     |    5 +
 test-suite/bugs/closed/4016.v                     |   12 +
 test-suite/bugs/closed/4017.v                     |    8 +
 test-suite/bugs/closed/4018.v                     |    3 +
 test-suite/bugs/closed/4031.v                     |   14 +
 test-suite/bugs/closed/4035.v                     |   13 +
 test-suite/bugs/closed/4046.v                     |    6 +
 test-suite/bugs/closed/4078.v                     |   14 +
 test-suite/bugs/closed/4089.v                     |  374 ++++
 test-suite/bugs/closed/4097.v                     |   65 +
 test-suite/bugs/closed/4101.v                     |   19 +
 test-suite/bugs/closed/4103.v                     |   12 +
 test-suite/bugs/closed/4120.v                     |    5 +
 test-suite/bugs/closed/4121.v                     |   15 +
 test-suite/bugs/closed/4165.v                     |    7 +
 test-suite/bugs/closed/4190.v                     |   15 +
 test-suite/bugs/closed/4193.v                     |    7 +
 test-suite/bugs/closed/HoTT_coq_007.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_014.v             |    2 +
 test-suite/bugs/closed/HoTT_coq_020.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_029.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_030.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_035.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_042.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_055.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_056.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_058.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_061.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_062.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_064.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_067.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_088.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_090.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_098.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_099.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_100.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_101.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_102.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_107.v             |    6 +-
 test-suite/bugs/closed/HoTT_coq_108.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_112.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_113.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_118.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_121.v             |    1 +
 test-suite/bugs/closed/HoTT_coq_123.v             |    1 +
 test-suite/bugs/{closed => opened}/2456.v         |    4 +-
 test-suite/bugs/opened/2951.v                     |    1 -
 test-suite/bugs/opened/3263.v                     |    1 +
 test-suite/bugs/opened/3345.v                     |    1 +
 test-suite/bugs/opened/3395.v                     |    1 +
 test-suite/bugs/opened/3491.v                     |    2 -
 test-suite/bugs/opened/3509.v                     |    1 +
 test-suite/bugs/opened/3510.v                     |    1 +
 test-suite/bugs/{closed => opened}/3593.v         |    2 +-
 test-suite/bugs/opened/3685.v                     |    1 +
 test-suite/bugs/opened/3754.v                     |    1 +
 test-suite/bugs/opened/3794.v                     |    7 +
 test-suite/bugs/{closed => opened}/3848.v         |    3 +-
 test-suite/bugs/opened/HoTT_coq_120.v             |    1 +
 test-suite/complexity/bug4076.v                   |   29 +
 test-suite/complexity/bug4076bis.v                |   31 +
 test-suite/ide/undo020.fake                       |    4 +-
 test-suite/output/Arguments.out                   |   17 +-
 test-suite/output/ArgumentsScope.out              |   14 -
 test-suite/output/Arguments_renaming.out          |   23 +-
 test-suite/output/Cases.out                       |    9 -
 test-suite/output/Errors.out                      |    8 +-
 test-suite/output/Implicit.out                    |    1 -
 test-suite/output/Notations.out                   |   22 +-
 test-suite/output/PrintInfos.out                  |    9 -
 test-suite/output/TranspModtype.out               |    8 -
 test-suite/output/inference.out                   |    2 -
 test-suite/output/names.out                       |    1 -
 test-suite/output/rewrite-2172.out                |    2 +-
 test-suite/output/simpl.v                         |    6 +-
 test-suite/prerequisite/admit.v                   |    2 +
 test-suite/success/AdvancedCanonicalStructure.v   |    1 +
 test-suite/success/Case22.v                       |   12 +
 test-suite/success/Inductive.v                    |   41 +
 test-suite/success/Injection.v                    |    2 +
 test-suite/success/Nsatz.v                        |    1 +
 test-suite/success/TacticNotation1.v              |   20 +
 test-suite/success/apply.v                        |   10 +
 test-suite/success/coindprim.v                    |   52 +
 test-suite/success/proof_using.v                  |    1 +
 test-suite/success/qed_export.v                   |   18 +
 test-suite/success/rewrite.v                      |   10 +
 test-suite/success/rewrite_dep.v                  |    1 +
 test-suite/success/setoid_test.v                  |    1 +
 test-suite/success/simpl.v                        |    1 +
 test-suite/success/tryif.v                        |   50 +
 theories/Classes/CMorphisms.v                     |   24 +-
 theories/Init/Logic.v                             |    3 -
 theories/Init/Notations.v                         |    2 +-
 theories/Init/Prelude.v                           |    2 +-
 theories/Init/Tactics.v                           |   14 +-
 theories/Lists/List.v                             |   10 +-
 theories/Lists/SetoidList.v                       |   11 +-
 theories/Lists/SetoidPermutation.v                |   74 +-
 theories/MMaps/MMapAVL.v                          | 2158 ++++++++++++++++++
 theories/MMaps/MMapFacts.v                        | 2434 +++++++++++++++++++++
 theories/MMaps/MMapInterface.v                    |  292 +++
 theories/MMaps/MMapList.v                         | 1144 ++++++++++
 theories/MMaps/MMapPositive.v                     |  698 ++++++
 theories/MMaps/MMapWeakList.v                     |  687 ++++++
 lib/dyn.mli => theories/MMaps/MMaps.v             |   28 +-
 theories/MMaps/vo.itarget                         |    7 +
 theories/MSets/MSetAVL.v                          |   18 +-
 theories/MSets/MSetPositive.v                     |   81 +-
 theories/Program/Equality.v                       |   11 +-
 theories/Program/Utils.v                          |    2 +-
 theories/Reals/Alembert.v                         |    1 +
 theories/Reals/Cos_rel.v                          |    7 +-
 theories/Reals/PSeries_reg.v                      |    6 +
 theories/Reals/Ratan.v                            |   10 +
 theories/Structures/EqualitiesFacts.v             |  216 +-
 theories/Structures/OrdersEx.v                    |   67 +
 theories/Structures/OrdersLists.v                 |  211 +-
 theories/ZArith/Int.v                             |  193 +-
 theories/theories.itarget                         |    1 +
 tools/coq_makefile.ml                             |   80 +-
 tools/coq_tex.ml                                  |    3 +-
 tools/coqc.ml                                     |    4 +-
 tools/coqdoc/cpretty.mll                          |   12 +-
 tools/coqdoc/output.ml                            |    1 -
 toplevel/auto_ind_decl.mli                        |    1 -
 toplevel/cerrors.ml                               |   46 +-
 toplevel/cerrors.mli                              |    2 +-
 toplevel/classes.ml                               |   15 +-
 toplevel/classes.mli                              |    3 +-
 toplevel/command.ml                               |   19 +-
 toplevel/command.mli                              |    3 +-
 toplevel/coqinit.ml                               |   33 +-
 toplevel/coqinit.mli                              |    4 +-
 toplevel/coqtop.ml                                |   18 +-
 toplevel/himsg.ml                                 |    4 +-
 toplevel/indschemes.ml                            |    2 +-
 toplevel/metasyntax.ml                            |   33 +-
 toplevel/mltop.ml                                 |   19 +-
 toplevel/mltop.mli                                |    1 -
 toplevel/obligations.ml                           |   24 +-
 toplevel/obligations.mli                          |    7 +-
 toplevel/record.ml                                |    7 +-
 toplevel/toplevel.mllib                           |    1 -
 toplevel/usage.ml                                 |   10 +-
 toplevel/vernacentries.ml                         |   98 +-
 toplevel/vernacinterp.ml                          |   22 +-
 toplevel/vernacinterp.mli                         |    8 +-
 toplevel/whelp.ml4                                |  224 --
 552 files changed, 14745 insertions(+), 4358 deletions(-)
 delete mode 100644 INSTALL.macosx
 delete mode 100644 dev/TODO
 create mode 100644 plugins/extraction/ExtrHaskellBasic.v
 create mode 100644 plugins/extraction/json.ml
 create mode 100644 plugins/extraction/json.mli
 rename toplevel/whelp.mli => plugins/omega/OmegaTactic.v (68%)
 create mode 100644 test-suite/_CoqProject
 create mode 100644 test-suite/bugs/closed/2590.v
 create mode 100644 test-suite/bugs/closed/2602.v
 create mode 100644 test-suite/bugs/closed/2775.v
 create mode 100644 test-suite/bugs/closed/2946.v
 create mode 100644 test-suite/bugs/closed/2951.v
 rename test-suite/bugs/{opened => closed}/3071.v (82%)
 create mode 100644 test-suite/bugs/closed/3199.v
 create mode 100644 test-suite/bugs/closed/3210.v
 create mode 100644 test-suite/bugs/closed/3249.v
 rename test-suite/bugs/{opened => closed}/3298.v (79%)
 rename test-suite/bugs/{opened => closed}/3467.v (78%)
 rename test-suite/bugs/{opened => closed}/3490.v (100%)
 create mode 100644 test-suite/bugs/closed/3491.v
 create mode 100644 test-suite/bugs/closed/3513.v
 create mode 100644 test-suite/bugs/closed/3560.v
 create mode 100644 test-suite/bugs/closed/3590.v
 create mode 100644 test-suite/bugs/closed/3612.v
 create mode 100644 test-suite/bugs/closed/3649.v
 rename test-suite/bugs/{opened => closed}/3681.v (100%)
 create mode 100644 test-suite/bugs/closed/3690.v
 create mode 100644 test-suite/bugs/closed/3703.v
 create mode 100644 test-suite/bugs/closed/3732.v
 create mode 100644 test-suite/bugs/closed/3755.v
 create mode 100644 test-suite/bugs/closed/3783.v
 rename test-suite/bugs/{opened => closed}/3786.v (80%)
 create mode 100644 test-suite/bugs/closed/3798.v
 create mode 100644 test-suite/bugs/closed/3808.v
 create mode 100644 test-suite/bugs/closed/3815.v
 create mode 100644 test-suite/bugs/closed/3881.v
 create mode 100644 test-suite/bugs/closed/3900.v
 create mode 100644 test-suite/bugs/closed/3916.v
 create mode 100644 test-suite/bugs/closed/3922.v
 create mode 100644 test-suite/bugs/closed/3938.v
 create mode 100644 test-suite/bugs/closed/3944.v
 create mode 100644 test-suite/bugs/closed/3953.v
 create mode 100644 test-suite/bugs/closed/3960.v
 create mode 100644 test-suite/bugs/closed/3978.v
 create mode 100644 test-suite/bugs/closed/3993.v
 create mode 100644 test-suite/bugs/closed/4001.v
 create mode 100644 test-suite/bugs/closed/4012.v
 create mode 100644 test-suite/bugs/closed/4016.v
 create mode 100644 test-suite/bugs/closed/4017.v
 create mode 100644 test-suite/bugs/closed/4018.v
 create mode 100644 test-suite/bugs/closed/4031.v
 create mode 100644 test-suite/bugs/closed/4035.v
 create mode 100644 test-suite/bugs/closed/4046.v
 create mode 100644 test-suite/bugs/closed/4078.v
 create mode 100644 test-suite/bugs/closed/4089.v
 create mode 100644 test-suite/bugs/closed/4097.v
 create mode 100644 test-suite/bugs/closed/4101.v
 create mode 100644 test-suite/bugs/closed/4103.v
 create mode 100644 test-suite/bugs/closed/4120.v
 create mode 100644 test-suite/bugs/closed/4121.v
 create mode 100644 test-suite/bugs/closed/4165.v
 create mode 100644 test-suite/bugs/closed/4190.v
 create mode 100644 test-suite/bugs/closed/4193.v
 rename test-suite/bugs/{closed => opened}/2456.v (97%)
 delete mode 100644 test-suite/bugs/opened/2951.v
 delete mode 100644 test-suite/bugs/opened/3491.v
 rename test-suite/bugs/{closed => opened}/3593.v (77%)
 create mode 100644 test-suite/bugs/opened/3794.v
 rename test-suite/bugs/{closed => opened}/3848.v (91%)
 create mode 100644 test-suite/complexity/bug4076.v
 create mode 100644 test-suite/complexity/bug4076bis.v
 create mode 100644 test-suite/prerequisite/admit.v
 create mode 100644 test-suite/success/TacticNotation1.v
 create mode 100644 test-suite/success/coindprim.v
 create mode 100644 test-suite/success/qed_export.v
 create mode 100644 test-suite/success/tryif.v
 create mode 100644 theories/MMaps/MMapAVL.v
 create mode 100644 theories/MMaps/MMapFacts.v
 create mode 100644 theories/MMaps/MMapInterface.v
 create mode 100644 theories/MMaps/MMapList.v
 create mode 100644 theories/MMaps/MMapPositive.v
 create mode 100644 theories/MMaps/MMapWeakList.v
 copy lib/dyn.mli => theories/MMaps/MMaps.v (53%)
 create mode 100644 theories/MMaps/vo.itarget
 delete mode 100644 toplevel/whelp.ml4

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git

_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

Reply via email to