. |-- azure-pipelines.yml |-- checker | |-- analyze.ml | |-- analyze.mli | |-- checker.ml | |-- checker.mli | |-- checkFlags.ml | |-- checkFlags.mli | |-- checkInductive.ml | |-- checkInductive.mli | |-- check.ml | |-- check.mli | |-- check.mllib | |-- check_stat.ml | |-- check_stat.mli | |-- checkTypes.ml | |-- checkTypes.mli | |-- coqchk.ml | |-- coqchk.mli | |-- dune | |-- include | |-- mod_checking.ml | |-- mod_checking.mli | |-- safe_checking.ml | |-- safe_checking.mli | |-- validate.ml | |-- validate.mli | |-- values.ml | |-- values.mli | |-- votour.ml | |-- votour.mli |-- clib | |-- bigint.ml | |-- bigint.mli | |-- cArray.ml | |-- cArray.mli | |-- cEphemeron.ml | |-- cEphemeron.mli | |-- clib.mllib | |-- cList.ml | |-- cList.mli | |-- cMap.ml | |-- cMap.mli | |-- cObj.ml | |-- cObj.mli | |-- cSet.ml | |-- cSet.mli | |-- cSig.mli | |-- cString.ml | |-- cString.mli | |-- cThread.ml | |-- cThread.mli | |-- cUnix.ml | |-- cUnix.mli | |-- diff2.ml | |-- diff2.mli | |-- dune | |-- dyn.ml | |-- dyn.mli | |-- exninfo.ml | |-- exninfo.mli | |-- hashcons.ml | |-- hashcons.mli | |-- hashset.ml | |-- hashset.mli | |-- heap.ml | |-- heap.mli | |-- hMap.ml | |-- hMap.mli | |-- int.ml | |-- int.mli | |-- iStream.ml | |-- iStream.mli | |-- minisys.ml | |-- monad.ml | |-- monad.mli | |-- option.ml | |-- option.mli | |-- orderedType.ml | |-- orderedType.mli | |-- predicate.ml | |-- predicate.mli | |-- range.ml | |-- range.mli | |-- segmenttree.ml | |-- segmenttree.mli | |-- store.ml | |-- store.mli | |-- terminal.ml | |-- terminal.mli | |-- trie.ml | |-- trie.mli | |-- unicode.ml | |-- unicode.mli | |-- unicodetable.ml | |-- unionfind.ml | |-- unionfind.mli |-- CODE_OF_CONDUCT.md |-- config | |-- config.mllib | |-- coq_config.mli | |-- dune |-- configure |-- configure.ml |-- CONTRIBUTING.md |-- coq-8-sources-tree.txt |-- coq-doc.opam |-- coqide.opam |-- coqide-server.opam |-- coq.opam |-- coq.opam.docker |-- coqpp | |-- coqpp_ast.mli | |-- coqpp_lex.mll | |-- coqpp_main.ml | |-- coqpp_parse.mly | |-- coqpp_parser.ml | |-- coqpp_parser.mli | |-- dune |-- CREDITS |-- default.nix |-- dev | |-- base_db | |-- base_include | |-- bugzilla2github_stripped.csv | |-- Bugzilla_Coq_autolink.user.js | |-- build | | |-- osx | | | |-- make-macos-dmg.sh | | |-- windows | | |-- CAVEATS.txt | | |-- configure_profile.sh | | |-- difftar-folder.sh | | |-- MakeCoq_explicitcachefolders_installer.bat | | |-- MakeCoq_local_installer.bat | | |-- MakeCoq_master_installer.bat | | |-- MakeCoq_MinGW.bat | | |-- makecoq_mingw.sh | | |-- MakeCoq_regtest_noproxy.bat | | |-- MakeCoq_regtests.bat | | |-- MakeCoq_SetRootPath.bat | | |-- patches_coq | | | |-- coq_new.nsi | | | |-- flexdll-0.37.patch | | | |-- isl-0.14.patch | | | |-- lablgtk-3.0.beta5.patch | | | |-- ln.c | | | |-- ocaml-4.07.1.patch | | | |-- pkg-config.c | | | |-- quickchick.patch | | | |-- ReplaceInFile.nsh | | | |-- sed-4.2.2-3.src.patch | | | |-- sed-4.2.2.patch | | | |-- StrRep.nsh | | |-- ReadMe.txt | |-- ci | | |-- azure-build.sh | | |-- azure-opam.sh | | |-- azure-test.sh | | |-- ci-aac_tactics.sh | | |-- ci-argosy.sh | | |-- ci-basic-overlay.sh | | |-- ci-bbv.sh | | |-- ci-bedrock2.sh | | |-- ci-bignums.sh | | |-- ci-color.sh | | |-- ci-common.sh | | |-- ci-compcert.sh | | |-- ci-coq_dpdgraph.sh | | |-- ci-coqhammer.sh | | |-- ci-coqprime.sh | | |-- ci-coq_tools.sh | | |-- ci-coquelicot.sh | | |-- ci-corn.sh | | |-- ci-cross_crypto.sh | | |-- ci-elpi.sh | | |-- ci-equations.sh | | |-- ci-ext_lib.sh | | |-- ci-fcsl_pcm.sh | | |-- ci-fiat_crypto_ocaml.sh | | |-- ci-fiat_crypto.sh | | |-- ci-fiat_parsers.sh | | |-- ci-flocq.sh | | |-- ci-geocoq.sh | | |-- ci-hott.sh | | |-- ci-lambda_rust.sh | | |-- ci-math_classes.sh | | |-- ci-mathcomp.sh | | |-- ci-metacoq.sh | | |-- ci-mtac2.sh | | |-- ci-paramcoq.sh | | |-- ci-perennial.sh | | |-- ci-quickchick.sh | | |-- ci-reduction_effects.sh | | |-- ci-relation_algebra.sh | | |-- ci-rewriter.sh | | |-- ci-sf.sh | | |-- ci-simple_io.sh | | |-- ci-stdlib2.sh | | |-- ci-tlc.sh | | |-- ci-unicoq.sh | | |-- ci-unimath.sh | | |-- ci-verdi_raft.sh | | |-- ci-vst.sh | | |-- ci-wrapper.sh | | |-- docker | | | |-- bionic_coq | | | | |-- Dockerfile | | | |-- README.md | | |-- gitlab.bat | | |-- nix | | | |-- bedrock2.nix | | | |-- bignums.nix | | | |-- CoLoR.nix | | | |-- CompCert.nix | | | |-- coq_dpdgraph.nix | | | |-- coq.nix | | | |-- coquelicot.nix | | | |-- Corn.nix | | | |-- cross_crypto.nix | | | |-- default.nix | | | |-- Elpi.nix | | | |-- fiat_crypto.nix | | | |-- flocq.nix | | | |-- formal-topology.nix | | | |-- GeoCoq.nix | | | |-- HoTT.nix | | | |-- iris.nix | | | |-- lambda-rust.nix | | | |-- math_classes.nix | | | |-- mtac2.nix | | | |-- oddorder.nix | | | |-- quickchick.nix | | | |-- README.md | | | |-- shell | | | |-- unicoq | | | | |-- default.nix | | | | |-- unicoq-num.patch | | | |-- verdi-raft.nix | | | |-- VST.nix | | |-- README-developers.md | | |-- README.md | | |-- README-users.md | | |-- user-overlays | | |-- 10185-SkySkimmer-instance-no-bang.sh | | |-- 11566-ejgallego-exninfo+coercion.sh | | |-- 11703-herbelin-master+turning-numTok-into-a-numeral-API.sh | | |-- 11731-ejgallego-proof+more_naming_unif.sh | | |-- 11812-ppedrot-export-hint-globality.sh | | |-- 11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh | | |-- 11820-SkySkimmer-partial-import.sh | | |-- 11896-ppedrot-evar-inst-list.sh | | |-- 11922-ppedrot-rm-local-reductionops.sh | | |-- 11948-proux01-hexadecimal.sh | | |-- 12023-herbelin-master+fixing-empty-Ltac-v-file.sh | | |-- 12107-SkySkimmer-no-mod-univs.sh | | |-- 12227-ppedrot-refiner-rm-v82.sh | | |-- 12267-gares-elpi-1.11.sh | | |-- 12523-term-notation-custom.sh | | |-- 12650-SkySkimmer-rebuild-record.sh | | |-- 8808-herbelin-master+support-binder+term-in-abbrev.sh | | |-- 8855-herbelin-master+more-search-options.sh | | |-- README.md | |-- Coq_Bugzilla_autolink.user.js | |-- core.dbg | |-- core_dune.dbg | |-- db | |-- doc | | |-- archive | | | |-- COMPATIBILITY | | | |-- extensions.txt | | | |-- naming-conventions.tex | | | |-- newsyntax.tex | | | |-- notes-on-conversion.v | | | |-- old_svn_branches.txt | | | |-- perf-analysis | | | |-- versions-history.tex | | |-- build-system.dev.txt | | |-- build-system.dune.md | | |-- build-system.txt | | |-- changes.md | | |-- coq-src-description.txt | | |-- critical-bugs | | |-- debugging.md | | |-- drop.txt | | |-- econstr.md | | |-- INSTALL.make.md | | |-- primproj.md | | |-- profiling.txt | | |-- proof-engine.md | | |-- README.md | | |-- release-process.md | | |-- shield-icon.png | | |-- SProp.md | | |-- style.txt | | |-- unification.txt | | |-- universes.md | | |-- xml-protocol.md | |-- dune | |-- dune_db | |-- dune_db_408 | |-- dune_db_409 | |-- dune-dbg.in | |-- dune-workspace.all | |-- dynlink.ml | |-- header.c | |-- header.ml | |-- header.py | |-- incdir | |-- incdir_dune | |-- inc_ltac | |-- inc_ltac_dune | |-- include | |-- include_dune | |-- include_printers | |-- lint-commits.sh | |-- lint-repository.sh | |-- macosify_accel.sh | |-- nixpkgs.nix | |-- nsis | | |-- coq.nsi | | |-- FileAssociation.nsh | |-- ocamldebug-coq.run | |-- README.md | |-- shim | | |-- dune | |-- tools | | |-- backport-pr.sh | | |-- change-header | | |-- check-eof-newline.sh | | |-- check-overlays.sh | | |-- check-owners-pr.sh | | |-- check-owners.sh | | |-- coqdev.el | | |-- create_overlays.sh | | |-- generate-release-changelog.sh | | |-- github-check-prs.py | | |-- make-changelog.sh | | |-- make_git_revision.sh | | |-- merge-pr.sh | | |-- objects.el | | |-- pin-ci.sh | | |-- pre-commit | | |-- update-compat.py | |-- top_printers.dbg | |-- top_printers.ml | |-- top_printers.mli | |-- v8-syntax | | |-- check-grammar | | |-- memo-v8.tex | | |-- syntax-v8.tex | |-- vm_printers.ml |-- doc | |-- changelog | | |-- 00-title.rst | | |-- 01-kernel | | | |-- 00000-title.rst | | |-- 02-specification-language | | | |-- 00000-title.rst | | |-- 03-notations | | | |-- 00000-title.rst | | |-- 04-tactics | | | |-- 00000-title.rst | | |-- 05-tactic-language | | | |-- 00000-title.rst | | |-- 06-ssreflect | | | |-- 00000-title.rst | | |-- 07-commands-and-options | | | |-- 00000-title.rst | | |-- 08-tools | | | |-- 00000-title.rst | | |-- 09-coqide | | | |-- 00000-title.rst | | |-- 10-standard-library | | | |-- 00000-title.rst | | |-- 11-infrastructure-and-dependencies | | | |-- 00000-title.rst | | |-- 12-misc | | | |-- 00000-title.rst | | |-- README.md | |-- common | | |-- macros.tex | | |-- styles | | | |-- html | | | |-- coqremote | | | | |-- cover.html | | | | |-- footer.html | | | | |-- header.html | | | | |-- hevea.css | | | | |-- modules | | | | | |-- node | | | | | | |-- node.css | | | | | |-- system | | | | | | |-- defaults.css | | | | | | |-- system.css | | | | | |-- user | | | | | |-- user.css | | | | |-- styles.hva | | | |-- simple | | | |-- cover.html | | | |-- footer.html | | | |-- header.html | | | |-- hevea.css | | | |-- style.css | | | |-- styles.hva | | |-- title.tex | |-- dune | |-- LICENSE | |-- plugin_tutorial | | |-- LICENSE | | |-- Makefile | | |-- README.md | | |-- tuto0 | | | |-- _CoqProject | | | |-- Makefile | | | |-- src | | | | |-- dune | | | | |-- g_tuto0.mlg | | | | |-- tuto0_main.ml | | | | |-- tuto0_main.mli | | | | |-- tuto0_plugin.mlpack | | | |-- theories | | | |-- Demo.v | | | |-- Loader.v | | |-- tuto1 | | | |-- _CoqProject | | | |-- Makefile | | | |-- src | | | | |-- dune | | | | |-- g_tuto1.mlg | | | | |-- inspector.ml | | | | |-- inspector.mli | | | | |-- simple_check.ml | | | | |-- simple_check.mli | | | | |-- simple_declare.ml | | | | |-- simple_declare.mli | | | | |-- simple_print.ml | | | | |-- simple_print.mli | | | | |-- tuto1_plugin.mlpack | | | |-- theories | | | |-- Demo.v | | | |-- Loader.v | | |-- tuto2 | | | |-- _CoqProject | | | |-- Makefile | | | |-- src | | | | |-- counter.ml | | | | |-- counter.mli | | | | |-- custom.ml | | | | |-- custom.mli | | | | |-- dune | | | | |-- g_tuto2.mlg | | | | |-- persistent_counter.ml | | | | |-- persistent_counter.mli | | | | |-- tuto2_plugin.mlpack | | | |-- theories | | | |-- Count.v | | | |-- Demo.v | | | |-- Loader.v | | |-- tuto3 | | |-- _CoqProject | | |-- Makefile | | |-- src | | | |-- construction_game.ml | | | |-- construction_game.mli | | | |-- dune | | | |-- g_tuto3.mlg | | | |-- tuto3_plugin.mlpack | | | |-- tuto_tactic.ml | | | |-- tuto_tactic.mli | | |-- theories | | |-- Data.v | | |-- Loader.v | | |-- test.v | |-- README.md | |-- sphinx | | |-- addendum | | | |-- canonical-structures.rst | | | |-- extended-pattern-matching.rst | | | |-- extraction.rst | | | |-- generalized-rewriting.rst | | | |-- implicit-coercions.rst | | | |-- micromega.rst | | | |-- miscellaneous-extensions.rst | | | |-- nsatz.rst | | | |-- omega.rst | | | |-- parallel-proof-processing.rst | | | |-- program.rst | | | |-- ring.rst | | | |-- sprop.rst | | | |-- type-classes.rst | | | |-- universe-polymorphism.rst | | |-- appendix | | | |-- history-and-changes | | | | |-- index.rst | | | |-- indexes | | | |-- index.rst | | |-- biblio.bib | | |-- changes.rst | | |-- conf.py | | |-- coq-attrindex.rst | | |-- coq-cmdindex.rst | | |-- coq-exnindex.rst | | |-- coq-optindex.rst | | |-- coq-tacindex.rst | | |-- dune | | |-- genindex.rst | | |-- history.rst | | |-- index.html.rst | | |-- index.latex.rst | | |-- introduction.rst | | |-- language | | | |-- cic.rst | | | |-- coq-library.rst | | | |-- core | | | | |-- assumptions.rst | | | | |-- basic.rst | | | | |-- coinductive.rst | | | | |-- conversion.rst | | | | |-- definitions.rst | | | | |-- index.rst | | | | |-- inductive.rst | | | | |-- modules.rst | | | | |-- primitive.rst | | | | |-- records.rst | | | | |-- sections.rst | | | | |-- sorts.rst | | | | |-- variants.rst | | | |-- extensions | | | | |-- arguments-command.rst | | | | |-- canonical.rst | | | | |-- evars.rst | | | | |-- implicit-arguments.rst | | | | |-- index.rst | | | | |-- match.rst | | | |-- gallina-extensions.rst | | | |-- gallina-specification-language.rst | | | |-- module-system.rst | | |-- license.rst | | |-- practical-tools | | | |-- coq-commands.rst | | | |-- coqide.rst | | | |-- utilities.rst | | |-- proof-engine | | | |-- detailed-tactic-examples.rst | | | |-- ltac2.rst | | | |-- ltac.rst | | | |-- proof-handling.rst | | | |-- ssreflect-proof-language.rst | | | |-- tactics.rst | | | |-- vernacular-commands.rst | | |-- proofs | | | |-- automatic-tactics | | | | |-- index.rst | | | |-- creating-tactics | | | | |-- index.rst | | | |-- writing-proofs | | | |-- index.rst | | |-- README.rst | | |-- README.template.rst | | |-- refman-preamble.rst | | |-- refman-preamble.sty | | |-- _static | | | |-- ansi.css | | | |-- ansi-dark.css | | | |-- coqdoc.css | | | |-- coqide.png | | | |-- coqide-queries.png | | | |-- coqnotations.sty | | | |-- CoqNotations.ttf | | | |-- diffs-coqide-compacted.png | | | |-- diffs-coqide-multigoal.png | | | |-- diffs-coqide-on.png | | | |-- diffs-coqide-removed.png | | | |-- diffs-coqtop-compacted.png | | | |-- diffs-coqtop-multigoal.png | | | |-- diffs-coqtop-on3.png | | | |-- diffs-coqtop-on.png | | | |-- diffs-error-message.png | | | |-- notations.css | | | |-- notations.js | | | |-- pre-text.css | | |-- std-glossindex.rst | | |-- _templates | | | |-- versions.html | | |-- user-extensions | | | |-- proof-schemes.rst | | | |-- syntax-extensions.rst | | |-- using | | | |-- libraries | | | | |-- funind.rst | | | | |-- index.rst | | | | |-- writing.rst | | | |-- tools | | | |-- coqdoc.rst | | | |-- index.rst | | |-- zebibliography.html.rst | | |-- zebibliography.latex.rst | |-- stdlib | | |-- dune | | |-- hidden-files | | |-- index-list.html.template | | |-- Library.tex | | |-- make-library-index | |-- tools | | |-- coqrst | | | |-- checkdeps.py | | | |-- coqdoc | | | | |-- __init__.py | | | | |-- main.py | | | |-- coqdomain.py | | | |-- __init__.py | | | |-- notations | | | | |-- CoqNotations.ttf | | | | |-- fontsupport.py | | | | |-- html.py | | | | |-- __init__.py | | | | |-- Makefile | | | | |-- parsing.py | | | | |-- plain.py | | | | |-- regexp.py | | | | |-- sphinx.py | | | | |-- TacticNotations.g | | | | |-- TacticNotationsLexer.py | | | | |-- TacticNotationsLexer.tokens | | | | |-- TacticNotationsParser.py | | | | |-- TacticNotations.tokens | | | | |-- TacticNotationsVisitor.py | | | | |-- UbuntuMono-B.ttf | | | |-- regen_readme.py | | | |-- repl | | | |-- ansicolors.py | | | |-- coqtop.py | | | |-- __init__.py | | |-- docgram | | | |-- common.edit_mlg | | | |-- doc_grammar.ml | | | |-- dune | | | |-- fullGrammar | | | |-- orderedGrammar | | | |-- README.md | | |-- latex_filter | | |-- show_latex_messages | | |-- Translator.tex | |-- whodidwhat | |-- whodidwhat-8.2update.tex | |-- whodidwhat-8.3update.tex | |-- whodidwhat-8.4update.tex | |-- whodidwhat-8.5update.tex |-- dune |-- dune-project |-- engine | |-- dune | |-- eConstr.ml | |-- eConstr.mli | |-- engine.mllib | |-- evar_kinds.ml | |-- evar_kinds.mli | |-- evarutil.ml | |-- evarutil.mli | |-- evd.ml | |-- evd.mli | |-- ftactic.ml | |-- ftactic.mli | |-- logic_monad.ml | |-- logic_monad.mli | |-- namegen.ml | |-- namegen.mli | |-- nameops.ml | |-- nameops.mli | |-- proofview.ml | |-- proofview.mli | |-- proofview_monad.ml | |-- proofview_monad.mli | |-- termops.ml | |-- termops.mli | |-- univGen.ml | |-- univGen.mli | |-- univMinim.ml | |-- univMinim.mli | |-- univNames.ml | |-- univNames.mli | |-- univops.ml | |-- univops.mli | |-- univProblem.ml | |-- univProblem.mli | |-- univSubst.ml | |-- univSubst.mli | |-- uState.ml | |-- uState.mli |-- gramlib | |-- dune | |-- gramext.ml | |-- gramext.mli | |-- gramlib.mllib | |-- grammar.ml | |-- grammar.mli | |-- LICENSE | |-- plexing.ml | |-- plexing.mli | |-- ploc.ml | |-- ploc.mli |-- ide | |-- config_lexer.mli | |-- config_lexer.mll | |-- configwin_ihm.ml | |-- configwin_ihm.mli | |-- configwin_messages.ml | |-- configwin.ml | |-- configwin.mli | |-- configwin_types.ml | |-- coq2.ico | |-- coq_commands.ml | |-- coq_commands.mli | |-- coq.ico | |-- coq_icon.rc | |-- coqide_main.ml | |-- coqide_main.mli | |-- coqide.ml | |-- coqide.mli | |-- coqide_os_specific.mli | |-- coqide_QUARTZ.ml.in | |-- coqide_ui.ml | |-- coqide_ui.mli | |-- coqide_WIN32.ml.in | |-- coqide_X11.ml.in | |-- coq.lang | |-- coq_lex.mli | |-- coq_lex.mll | |-- coq.ml | |-- coq.mli | |-- coqOps.ml | |-- coqOps.mli | |-- coq.png | |-- coq-ssreflect.lang | |-- coq_style.xml | |-- default_bindings_src.ml | |-- document.ml | |-- document.mli | |-- dune | |-- fake_ide.ml | |-- FAQ | |-- fileOps.ml | |-- fileOps.mli | |-- gtk_parsing.ml | |-- gtk_parsing.mli | |-- ide_common.mllib | |-- ide.mllib | |-- idetop.ml | |-- ideutils.ml | |-- ideutils.mli | |-- ide_win32_stubs.c | |-- MacOS | | |-- coqfile.icns | | |-- coqide.icns | | |-- Info.plist.template | |-- macos_prehook.ml | |-- macos_prehook.mli | |-- Make | |-- microPG.ml | |-- microPG.mli | |-- minilib.ml | |-- minilib.mli | |-- preferences.ml | |-- preferences.mli | |-- protocol | | |-- dune | | |-- ideprotocol.mllib | | |-- interface.ml | | |-- richpp.ml | | |-- richpp.mli | | |-- serialize.ml | | |-- serialize.mli | | |-- xml_lexer.mli | | |-- xml_lexer.mll | | |-- xml_parser.ml | | |-- xml_parser.mli | | |-- xml_printer.ml | | |-- xml_printer.mli | | |-- xmlprotocol.ml | | |-- xmlprotocol.mli | |-- sentence.ml | |-- sentence.mli | |-- session.ml | |-- session.mli | |-- tags.ml | |-- tags.mli | |-- unicode_bindings.ml | |-- unicode_bindings.mli | |-- utf8_convert.mli | |-- utf8_convert.mll | |-- wg_Command.ml | |-- wg_Command.mli | |-- wg_Completion.ml | |-- wg_Completion.mli | |-- wg_Detachable.ml | |-- wg_Detachable.mli | |-- wg_Find.ml | |-- wg_Find.mli | |-- wg_MessageView.ml | |-- wg_MessageView.mli | |-- wg_Notebook.ml | |-- wg_Notebook.mli | |-- wg_ProofView.ml | |-- wg_ProofView.mli | |-- wg_RoutedMessageViews.ml | |-- wg_RoutedMessageViews.mli | |-- wg_ScriptView.ml | |-- wg_ScriptView.mli | |-- wg_Segment.ml | |-- wg_Segment.mli |-- INSTALL.md |-- install.sh |-- interp | |-- constrexpr.ml | |-- constrexpr_ops.ml | |-- constrexpr_ops.mli | |-- constrextern.ml | |-- constrextern.mli | |-- constrintern.ml | |-- constrintern.mli | |-- decls.ml | |-- decls.mli | |-- deprecation.ml | |-- deprecation.mli | |-- doc.tex | |-- dumpglob.ml | |-- dumpglob.mli | |-- dune | |-- genintern.ml | |-- genintern.mli | |-- impargs.ml | |-- impargs.mli | |-- implicit_quantifiers.ml | |-- implicit_quantifiers.mli | |-- interp.mllib | |-- modintern.ml | |-- modintern.mli | |-- notation.ml | |-- notation.mli | |-- notation_ops.ml | |-- notation_ops.mli | |-- notation_term.ml | |-- numTok.ml | |-- numTok.mli | |-- reserve.ml | |-- reserve.mli | |-- smartlocate.ml | |-- smartlocate.mli | |-- stdarg.ml | |-- stdarg.mli | |-- syntax_def.ml | |-- syntax_def.mli |-- kernel | |-- byterun | | |-- coq_fix_code.c | | |-- coq_fix_code.h | | |-- coq_float64.h | | |-- coq_interp.c | | |-- coq_interp.h | | |-- coq_memory.c | | |-- coq_memory.h | | |-- coq_uint63_emul.h | | |-- coq_uint63_native.h | | |-- coq_values.c | | |-- coq_values.h | | |-- dune | | |-- libcoqrun.clib | |-- cbytecodes.ml | |-- cbytecodes.mli | |-- cbytegen.ml | |-- cbytegen.mli | |-- cClosure.ml | |-- cClosure.mli | |-- cemitcodes.ml | |-- cemitcodes.mli | |-- clambda.ml | |-- clambda.mli | |-- constr.ml | |-- constr.mli | |-- context.ml | |-- context.mli | |-- conv_oracle.ml | |-- conv_oracle.mli | |-- cooking.ml | |-- cooking.mli | |-- cPrimitives.ml | |-- cPrimitives.mli | |-- csymtable.ml | |-- csymtable.mli | |-- declarations.ml | |-- declareops.ml | |-- declareops.mli | |-- doc.tex | |-- dune | |-- entries.ml | |-- environ.ml | |-- environ.mli | |-- esubst.ml | |-- esubst.mli | |-- evar.ml | |-- evar.mli | |-- float64.ml | |-- float64.mli | |-- genOpcodeFiles.ml | |-- indtypes.ml | |-- indtypes.mli | |-- indTyping.ml | |-- indTyping.mli | |-- inductive.ml | |-- inductive.mli | |-- inferCumulativity.ml | |-- inferCumulativity.mli | |-- kernel.mllib | |-- modops.ml | |-- modops.mli | |-- mod_subst.ml | |-- mod_subst.mli | |-- mod_typing.ml | |-- mod_typing.mli | |-- names.ml | |-- names.mli | |-- nativecode.ml | |-- nativecode.mli | |-- nativeconv.ml | |-- nativeconv.mli | |-- nativelambda.ml | |-- nativelambda.mli | |-- nativelib.ml | |-- nativelib.mli | |-- nativelibrary.ml | |-- nativelibrary.mli | |-- nativevalues.ml | |-- nativevalues.mli | |-- opaqueproof.ml | |-- opaqueproof.mli | |-- primred.ml | |-- primred.mli | |-- reduction.ml | |-- reduction.mli | |-- relevanceops.ml | |-- relevanceops.mli | |-- retroknowledge.ml | |-- retroknowledge.mli | |-- safe_typing.ml | |-- safe_typing.mli | |-- section.ml | |-- section.mli | |-- sorts.ml | |-- sorts.mli | |-- subtyping.ml | |-- subtyping.mli | |-- term.ml | |-- term.mli | |-- term_typing.ml | |-- term_typing.mli | |-- transparentState.ml | |-- transparentState.mli | |-- type_errors.ml | |-- type_errors.mli | |-- typeops.ml | |-- typeops.mli | |-- uGraph.ml | |-- uGraph.mli | |-- uint63_31.ml | |-- uint63_63.ml | |-- uint63.mli | |-- univ.ml | |-- univ.mli | |-- vars.ml | |-- vars.mli | |-- vconv.ml | |-- vconv.mli | |-- vm.ml | |-- vm.mli | |-- vmvalues.ml | |-- vmvalues.mli |-- lib | |-- acyclicGraph.ml | |-- acyclicGraph.mli | |-- aux_file.ml | |-- aux_file.mli | |-- cAst.ml | |-- cAst.mli | |-- cErrors.ml | |-- cErrors.mli | |-- control.ml | |-- control.mli | |-- coqProject_file.ml | |-- coqProject_file.mli | |-- cProfile.ml | |-- cProfile.mli | |-- cWarnings.ml | |-- cWarnings.mli | |-- dAst.ml | |-- dAst.mli | |-- doc.tex | |-- dune | |-- envars.ml | |-- envars.mli | |-- explore.ml | |-- explore.mli | |-- feedback.ml | |-- feedback.mli | |-- flags.ml | |-- flags.mli | |-- future.ml | |-- future.mli | |-- genarg.ml | |-- genarg.mli | |-- hook.ml | |-- hook.mli | |-- lib.mllib | |-- loc.ml | |-- loc.mli | |-- objFile.ml | |-- objFile.mli | |-- pp_diff.ml | |-- pp_diff.mli | |-- pp.ml | |-- pp.mli | |-- remoteCounter.ml | |-- remoteCounter.mli | |-- rtree.ml | |-- rtree.mli | |-- spawn.ml | |-- spawn.mli | |-- stateid.ml | |-- stateid.mli | |-- system.ml | |-- system.mli | |-- util.ml | |-- util.mli | |-- xml_datatype.mli |-- library | |-- coqlib.ml | |-- coqlib.mli | |-- doc.tex | |-- dune | |-- global.ml | |-- global.mli | |-- globnames.ml | |-- globnames.mli | |-- goptions.ml | |-- goptions.mli | |-- lib.ml | |-- lib.mli | |-- libnames.ml | |-- libnames.mli | |-- libobject.ml | |-- libobject.mli | |-- library.mllib | |-- nametab.ml | |-- nametab.mli | |-- states.ml | |-- states.mli | |-- summary.ml | |-- summary.mli |-- LICENSE |-- Makefile |-- Makefile.build |-- Makefile.checker |-- Makefile.ci |-- Makefile.common |-- Makefile.dev |-- Makefile.doc |-- Makefile.dune |-- Makefile.ide |-- Makefile.install |-- Makefile.make |-- Makefile.vofiles |-- man | |-- coqc.1 | |-- coqchk.1 | |-- coqdep.1 | |-- coqdoc.1 | |-- coqide.1 | |-- coq_makefile.1 | |-- coq-tex.1 | |-- coqtop.1 | |-- coqtop.byte.1 | |-- coqtop.opt.1 | |-- coqwc.1 | |-- dune |-- META.coq.in |-- parsing | |-- cLexer.ml | |-- cLexer.mli | |-- dune | |-- extend.ml | |-- g_constr.mlg | |-- g_prim.mlg | |-- notation_gram.ml | |-- notgram_ops.ml | |-- notgram_ops.mli | |-- parsing.mllib | |-- pcoq.ml | |-- pcoq.mli | |-- ppextend.ml | |-- ppextend.mli | |-- tok.ml | |-- tok.mli |-- plugins | |-- btauto | | |-- btauto_plugin.mlpack | | |-- dune | | |-- g_btauto.mlg | | |-- refl_btauto.ml | | |-- refl_btauto.mli | |-- cc | | |-- ccalgo.ml | | |-- ccalgo.mli | | |-- cc_plugin.mlpack | | |-- ccproof.ml | | |-- ccproof.mli | | |-- cctac.ml | | |-- cctac.mli | | |-- dune | | |-- g_congruence.mlg | | |-- README | |-- derive | | |-- derive.ml | | |-- derive.mli | | |-- derive_plugin.mlpack | | |-- dune | | |-- g_derive.mlg | |-- extraction | | |-- big.ml | | |-- CHANGES | | |-- common.ml | | |-- common.mli | | |-- dune | | |-- extract_env.ml | | |-- extract_env.mli | | |-- extraction.ml | | |-- extraction.mli | | |-- extraction_plugin.mlpack | | |-- g_extraction.mlg | | |-- haskell.ml | | |-- haskell.mli | | |-- json.ml | | |-- json.mli | | |-- miniml.ml | | |-- miniml.mli | | |-- mlutil.ml | | |-- mlutil.mli | | |-- modutil.ml | | |-- modutil.mli | | |-- ocaml.ml | | |-- ocaml.mli | | |-- README | | |-- scheme.ml | | |-- scheme.mli | | |-- table.ml | | |-- table.mli | |-- firstorder | | |-- dune | | |-- formula.ml | | |-- formula.mli | | |-- g_ground.mlg | | |-- ground.ml | | |-- ground.mli | | |-- ground_plugin.mlpack | | |-- instances.ml | | |-- instances.mli | | |-- rules.ml | | |-- rules.mli | | |-- sequent.ml | | |-- sequent.mli | | |-- unify.ml | | |-- unify.mli | |-- funind | | |-- dune | | |-- functional_principles_proofs.ml | | |-- functional_principles_proofs.mli | | |-- functional_principles_types.ml | | |-- functional_principles_types.mli | | |-- gen_principle.ml | | |-- gen_principle.mli | | |-- g_indfun.mlg | | |-- glob_termops.ml | | |-- glob_termops.mli | | |-- glob_term_to_relation.ml | | |-- glob_term_to_relation.mli | | |-- indfun_common.ml | | |-- indfun_common.mli | | |-- indfun.ml | | |-- indfun.mli | | |-- invfun.ml | | |-- invfun.mli | | |-- recdef.ml | | |-- recdef.mli | | |-- recdef_plugin.mlpack | |-- ltac | | |-- coretactics.mlg | | |-- dune | | |-- evar_tactics.ml | | |-- evar_tactics.mli | | |-- extraargs.mlg | | |-- extraargs.mli | | |-- extratactics.mlg | | |-- extratactics.mli | | |-- g_auto.mlg | | |-- g_class.mlg | | |-- g_eqdecide.mlg | | |-- g_ltac.mlg | | |-- g_obligations.mlg | | |-- g_rewrite.mlg | | |-- g_tactic.mlg | | |-- leminv.ml | | |-- leminv.mli | | |-- ltac_plugin.mlpack | | |-- pltac.ml | | |-- pltac.mli | | |-- pptactic.ml | | |-- pptactic.mli | | |-- profile_ltac.ml | | |-- profile_ltac.mli | | |-- profile_ltac_tactics.mlg | | |-- rewrite.ml | | |-- rewrite.mli | | |-- tacarg.ml | | |-- tacarg.mli | | |-- taccoerce.ml | | |-- taccoerce.mli | | |-- tacentries.ml | | |-- tacentries.mli | | |-- tacenv.ml | | |-- tacenv.mli | | |-- tacexpr.ml | | |-- tacexpr.mli | | |-- tacintern.ml | | |-- tacintern.mli | | |-- tacinterp.ml | | |-- tacinterp.mli | | |-- tacsubst.ml | | |-- tacsubst.mli | | |-- tactic_debug.ml | | |-- tactic_debug.mli | | |-- tactic_matching.ml | | |-- tactic_matching.mli | | |-- tactic_option.ml | | |-- tactic_option.mli | | |-- tauto.ml | | |-- tauto.mli | | |-- tauto_plugin.mlpack | |-- micromega | | |-- certificate.ml | | |-- certificate.mli | | |-- coq_micromega.ml | | |-- coq_micromega.mli | | |-- csdpcert.ml | | |-- csdpcert.mli | | |-- dune | | |-- g_micromega.mlg | | |-- g_micromega.mli | | |-- g_zify.mlg | | |-- itv.ml | | |-- itv.mli | | |-- LICENSE.sos | | |-- mfourier.ml | | |-- mfourier.mli | | |-- micromega.ml | | |-- micromega.mli | | |-- micromega_plugin.mlpack | | |-- mutils.ml | | |-- mutils.mli | | |-- numCompat.ml | | |-- numCompat.mli | | |-- persistent_cache.ml | | |-- persistent_cache.mli | | |-- polynomial.ml | | |-- polynomial.mli | | |-- simplex.ml | | |-- simplex.mli | | |-- sos_lib.ml | | |-- sos_lib.mli | | |-- sos.ml | | |-- sos.mli | | |-- sos_types.ml | | |-- sos_types.mli | | |-- vect.ml | | |-- vect.mli | | |-- zify.ml | | |-- zify.mli | | |-- zify_plugin.mlpack | |-- nsatz | | |-- dune | | |-- g_nsatz.mlg | | |-- ideal.ml | | |-- ideal.mli | | |-- nsatz.ml | | |-- nsatz.mli | | |-- nsatz_plugin.mlpack | | |-- polynom.ml | | |-- polynom.mli | | |-- utile.ml | | |-- utile.mli | |-- omega | | |-- coq_omega.ml | | |-- coq_omega.mli | | |-- dune | | |-- g_omega.mlg | | |-- omega.ml | | |-- omega_plugin.mlpack | |-- rtauto | | |-- dune | | |-- g_rtauto.mlg | | |-- proof_search.ml | | |-- proof_search.mli | | |-- refl_tauto.ml | | |-- refl_tauto.mli | | |-- rtauto_plugin.mlpack | |-- setoid_ring | | |-- dune | | |-- g_newring.mlg | | |-- newring_ast.ml | | |-- newring_ast.mli | | |-- newring.ml | | |-- newring.mli | | |-- newring_plugin.mlpack | |-- ssr | | |-- dune | | |-- ssrast.mli | | |-- ssrbwd.ml | | |-- ssrbwd.mli | | |-- ssrcommon.ml | | |-- ssrcommon.mli | | |-- ssreflect_plugin.mlpack | | |-- ssrelim.ml | | |-- ssrelim.mli | | |-- ssrequality.ml | | |-- ssrequality.mli | | |-- ssrfwd.ml | | |-- ssrfwd.mli | | |-- ssripats.ml | | |-- ssripats.mli | | |-- ssrparser.mlg | | |-- ssrparser.mli | | |-- ssrprinters.ml | | |-- ssrprinters.mli | | |-- ssrtacticals.ml | | |-- ssrtacticals.mli | | |-- ssrvernac.mlg | | |-- ssrvernac.mli | | |-- ssrview.ml | | |-- ssrview.mli | |-- ssrmatching | | |-- dune | | |-- g_ssrmatching.mlg | | |-- g_ssrmatching.mli | | |-- ssrmatching.ml | | |-- ssrmatching.mli | | |-- ssrmatching_plugin.mlpack | |-- ssrsearch | | |-- dune | | |-- g_search.mlg | | |-- ssrsearch_plugin.mlpack | |-- syntax | |-- dune | |-- float_syntax.ml | |-- float_syntax_plugin.mlpack | |-- g_numeral.mlg | |-- g_string.mlg | |-- int63_syntax.ml | |-- int63_syntax_plugin.mlpack | |-- numeral.ml | |-- numeral.mli | |-- numeral_notation_plugin.mlpack | |-- r_syntax.ml | |-- r_syntax.mli | |-- r_syntax_plugin.mlpack | |-- string_notation.ml | |-- string_notation.mli | |-- string_notation_plugin.mlpack |-- pretyping | |-- arguments_renaming.ml | |-- arguments_renaming.mli | |-- cases.ml | |-- cases.mli | |-- cbv.ml | |-- cbv.mli | |-- coercion.ml | |-- coercion.mli | |-- coercionops.ml | |-- coercionops.mli | |-- constr_matching.ml | |-- constr_matching.mli | |-- detyping.ml | |-- detyping.mli | |-- doc.tex | |-- dune | |-- evarconv.ml | |-- evarconv.mli | |-- evardefine.ml | |-- evardefine.mli | |-- evarsolve.ml | |-- evarsolve.mli | |-- find_subterm.ml | |-- find_subterm.mli | |-- geninterp.ml | |-- geninterp.mli | |-- globEnv.ml | |-- globEnv.mli | |-- glob_ops.ml | |-- glob_ops.mli | |-- glob_term.ml | |-- heads.ml | |-- heads.mli | |-- indrec.ml | |-- indrec.mli | |-- inductiveops.ml | |-- inductiveops.mli | |-- keys.ml | |-- keys.mli | |-- locus.ml | |-- locusops.ml | |-- locusops.mli | |-- ltac_pretype.ml | |-- nativenorm.ml | |-- nativenorm.mli | |-- pattern.ml | |-- patternops.ml | |-- patternops.mli | |-- pretype_errors.ml | |-- pretype_errors.mli | |-- pretyping.ml | |-- pretyping.mli | |-- pretyping.mllib | |-- program.ml | |-- program.mli | |-- recordops.ml | |-- recordops.mli | |-- reductionops.ml | |-- reductionops.mli | |-- retyping.ml | |-- retyping.mli | |-- tacred.ml | |-- tacred.mli | |-- typeclasses_errors.ml | |-- typeclasses_errors.mli | |-- typeclasses.ml | |-- typeclasses.mli | |-- typing.ml | |-- typing.mli | |-- unification.ml | |-- unification.mli | |-- vnorm.ml | |-- vnorm.mli |-- printing | |-- dune | |-- genprint.ml | |-- genprint.mli | |-- ppconstr.ml | |-- ppconstr.mli | |-- pputils.ml | |-- pputils.mli | |-- printer.ml | |-- printer.mli | |-- printing.mllib | |-- printmod.ml | |-- printmod.mli | |-- proof_diffs.ml | |-- proof_diffs.mli |-- proofs | |-- clenv.ml | |-- clenv.mli | |-- clenvtac.ml | |-- clenvtac.mli | |-- doc.tex | |-- dune | |-- evar_refiner.ml | |-- evar_refiner.mli | |-- goal.ml | |-- goal.mli | |-- goal_select.ml | |-- goal_select.mli | |-- logic.ml | |-- logic.mli | |-- miscprint.ml | |-- miscprint.mli | |-- proof_bullet.ml | |-- proof_bullet.mli | |-- proof.ml | |-- proof.mli | |-- proofs.mllib | |-- refine.ml | |-- refine.mli | |-- refiner.ml | |-- refiner.mli | |-- tacmach.ml | |-- tacmach.mli | |-- tactypes.ml |-- README.md |-- shell.nix |-- stm | |-- asyncTaskQueue.ml | |-- asyncTaskQueue.mli | |-- coqworkmgrApi.ml | |-- coqworkmgrApi.mli | |-- dag.ml | |-- dag.mli | |-- dune | |-- proofBlockDelimiter.ml | |-- proofBlockDelimiter.mli | |-- spawned.ml | |-- spawned.mli | |-- stm.ml | |-- stm.mli | |-- stm.mllib | |-- tQueue.ml | |-- tQueue.mli | |-- vcs.ml | |-- vcs.mli | |-- vernac_classifier.ml | |-- vernac_classifier.mli | |-- vio_checking.ml | |-- vio_checking.mli | |-- workerPool.ml | |-- workerPool.mli |-- tactics | |-- abstract.ml | |-- abstract.mli | |-- auto.ml | |-- auto.mli | |-- autorewrite.ml | |-- autorewrite.mli | |-- btermdn.ml | |-- btermdn.mli | |-- class_tactics.ml | |-- class_tactics.mli | |-- contradiction.ml | |-- contradiction.mli | |-- declareScheme.ml | |-- declareScheme.mli | |-- declareUctx.ml | |-- declareUctx.mli | |-- dnet.ml | |-- dnet.mli | |-- dn.ml | |-- dn.mli | |-- doc.tex | |-- dune | |-- eauto.ml | |-- eauto.mli | |-- elim.ml | |-- elim.mli | |-- elimschemes.ml | |-- elimschemes.mli | |-- eqdecide.ml | |-- eqdecide.mli | |-- eqschemes.ml | |-- eqschemes.mli | |-- equality.ml | |-- equality.mli | |-- genredexpr.ml | |-- hints.ml | |-- hints.mli | |-- hipattern.ml | |-- hipattern.mli | |-- ind_tables.ml | |-- ind_tables.mli | |-- inv.ml | |-- inv.mli | |-- ppred.ml | |-- ppred.mli | |-- redexpr.ml | |-- redexpr.mli | |-- redops.ml | |-- redops.mli | |-- tacticals.ml | |-- tacticals.mli | |-- tactics.ml | |-- tactics.mli | |-- tactics.mllib | |-- term_dnet.ml | |-- term_dnet.mli |-- test-suite | |-- arithmetic | | |-- primitive.v | |-- bugs | | |-- bug_11140.v | | |-- bug_4690.v | | |-- bug_5996.v | | |-- bug_9490.v | | |-- bug_9532.v | | |-- closed | | | |-- bug_10025.v | | | |-- bug_10026.v | | | |-- bug_10031.v | | | |-- bug_10060.v | | | |-- bug_10088.v | | | |-- bug_10097.v | | | |-- bug_10116.v | | | |-- bug_10161.v | | | |-- bug_10176.v | | | |-- bug_10189.v | | | |-- bug_10196.v | | | |-- bug_10197.v | | | |-- bug_10225.v | | | |-- bug_10264.v | | | |-- bug_10298.v | | | |-- bug_10300.v | | | |-- bug_10504.v | | | |-- bug_10533.v | | | |-- bug_10560.v | | | |-- bug_10669.v | | | |-- bug_10757.v | | | |-- bug_10762.v | | | |-- bug_10778.v | | | |-- bug_10812.v | | | |-- bug_10888.v | | | |-- bug_10894.v | | | |-- bug_10903.v | | | |-- bug_10904.v | | | |-- bug_10917.v | | | |-- bug_11039.v | | | |-- bug_11046.v | | | |-- bug_11048.v | | | |-- bug_11114.v | | | |-- bug_11121.v | | | |-- bug_11133.v | | | |-- bug_11161.v | | | |-- bug_11168.v | | | |-- bug_11321.v | | | |-- bug_11342.v | | | |-- bug_11360.v | | | |-- bug_11421.v | | | |-- bug_11515.v | | | |-- bug_11549.v | | | |-- bug_11552.v | | | |-- bug_11553.v | | | |-- bug_11585.v | | | |-- bug_11722.v | | | |-- bug_11727.v | | | |-- bug_11730.v | | | |-- bug_11783.v | | | |-- bug_11811.v | | | |-- bug_11845.v | | | |-- bug_11846.v | | | |-- bug_11890.v | | | |-- bug_11935.v | | | |-- bug_11941.v | | | |-- bug_12045.v | | | |-- bug_12196.v | | | |-- bug_12228.v | | | |-- bug_12233.v | | | |-- bug_12234.v | | | |-- bug_12257.v | | | |-- bug_12365.v | | | |-- bug_1238.v | | | |-- bug_12390.v | | | |-- bug_12418.v | | | |-- bug_1243.v | | | |-- bug_12483.v | | | |-- bug_12529.v | | | |-- bug_12534.v | | | |-- bug_12551.v | | | |-- bug_12571.v | | | |-- bug_12649.v | | | |-- bug_12651.v | | | |-- bug_1302.v | | | |-- bug_1322.v | | | |-- bug_1341.v | | | |-- bug_1362.v | | | |-- bug_1411.v | | | |-- bug_1414.v | | | |-- bug_1416.v | | | |-- bug_1419.v | | | |-- bug_1425.v | | | |-- bug_1446.v | | | |-- bug_1448.v | | | |-- bug_1477.v | | | |-- bug_1483.v | | | |-- bug_1501.v | | | |-- bug_1507.v | | | |-- bug_1519.v | | | |-- bug_1542.v | | | |-- bug_1543.v | | | |-- bug_1545.v | | | |-- bug_1547.v | | | |-- bug_1551.v | | | |-- bug_1568.v | | | |-- bug_1576.v | | | |-- bug_1582.v | | | |-- bug_1584.v | | | |-- bug_1604.v | | | |-- bug_1614.v | | | |-- bug_1618.v | | | |-- bug_1634.v | | | |-- bug_1643.v | | | |-- bug_1680.v | | | |-- bug_1683.v | | | |-- bug_1696.v | | | |-- bug_1703.v | | | |-- bug_1704.v | | | |-- bug_1711.v | | | |-- bug_1718.v | | | |-- bug_1738.v | | | |-- bug_1740.v | | | |-- bug_1754.v | | | |-- bug_1773.v | | | |-- bug_1774.v | | | |-- bug_1775.v | | | |-- bug_1776.v | | | |-- bug_1779.v | | | |-- bug_1780.v | | | |-- bug_1784.v | | | |-- bug_1787.v | | | |-- bug_1791.v | | | |-- bug_1834.v | | | |-- bug_1844.v | | | |-- bug_1850.v | | | |-- bug_1859.v | | | |-- bug_1865.v | | | |-- bug_1891.v | | | |-- bug_1898.v | | | |-- bug_1900.v | | | |-- bug_1901.v | | | |-- bug_1905.v | | | |-- bug_1907.v | | | |-- bug_1912.v | | | |-- bug_1915.v | | | |-- bug_1918.v | | | |-- bug_1925.v | | | |-- bug_1931.v | | | |-- bug_1935.v | | | |-- bug_1939.v | | | |-- bug_1944.v | | | |-- bug_1951.v | | | |-- bug_1962.v | | | |-- bug_1963.v | | | |-- bug_1977.v | | | |-- bug_1981.v | | | |-- bug_2001.v | | | |-- bug_2006.v | | | |-- bug_2016.v | | | |-- bug_2017.v | | | |-- bug_2021.v | | | |-- bug_2027.v | | | |-- bug_2083.v | | | |-- bug_2089.v | | | |-- bug_2095.v | | | |-- bug_2105.v | | | |-- bug_2108.v | | | |-- bug_2117.v | | | |-- bug_2123.v | | | |-- bug_2127.v | | | |-- bug_2135.v | | | |-- bug_2136.v | | | |-- bug_2137.v | | | |-- bug_2139.v | | | |-- bug_2141.v | | | |-- bug_2145.v | | | |-- bug_2149.v | | | |-- bug_2164.v | | | |-- bug_2181.v | | | |-- bug_2193.v | | | |-- bug_2230.v | | | |-- bug_2231.v | | | |-- bug_2243.v | | | |-- bug_2244.v | | | |-- bug_2245.v | | | |-- bug_2250.v | | | |-- bug_2251.v | | | |-- bug_2255.v | | | |-- bug_2262.v | | | |-- bug_2281.v | | | |-- bug_2295.v | | | |-- bug_2299.v | | | |-- bug_2300.v | | | |-- bug_2303.v | | | |-- bug_2304.v | | | |-- bug_2307.v | | | |-- bug_2310.v | | | |-- bug_2319.v | | | |-- bug_2320.v | | | |-- bug_2342.v | | | |-- bug_2347.v | | | |-- bug_2350.v | | | |-- bug_2353.v | | | |-- bug_2360.v | | | |-- bug_2362.v | | | |-- bug_2375.v | | | |-- bug_2378.v | | | |-- bug_2388.v | | | |-- bug_2393.v | | | |-- bug_2404.v | | | |-- bug_2406.v | | | |-- bug_2417.v | | | |-- bug_2428.v | | | |-- bug_2447.v | | | |-- bug_2456.v | | | |-- bug_2464.v | | | |-- bug_2467.v | | | |-- bug_2473.v | | | |-- bug_2584.v | | | |-- bug_2586.v | | | |-- bug_2590.v | | | |-- bug_2602.v | | | |-- bug_2603.v | | | |-- bug_2608.v | | | |-- bug_2613.v | | | |-- bug_2615.v | | | |-- bug_2616.v | | | |-- bug_2629.v | | | |-- bug_2667.v | | | |-- bug_2668.v | | | |-- bug_2670.v | | | |-- bug_2680.v | | | |-- bug_2713.v | | | |-- bug_2729.v | | | |-- bug_2732.v | | | |-- bug_2733.v | | | |-- bug_2734.v | | | |-- bug_2750.v | | | |-- bug_2775.v | | | |-- bug_2800.v | | | |-- bug_2810.v | | | |-- bug_2814.v | | | |-- bug_2817.v | | | |-- bug_2818.v | | | |-- bug_2828.v | | | |-- bug_2830.v | | | |-- bug_2834.v | | | |-- bug_2836.v | | | |-- bug_2837.v | | | |-- bug_2839.v | | | |-- bug_2846.v | | | |-- bug_2848.v | | | |-- bug_2854.v | | | |-- bug_2876.v | | | |-- bug_2881.v | | | |-- bug_2883.v | | | |-- bug_2900.v | | | |-- bug_2920.v | | | |-- bug_2923.v | | | |-- bug_2928.v | | | |-- bug_2930.v | | | |-- bug_2945.v | | | |-- bug_2946.v | | | |-- bug_2951.v | | | |-- bug_2955.v | | | |-- bug_2966.v | | | |-- bug_2969.v | | | |-- bug_2981.v | | | |-- bug_2983.v | | | |-- bug_2990.v | | | |-- bug_2994.v | | | |-- bug_2995.v | | | |-- bug_2996.v | | | |-- bug_3000.v | | | |-- bug_3001.v | | | |-- bug_3003.v | | | |-- bug_3004.v | | | |-- bug_3008.v | | | |-- bug_3010b.v | | | |-- bug_3016.v | | | |-- bug_3017.v | | | |-- bug_3022.v | | | |-- bug_3023.v | | | |-- bug_3036.v | | | |-- bug_3037.v | | | |-- bug_3043.v | | | |-- bug_3045.v | | | |-- bug_3050.v | | | |-- bug_3054.v | | | |-- bug_3062.v | | | |-- bug_3068.v | | | |-- bug_3070.v | | | |-- bug_3071.v | | | |-- bug_3080.v | | | |-- bug_3088.v | | | |-- bug_3093.v | | | |-- bug_3100.v | | | |-- bug_3125.v | | | |-- bug_3142.v | | | |-- bug_3164.v | | | |-- bug_3188.v | | | |-- bug_3199.v | | | |-- bug_3205.v | | | |-- bug_3209.v | | | |-- bug_3210.v | | | |-- bug_3212.v | | | |-- bug_3217.v | | | |-- bug_3228.v | | | |-- bug_3230.v | | | |-- bug_3242.v | | | |-- bug_3249.v | | | |-- bug_3251.v | | | |-- bug_3257.v | | | |-- bug_3258.v | | | |-- bug_3259.v | | | |-- bug_3260.v | | | |-- bug_3262.v | | | |-- bug_3264.v | | | |-- bug_3265.v | | | |-- bug_3266.v | | | |-- bug_3267.v | | | |-- bug_3281.v | | | |-- bug_3282.v | | | |-- bug_3284.v | | | |-- bug_3285.v | | | |-- bug_3286.v | | | |-- bug_3287.v | | | |-- bug_3289.v | | | |-- bug_3291.v | | | |-- bug_3294.v | | | |-- bug_3297.v | | | |-- bug_3298.v | | | |-- bug_3300.v | | | |-- bug_3305.v | | | |-- bug_3306.v | | | |-- bug_3310.v | | | |-- bug_3314.v | | | |-- bug_3315.v | | | |-- bug_3317.v | | | |-- bug_3319.v | | | |-- bug_3320.v | | | |-- bug_3321.v | | | |-- bug_3322.v | | | |-- bug_3323.v | | | |-- bug_3324.v | | | |-- bug_3325.v | | | |-- bug_3326.v | | | |-- bug_3329.v | | | |-- bug_3330.v | | | |-- bug_3331.v | | | |-- bug_3332.v | | | |-- bug_3336.v | | | |-- bug_3337.v | | | |-- bug_3338.v | | | |-- bug_3344.v | | | |-- bug_3346.v | | | |-- bug_3347.v | | | |-- bug_3348.v | | | |-- bug_3350.v | | | |-- bug_3352.v | | | |-- bug_3354.v | | | |-- bug_3355.v | | | |-- bug_3368.v | | | |-- bug_3372.v | | | |-- bug_3373.v | | | |-- bug_3374.v | | | |-- bug_3375.v | | | |-- bug_3377.v | | | |-- bug_3382.v | | | |-- bug_3383.v | | | |-- bug_3386.v | | | |-- bug_3387.v | | | |-- bug_3388.v | | | |-- bug_3390.v | | | |-- bug_3392.v | | | |-- bug_3393.v | | | |-- bug_3402.v | | | |-- bug_3408.v | | | |-- bug_3416.v | | | |-- bug_3417.v | | | |-- bug_3422.v | | | |-- bug_3427.v | | | |-- bug_3428.v | | | |-- bug_3439.v | | | |-- bug_3446.v | | | |-- bug_3453.v | | | |-- bug_3454.v | | | |-- bug_3461.v | | | |-- bug_3467.v | | | |-- bug_3468.v | | | |-- bug_3469.v | | | |-- bug_3477.v | | | |-- bug_3480.v | | | |-- bug_3481.v | | | |-- bug_3482.v | | | |-- bug_3483.v | | | |-- bug_3484.v | | | |-- bug_3485.v | | | |-- bug_3487.v | | | |-- bug_3490.v | | | |-- bug_3491.v | | | |-- bug_3495.v | | | |-- bug_3505.v | | | |-- bug_3509.v | | | |-- bug_3510.v | | | |-- bug_3513.v | | | |-- bug_3520.v | | | |-- bug_3531.v | | | |-- bug_3537.v | | | |-- bug_3539.v | | | |-- bug_3542.v | | | |-- bug_3546.v | | | |-- bug_3554.v | | | |-- bug_3559.v | | | |-- bug_3560.v | | | |-- bug_3561.v | | | |-- bug_3562.v | | | |-- bug_3563.v | | | |-- bug_3566.v | | | |-- bug_3567.v | | | |-- bug_3584.v | | | |-- bug_3590.v | | | |-- bug_3593.v | | | |-- bug_3594.v | | | |-- bug_3596.v | | | |-- bug_3612.v | | | |-- bug_3616.v | | | |-- bug_3618.v | | | |-- bug_3623.v | | | |-- bug_3624.v | | | |-- bug_3625.v | | | |-- bug_3628.v | | | |-- bug_3633.v | | | |-- bug_3637.v | | | |-- bug_3638.v | | | |-- bug_3640.v | | | |-- bug_3641.v | | | |-- bug_3647.v | | | |-- bug_3648.v | | | |-- bug_3649.v | | | |-- bug_3652.v | | | |-- bug_3653.v | | | |-- bug_3654.v | | | |-- bug_3656.v | | | |-- bug_3657.v | | | |-- bug_3658.v | | | |-- bug_3660.v | | | |-- bug_3661.v | | | |-- bug_3662.v | | | |-- bug_3664.v | | | |-- bug_3665.v | | | |-- bug_3666.v | | | |-- bug_3667.v | | | |-- bug_3668.v | | | |-- bug_3670.v | | | |-- bug_3672.v | | | |-- bug_3675.v | | | |-- bug_3681.v | | | |-- bug_3682.v | | | |-- bug_3684.v | | | |-- bug_3685.v | | | |-- bug_3686.v | | | |-- bug_3690.v | | | |-- bug_3692.v | | | |-- bug_3698.v | | | |-- bug_3699.v | | | |-- bug_3700.v | | | |-- bug_3703.v | | | |-- bug_3709.v | | | |-- bug_3710.v | | | |-- bug_3723.v | | | |-- bug_3732.v | | | |-- bug_3735.v | | | |-- bug_3736.v | | | |-- bug_3743.v | | | |-- bug_3746.v | | | |-- bug_3753.v | | | |-- bug_3754.v | | | |-- bug_3755.v | | | |-- bug_3777.v | | | |-- bug_3779.v | | | |-- bug_3782.v | | | |-- bug_3783.v | | | |-- bug_3786.v | | | |-- bug_3788.v | | | |-- bug_3792.v | | | |-- bug_3798.v | | | |-- bug_3804.v | | | |-- bug_3807.v | | | |-- bug_3808.v | | | |-- bug_3810.v | | | |-- bug_3815.v | | | |-- bug_3819.v | | | |-- bug_3821.v | | | |-- bug_3825.v | | | |-- bug_3828.v | | | |-- bug_3848.v | | | |-- bug_3849.v | | | |-- bug_3854.v | | | |-- bug_3881.v | | | |-- bug_3886.v | | | |-- bug_3890.v | | | |-- bug_3892.v | | | |-- bug_3895.v | | | |-- bug_3896.v | | | |-- bug_3899.v | | | |-- bug_3900.v | | | |-- bug_3911.v | | | |-- bug_3916.v | | | |-- bug_3920.v | | | |-- bug_3922.v | | | |-- bug_3923.v | | | |-- bug_3929.v | | | |-- bug_3938.v | | | |-- bug_3943.v | | | |-- bug_3944.v | | | |-- bug_3948.v | | | |-- bug_3953.v | | | |-- bug_3956.v | | | |-- bug_3957.v | | | |-- bug_3960.v | | | |-- bug_3974.v | | | |-- bug_3975.v | | | |-- bug_3978.v | | | |-- bug_3993.v | | | |-- bug_3998.v | | | |-- bug_4001.v | | | |-- bug_4012.v | | | |-- bug_4016.v | | | |-- bug_4017.v | | | |-- bug_4018.v | | | |-- bug_4031.v | | | |-- bug_4034.v | | | |-- bug_4035.v | | | |-- bug_4046.v | | | |-- bug_4057.v | | | |-- bug_4069.v | | | |-- bug_4078.v | | | |-- bug_4089.v | | | |-- bug_4095.v | | | |-- bug_4097.v | | | |-- bug_4101.v | | | |-- bug_4103.v | | | |-- bug_4116.v | | | |-- bug_4120.v | | | |-- bug_4121.v | | | |-- bug_4132.v | | | |-- bug_4149.v | | | |-- bug_4151.v | | | |-- bug_4157.v | | | |-- bug_4161.v | | | |-- bug_4165.v | | | |-- bug_4187.v | | | |-- bug_4190.v | | | |-- bug_4191.v | | | |-- bug_4193.v | | | |-- bug_4198.v | | | |-- bug_4202.v | | | |-- bug_4203.v | | | |-- bug_4205.v | | | |-- bug_4214.v | | | |-- bug_4216.v | | | |-- bug_4217.v | | | |-- bug_4221.v | | | |-- bug_4232.v | | | |-- bug_4234.v | | | |-- bug_4240.v | | | |-- bug_4250.v | | | |-- bug_4251.v | | | |-- bug_4254.v | | | |-- bug_4256.v | | | |-- bug_4272.v | | | |-- bug_4273.v | | | |-- bug_4276.v | | | |-- bug_4280.v | | | |-- bug_4283.v | | | |-- bug_4284.v | | | |-- bug_4287.v | | | |-- bug_4292.v | | | |-- bug_4293.v | | | |-- bug_4294.v | | | |-- bug_4298.v | | | |-- bug_4299.v | | | |-- bug_4301.v | | | |-- bug_4305.v | | | |-- bug_4306.v | | | |-- bug_4316.v | | | |-- bug_4318.v | | | |-- bug_4325.v | | | |-- bug_4328.v | | | |-- bug_4346.v | | | |-- bug_4347.v | | | |-- bug_4354.v | | | |-- bug_4363.v | | | |-- bug_4372.v | | | |-- bug_4375.v | | | |-- bug_4378.v | | | |-- bug_4390.v | | | |-- bug_4397.v | | | |-- bug_4403.v | | | |-- bug_4404.v | | | |-- bug_4412.v | | | |-- bug_4416.v | | | |-- bug_4420.v | | | |-- bug_4433.v | | | |-- bug_4443.v | | | |-- bug_4450.v | | | |-- bug_4453.v | | | |-- bug_4456.v | | | |-- bug_4462.v | | | |-- bug_4464.v | | | |-- bug_4467.v | | | |-- bug_4471.v | | | |-- bug_4479.v | | | |-- bug_4480.v | | | |-- bug_4484.v | | | |-- bug_4495.v | | | |-- bug_4498.v | | | |-- bug_4502.v | | | |-- bug_4503.v | | | |-- bug_4509.v | | | |-- bug_4511.v | | | |-- bug_4519.v | | | |-- bug_4527.v | | | |-- bug_4529.v | | | |-- bug_4533.v | | | |-- bug_4538.v | | | |-- bug_4544.v | | | |-- bug_4574.v | | | |-- bug_4576.v | | | |-- bug_4580.v | | | |-- bug_4582.v | | | |-- bug_4588.v | | | |-- bug_4596.v | | | |-- bug_4603.v | | | |-- bug_4612.v | | | |-- bug_4616.v | | | |-- bug_4622.v | | | |-- bug_4623.v | | | |-- bug_4624.v | | | |-- bug_4627.v | | | |-- bug_4628.v | | | |-- bug_4634.v | | | |-- bug_4638.v | | | |-- bug_4644.v | | | |-- bug_4653.v | | | |-- bug_4661.v | | | |-- bug_4663.v | | | |-- bug_4670.v | | | |-- bug_4673.v | | | |-- bug_4679.v | | | |-- bug_4684.v | | | |-- bug_4695.v | | | |-- bug_4708.v | | | |-- bug_4709.v | | | |-- bug_4710.v | | | |-- bug_4713.v | | | |-- bug_4717.v | | | |-- bug_4718.v | | | |-- bug_4720.v | | | |-- bug_4723.v | | | |-- bug_4725.v | | | |-- bug_4726.v | | | |-- bug_4737.v | | | |-- bug_4745.v | | | |-- bug_4746.v | | | |-- bug_4754.v | | | |-- bug_4762.v | | | |-- bug_4763.v | | | |-- bug_4764.v | | | |-- bug_4769.v | | | |-- bug_4771.v | | | |-- bug_4772.v | | | |-- bug_4780.v | | | |-- bug_4781.v | | | |-- bug_4782.v | | | |-- bug_4785.v | | | |-- bug_4787.v | | | |-- bug_4813.v | | | |-- bug_4816.v | | | |-- bug_4818.v | | | |-- bug_4836 | | | | |-- PLACEHOLDER | | | |-- bug_4836.v | | | |-- bug_4844.v | | | |-- bug_4852.v | | | |-- bug_4858.v | | | |-- bug_4859.v | | | |-- bug_4863.v | | | |-- bug_4865.v | | | |-- bug_4869.v | | | |-- bug_4873.v | | | |-- bug_4877.v | | | |-- bug_4880.v | | | |-- bug_4893.v | | | |-- bug_4904.v | | | |-- bug_4925.v | | | |-- bug_4932.v | | | |-- bug_4955.v | | | |-- bug_4957.v | | | |-- bug_4966.v | | | |-- bug_4969.v | | | |-- bug_4970.v | | | |-- bug_5011.v | | | |-- bug_5012.v | | | |-- bug_5019.v | | | |-- bug_5036.v | | | |-- bug_5043.v | | | |-- bug_5045.v | | | |-- bug_5065.v | | | |-- bug_5066.v | | | |-- bug_5077.v | | | |-- bug_5078.v | | | |-- bug_5093.v | | | |-- bug_5095.v | | | |-- bug_5096.v | | | |-- bug_5097.v | | | |-- bug_5123.v | | | |-- bug_5127.v | | | |-- bug_5145.v | | | |-- bug_5149.v | | | |-- bug_5153.v | | | |-- bug_5159.v | | | |-- bug_5161.v | | | |-- bug_5177.v | | | |-- bug_5180.v | | | |-- bug_5181.v | | | |-- bug_5188.v | | | |-- bug_5193.v | | | |-- bug_5197.v | | | |-- bug_5198.v | | | |-- bug_5203.v | | | |-- bug_5205.v | | | |-- bug_5208.v | | | |-- bug_5215_2.v | | | |-- bug_5215.v | | | |-- bug_5219.v | | | |-- bug_5233.v | | | |-- bug_5245.v | | | |-- bug_5255.v | | | |-- bug_5277.v | | | |-- bug_5281.v | | | |-- bug_5286.v | | | |-- bug_5300.v | | | |-- bug_5315.v | | | |-- bug_5321.v | | | |-- bug_5322.v | | | |-- bug_5323.v | | | |-- bug_5331.v | | | |-- bug_5345.v | | | |-- bug_5346.v | | | |-- bug_5347.v | | | |-- bug_5359.v | | | |-- bug_5365.v | | | |-- bug_5368.v | | | |-- bug_5372.v | | | |-- bug_5377.v | | | |-- bug_5401.v | | | |-- bug_5414.v | | | |-- bug_5434.v | | | |-- bug_5435.v | | | |-- bug_5445.v | | | |-- bug_5449.v | | | |-- bug_5460.v | | | |-- bug_5470.v | | | |-- bug_5476.v | | | |-- bug_5486.v | | | |-- bug_5487.v | | | |-- bug_5500.v | | | |-- bug_5501.v | | | |-- bug_5522.v | | | |-- bug_5523.v | | | |-- bug_5526.v | | | |-- bug_5532.v | | | |-- bug_5539.v | | | |-- bug_5547.v | | | |-- bug_5550.v | | | |-- bug_5578.v | | | |-- bug_5598.v | | | |-- bug_5608.v | | | |-- bug_5617.v | | | |-- bug_5618.v | | | |-- bug_5641.v | | | |-- bug_5666.v | | | |-- bug_5671.v | | | |-- bug_5683.v | | | |-- bug_5692.v | | | |-- bug_5696.v | | | |-- bug_5697.v | | | |-- bug_5707.v | | | |-- bug_5713.v | | | |-- bug_5717.v | | | |-- bug_5719.v | | | |-- bug_5726.v | | | |-- bug_5741.v | | | |-- bug_5749.v | | | |-- bug_5750.v | | | |-- bug_5752.v | | | |-- bug_5755.v | | | |-- bug_5757.v | | | |-- bug_5761.v | | | |-- bug_5762.v | | | |-- bug_5764.v | | | |-- bug_5765.v | | | |-- bug_5769.v | | | |-- bug_5786.v | | | |-- bug_5790.v | | | |-- bug_5797.v | | | |-- bug_5845.v | | | |-- bug_5940.v | | | |-- bug_6070.v | | | |-- bug_6129.v | | | |-- bug_6165.v | | | |-- bug_6191.v | | | |-- bug_6202.v | | | |-- bug_6297.v | | | |-- bug_6313.v | | | |-- bug_6323.v | | | |-- bug_6378.v | | | |-- bug_6384.v | | | |-- bug_6385.v | | | |-- bug_6490.v | | | |-- bug_6529.v | | | |-- bug_6534.v | | | |-- bug_6617.v | | | |-- bug_6631.v | | | |-- bug_6634.v | | | |-- bug_6661.v | | | |-- bug_6677.v | | | |-- bug_6770.v | | | |-- bug_6774.v | | | |-- bug_6775.v | | | |-- bug_6878.v | | | |-- bug_6910.v | | | |-- bug_6951.v | | | |-- bug_6956.v | | | |-- bug_7011.v | | | |-- bug_7068.v | | | |-- bug_7076.v | | | |-- bug_7092.v | | | |-- bug_7113.v | | | |-- bug_7195.v | | | |-- bug_7333.v | | | |-- bug_7392.v | | | |-- bug_7421.v | | | |-- bug_7462.v | | | |-- bug_7554.v | | | |-- bug_7615.v | | | |-- bug_7631.v | | | |-- bug_7695.v | | | |-- bug_7700.v | | | |-- bug_7712.v | | | |-- bug_7723.v | | | |-- bug_7754.v | | | |-- bug_7779.v | | | |-- bug_7780.v | | | |-- bug_7795.v | | | |-- bug_7811.v | | | |-- bug_7812.v | | | |-- bug_7854.v | | | |-- bug_7867.v | | | |-- bug_7900.v | | | |-- bug_7903.v | | | |-- bug_7904.v | | | |-- bug_7967.v | | | |-- bug_8004.v | | | |-- bug_8076.v | | | |-- bug_8081.v | | | |-- bug_808_2411.v | | | |-- bug_8106.v | | | |-- bug_8119.v | | | |-- bug_8121.v | | | |-- bug_8126.v | | | |-- bug_8215.v | | | |-- bug_8224.v | | | |-- bug_8270.v | | | |-- bug_8288.v | | | |-- bug_8364.v | | | |-- bug_8369.v | | | |-- bug_8432.v | | | |-- bug_8459.v | | | |-- bug_8478.v | | | |-- bug_8532.v | | | |-- bug_8544.v | | | |-- bug_8553.v | | | |-- bug_8672.v | | | |-- bug_8725.v | | | |-- bug_8755.v | | | |-- bug_8785.v | | | |-- bug_8791.v | | | |-- bug_8794.v | | | |-- bug_8819.v | | | |-- bug_8848.v | | | |-- bug_8885.v | | | |-- bug_8908.v | | | |-- bug_8951.v | | | |-- bug_9014.v | | | |-- bug_9058.v | | | |-- bug_9114.v | | | |-- bug_9166.v | | | |-- bug_9229.v | | | |-- bug_9240.v | | | |-- bug_9268.v | | | |-- bug_9294.v | | | |-- bug_9300.v | | | |-- bug_9313.v | | | |-- bug_9329.v | | | |-- bug_9344.v | | | |-- bug_9348.v | | | |-- bug_9363.v | | | |-- bug_9367.v | | | |-- bug_9375.v | | | |-- bug_9432.v | | | |-- bug_9451.v | | | |-- bug_9453.v | | | |-- bug_9494.v | | | |-- bug_9508.v | | | |-- bug_9512.v | | | |-- bug_9517.v | | | |-- bug_9521.v | | | |-- bug_9526.v | | | |-- bug_9527.v | | | |-- bug_9583.v | | | |-- bug_9595.v | | | |-- bug_9598.v | | | |-- bug_9631.v | | | |-- bug_9640.v | | | |-- bug_9652.v | | | |-- bug_9663.v | | | |-- bug_9679.v | | | |-- bug_9684.v | | | |-- bug_9741.v | | | |-- bug_9851.v | | | |-- bug_9930.v | | | |-- bug_sprop_13.v | | | |-- bug_sprop_14.v | | | |-- HoTT_coq_001.v | | | |-- HoTT_coq_002.v | | | |-- HoTT_coq_006.v | | | |-- HoTT_coq_007.v | | | |-- HoTT_coq_010.v | | | |-- HoTT_coq_012.v | | | |-- HoTT_coq_013.v | | | |-- HoTT_coq_014.v | | | |-- HoTT_coq_016.v | | | |-- HoTT_coq_020.v | | | |-- HoTT_coq_023.v | | | |-- HoTT_coq_025.v | | | |-- HoTT_coq_027.v | | | |-- HoTT_coq_028.v | | | |-- HoTT_coq_029.v | | | |-- HoTT_coq_030.v | | | |-- HoTT_coq_032.v | | | |-- HoTT_coq_034.v | | | |-- HoTT_coq_035.v | | | |-- HoTT_coq_036.v | | | |-- HoTT_coq_037.v | | | |-- HoTT_coq_041.v | | | |-- HoTT_coq_042.v | | | |-- HoTT_coq_043.v | | | |-- HoTT_coq_044.v | | | |-- HoTT_coq_045.v | | | |-- HoTT_coq_047.v | | | |-- HoTT_coq_048.v | | | |-- HoTT_coq_049.v | | | |-- HoTT_coq_050.v | | | |-- HoTT_coq_052.v | | | |-- HoTT_coq_053.v | | | |-- HoTT_coq_054.v | | | |-- HoTT_coq_055.v | | | |-- HoTT_coq_056.v | | | |-- HoTT_coq_057.v | | | |-- HoTT_coq_058.v | | | |-- HoTT_coq_059.v | | | |-- HoTT_coq_061.v | | | |-- HoTT_coq_062.v | | | |-- HoTT_coq_063.v | | | |-- HoTT_coq_064.v | | | |-- HoTT_coq_067.v | | | |-- HoTT_coq_068.v | | | |-- HoTT_coq_071.v | | | |-- HoTT_coq_074.v | | | |-- HoTT_coq_077.v | | | |-- HoTT_coq_078.v | | | |-- HoTT_coq_079.v | | | |-- HoTT_coq_080.v | | | |-- HoTT_coq_081.v | | | |-- HoTT_coq_082.v | | | |-- HoTT_coq_083.v | | | |-- HoTT_coq_084.v | | | |-- HoTT_coq_085.v | | | |-- HoTT_coq_087.v | | | |-- HoTT_coq_088.v | | | |-- HoTT_coq_089.v | | | |-- HoTT_coq_090.v | | | |-- HoTT_coq_091.v | | | |-- HoTT_coq_093.v | | | |-- HoTT_coq_094.v | | | |-- HoTT_coq_097.v | | | |-- HoTT_coq_098.v | | | |-- HoTT_coq_099.v | | | |-- HoTT_coq_100.v | | | |-- HoTT_coq_101.v | | | |-- HoTT_coq_102.v | | | |-- HoTT_coq_103.v | | | |-- HoTT_coq_104.v | | | |-- HoTT_coq_105.v | | | |-- HoTT_coq_107.v | | | |-- HoTT_coq_108.v | | | |-- HoTT_coq_110.v | | | |-- HoTT_coq_111.v | | | |-- HoTT_coq_112.v | | | |-- HoTT_coq_113.v | | | |-- HoTT_coq_114.v | | | |-- HoTT_coq_115.v | | | |-- HoTT_coq_116.v | | | |-- HoTT_coq_117.v | | | |-- HoTT_coq_118.v | | | |-- HoTT_coq_120.v | | | |-- HoTT_coq_121.v | | | |-- HoTT_coq_122.v | | | |-- HoTT_coq_123.v | | | |-- HoTT_coq_124.v | | | |-- PLACEHOLDER.v | | |-- opened | | |-- 2652a.v-disabled | | |-- 2652b.v-disabled | | |-- bug_1338.v-disabled | | |-- bug_1596.v | | |-- bug_1615.v | | |-- bug_1671.v | | |-- bug_1811.v | | |-- bug_2572.v-disabled | | |-- bug_3010.v-disabled | | |-- bug_3092.v | | |-- bug_3166.v | | |-- bug_3186.v-disabled | | |-- bug_3248.v | | |-- bug_3277.v | | |-- bug_3278.v | | |-- bug_3283.v | | |-- bug_3295.v | | |-- bug_3304.v | | |-- bug_3311.v | | |-- bug_3312.v | | |-- bug_3343.v | | |-- bug_3345.v | | |-- bug_3357.v | | |-- bug_3363.v | | |-- bug_3370.v | | |-- bug_3395.v | | |-- bug_3424.v | | |-- bug_3459.v | | |-- bug_3463.v | | |-- bug_3478.v-disabled | | |-- bug_3626.v | | |-- bug_3655.v | | |-- bug_3794.v | | |-- bug_3889.v | | |-- bug_3919.v-disabled | | |-- bug_3922.v-disabled | | |-- bug_3928.v-disabled | | |-- bug_3938.v | | |-- bug_3946.v | | |-- bug_4701.v | | |-- bug_4721.v | | |-- bug_4728.v | | |-- bug_4755.v | | |-- bug_4771.v | | |-- bug_4778.v | | |-- bug_4813.v | | |-- bug_6393.v | | |-- bug_6602.v | | |-- HoTT_coq_106.v | |-- complexity | | |-- bug4076bis.v | | |-- bug4076.v | | |-- ConstructiveCauchyRealsPerformance.v | | |-- constructor.v | | |-- evar_instance.v | | |-- f_equal.v | | |-- guard.v | | |-- injection.v | | |-- lettuple.v | | |-- Notations.v | | |-- patternmatching.v | | |-- pattern.v | | |-- pretyping.v | | |-- ring2.v | | |-- ring.v | | |-- setoid_rewrite.v | | |-- unification.v | |-- coqchk | | |-- bug_7539.v | | |-- bug_8655.v | | |-- bug_8876.v | | |-- bug_8881.v | | |-- bug_8937.v | | |-- cumulativity.v | | |-- include_primproj.v | | |-- include.v | | |-- inductive_functor_params.v | | |-- inductive_functor_squash.v | | |-- inductive_functor_template.v | | |-- primproj2.v | | |-- primproj.v | | |-- univ.v | |-- coqdoc | | |-- binder.html.out | | |-- binder.tex.out | | |-- binder.v | | |-- bug11194.html.out | | |-- bug11194.tex.out | | |-- bug11194.v | | |-- bug11353.html.out | | |-- bug11353.tex.out | | |-- bug11353.v | | |-- bug12742.html.out | | |-- bug12742.tex.out | | |-- bug12742.v | | |-- bug5648.html.out | | |-- bug5648.tex.out | | |-- bug5648.v | | |-- bug5700.html.out | | |-- bug5700.tex.out | | |-- bug5700.v | | |-- links.html.out | | |-- links.tex.out | | |-- links.v | | |-- Record.html.out | | |-- Record.tex.out | | |-- Record.v | |-- coq-makefile | | |-- arg | | | |-- _CoqProject | | | |-- run.sh | | |-- camldep | | | |-- _CoqProject | | | |-- run.sh | | |-- compat-subdirs | | | |-- _CoqProject | | | |-- run.sh | | | |-- subdir | | | |-- Makefile | | |-- coqdoc1 | | | |-- _CoqProject | | | |-- run.sh | | |-- coqdoc2 | | | |-- _CoqProject | | | |-- run.sh | | |-- emptyprefix | | | |-- _CoqProject | | | |-- _CoqProject.sub | | | |-- run.sh | | |-- extend-subdirs | | | |-- _CoqProject | | | |-- Makefile.local | | | |-- run.sh | | | |-- subdir | | | |-- Makefile | | |-- findlib-package | | | |-- _CoqProject | | | |-- findlib | | | | |-- foo | | | | |-- foolib.ml | | | | |-- foo.mli | | | | |-- Makefile | | | | |-- META | | | |-- Makefile.local | | | |-- run.sh | | |-- findlib-package-unpacked | | | |-- _CoqProject | | | |-- findlib | | | | |-- foo | | | | |-- foolib.ml | | | | |-- foo.mli | | | | |-- Makefile | | | | |-- META | | | |-- Makefile.local | | | |-- run.sh | | |-- latex1 | | | |-- _CoqProject | | | |-- run.sh | | |-- merlin1 | | | |-- _CoqProject | | | |-- run.sh | | |-- missing-install | | | |-- run.sh | | |-- mlpack1 | | | |-- _CoqProject | | | |-- run.sh | | |-- mlpack2 | | | |-- _CoqProject | | | |-- run.sh | | |-- multiroot | | | |-- _CoqProject | | | |-- run.sh | | |-- native1 | | | |-- _CoqProject | | | |-- run.sh | | |-- native2 | | | |-- _CoqProject | | | |-- run.sh | | |-- only | | | |-- _CoqProject | | | |-- run.sh | | |-- plugin1 | | | |-- _CoqProject | | | |-- run.sh | | |-- plugin2 | | | |-- _CoqProject | | | |-- run.sh | | |-- plugin3 | | | |-- _CoqProject | | | |-- run.sh | | |-- quick2vo | | | |-- _CoqProject | | | |-- run.sh | | |-- template | | | |-- init.sh | | | |-- path-init.sh | | | |-- src | | | | |-- test_aux.ml | | | | |-- test_aux.mli | | | | |-- test.mlg | | | | |-- test.mli | | | | |-- test_plugin.mlpack | | | |-- theories | | | |-- sub | | | | |-- testsub.v | | | |-- test.v | | |-- timing | | | |-- after | | | | |-- _CoqProject | | | | |-- Fast.v | | | | |-- Slow.v | | | | |-- time-of-build-after.log.desired | | | | |-- time-of-build-before.log.desired | | | | |-- time-of-build-both.log.desired | | | |-- aggregate | | | | |-- _CoqProject | | | | |-- Fast.v | | | | |-- Slow.v | | | |-- before | | | | |-- _CoqProject | | | | |-- Fast.v | | | | |-- Slow.v | | | |-- error | | | | |-- A.v | | | | |-- _CoqProject | | | |-- per-file-after | | | | |-- A.v | | | | |-- A.v.timing.diff.desired | | | | |-- _CoqProject | | | |-- per-file-before | | | | |-- A.v | | | | |-- _CoqProject | | | |-- precomputed-time-tests | | | | |-- 001-correct-diff-sorting-order | | | | | |-- run.sh | | | | | |-- time-of-build-after.log.in | | | | | |-- time-of-build-before.log.in | | | | | |-- time-of-build-both-real-absolute.log.expected | | | | | |-- time-of-build-both-real-auto.log.expected | | | | | |-- time-of-build-both-real-diff.log.expected | | | | | |-- time-of-build-both-real.log.expected | | | | | |-- time-of-build-both-user-absolute.log.expected | | | | | |-- time-of-build-both-user-auto.log.expected | | | | | |-- time-of-build-both-user-diff.log.expected | | | | | |-- time-of-build-both-user.log.expected | | | | |-- 002-single-file-sorting | | | | | |-- run.sh | | | | | |-- time-of-build.log.in | | | | | |-- time-of-build-pretty-real.log.expected | | | | | |-- time-of-build-pretty-user.log.expected | | | | |-- 003-non-utf8 | | | | | |-- run.sh | | | | | |-- time-of-build.log.in | | | | | |-- time-of-build-pretty.log.expected | | | | |-- 004-per-file-fuzz | | | | | |-- foo_after.v | | | | | |-- foo_before.v | | | | | |-- foo-real.v.timing.diff.expected | | | | | |-- foo-user.v.timing.diff.expected | | | | | |-- foo.v.after-timing.in | | | | | |-- foo.v.before-timing.in | | | | | |-- run.sh | | | | |-- 005-correct-diff-sorting-order-mem | | | | | |-- run.sh | | | | | |-- time-of-build-after.log.in | | | | | |-- time-of-build-before.log.in | | | | | |-- time-of-build-both-real-absolute.log.expected | | | | | |-- time-of-build-both-real-auto.log.expected | | | | | |-- time-of-build-both-real-diff.log.expected | | | | | |-- time-of-build-both-real.log.expected | | | | | |-- time-of-build-both-user-absolute.log.expected | | | | | |-- time-of-build-both-user-auto.log.expected | | | | | |-- time-of-build-both-user-diff.log.expected | | | | | |-- time-of-build-both-user.log.expected | | | | |-- 006-zero-before | | | | | |-- run.sh | | | | | |-- time-of-build-after.log.in | | | | | |-- time-of-build-before.log.in | | | | | |-- time-of-build-both.log.expected | | | | |-- run.sh | | | |-- run.sh | | |-- uninstall1 | | | |-- _CoqProject | | | |-- run.sh | | |-- uninstall2 | | | |-- _CoqProject | | | |-- run.sh | | |-- validate1 | | | |-- _CoqProject | | | |-- run.sh | | |-- vio2vo | | |-- _CoqProject | | |-- run.sh | |-- _CoqProject | |-- coqwc | | |-- BZ5637.out | | |-- BZ5637.v | | |-- BZ5756.out | | |-- BZ5756.v | | |-- false.out | | |-- false.v | | |-- next-obligation.out | | |-- next-obligation.v | | |-- theorem.out | | |-- theorem.v | |-- dune | |-- failure | | |-- autorewritein.v | | |-- Case10.v | | |-- Case11.v | | |-- Case12.v | | |-- Case13.v | | |-- Case14.v | | |-- Case15.v | | |-- Case16.v | | |-- Case1.v | | |-- Case2.v | | |-- Case3.v | | |-- Case4.v | | |-- Case5.v | | |-- Case6.v | | |-- Case7.v | | |-- Case8.v | | |-- Case9.v | | |-- cases.v | | |-- check.v | | |-- circular_subtyping.v | | |-- clash_cons.v | | |-- clashes.v | | |-- ClearBody.v | | |-- cofixpoint.v | | |-- coqbugs0266.v | | |-- evar1.v | | |-- evarclear1.v | | |-- evarclear2.v | | |-- evarlemma.v | | |-- fixpoint1.v | | |-- fixpoint2.v | | |-- fixpoint3.v | | |-- fixpoint4.v | | |-- fixpointeta.v | | |-- guard_cofix.v | | |-- guard.v | | |-- illtype1.v | | |-- ImportedCoercion.v | | |-- inductive.v | | |-- int63.v | | |-- ltac1.v | | |-- ltac2.v | | |-- ltac4.v | | |-- Notations.v | | |-- pattern.v | | |-- positivity.v | | |-- proofirrelevance.v | | |-- prop_set_proof_irrelevance.v | | |-- redef.v | | |-- Reordering.v | | |-- rewrite_in_goal.v | | |-- rewrite_in_hyp2.v | | |-- rewrite_in_hyp.v | | |-- search.v | | |-- Sections.v | | |-- sortelim.v | | |-- subterm2.v | | |-- subterm3.v | | |-- subterm.v | | |-- subtyping2.v | | |-- subtyping.v | | |-- Tauto.v | | |-- Uminus.v | | |-- universes3.v | | |-- universes_buraliforti_redef.v | | |-- universes_buraliforti.v | | |-- universes_sections1.v | | |-- universes_sections2.v | | |-- universes.v | | |-- univ_include.v | |-- ide | | |-- blocking-futures.fake | | |-- bug4246.fake | | |-- bug4249.fake | | |-- bug7088.fake | | |-- debug_ltac.fake | | |-- join.fake | | |-- join-sync.fake | | |-- load.fake | | |-- reopen1.fake | | |-- reopen.fake | | |-- undo001.fake | | |-- undo002.fake | | |-- undo003.fake | | |-- undo004.fake | | |-- undo005.fake | | |-- undo006.fake | | |-- undo008.fake | | |-- undo009.fake | | |-- undo010.fake | | |-- undo012.fake | | |-- undo013.fake | | |-- undo014.fake | | |-- undo015.fake | | |-- undo016.fake | | |-- undo017.fake | | |-- undo018.fake | | |-- undo019.fake | | |-- undo020.fake | | |-- undo021.fake | | |-- undo022.fake | | |-- univ.fake | |-- ideal-features | | |-- Apply.v | | |-- Case4.v | | |-- Case9.v | | |-- complexity | | | |-- evars_subst.v | | |-- eapply_evar.v | | |-- evars_subst.v | | |-- implicit_binders.v | | |-- universes.v | |-- interactive | | |-- Back.v | | |-- bug_4289.v | | |-- Evar.v | | |-- ParalITP_smallproofs.v | | |-- ParalITP.v | | |-- PrimNotation.v | | |-- proof_block.v | |-- ltac2 | | |-- array_lib.v | | |-- binder.v | | |-- compat.v | | |-- constr.v | | |-- errors.v | | |-- example1.v | | |-- example2.v | | |-- ltac2env.v | | |-- matching.v | | |-- notations.v | | |-- quot.v | | |-- rebind.v | | |-- stuff | | | |-- ltac2.v | | |-- syntax.v | | |-- tacticals.v | | |-- term_notations.v | | |-- typing.v | |-- Makefile | |-- micromega | | |-- bertot.v | | |-- bug_10158.v | | |-- bug_11191a.v | | |-- bug_11191b.v | | |-- bug_11270.v | | |-- bug_11436.v | | |-- bug_12210.v | | |-- bug_9162.v | | |-- evars_loops_in_8_10_fixed_8_11.v | | |-- example_nia.v | | |-- example.v | | |-- heap3_vcgen_25.v | | |-- non_lin_ci.v | | |-- qexample.v | | |-- rexample.v | | |-- rsyntax.v | | |-- square.v | | |-- zomicron.v | |-- misc | | |-- 4722.sh | | |-- 7595 | | | |-- base.v | | | |-- FOO.v | | |-- 7595.sh | | |-- 7704.sh | | |-- aux7704.v | | |-- changelog.sh | | |-- coqc_dash_o.sh | | |-- coqc_dash_o.v | | |-- deps | | | |-- A | | | | |-- A.v | | | |-- B | | | | |-- A.v | | | | |-- B.v | | | |-- checksum.v | | | |-- client | | | | |-- bar.v | | | | |-- foo.v | | | |-- deps.out | | | |-- lib | | | | |-- foo.v | | | |-- αβ | | | |-- γδ.v | | | |-- εζ.v | | |-- deps-checksum.sh | | |-- deps-order.sh | | |-- deps-utf8.sh | | |-- exitstatus | | | |-- illtyped.v | | |-- exitstatus.sh | | |-- poly-capture-global-univs | | | |-- _CoqProject | | | |-- src | | | | |-- evilImpl.ml | | | | |-- evilImpl.mli | | | | |-- evil.mlg | | | | |-- evil_plugin.mlpack | | | |-- theories | | | |-- evil.v | | |-- poly-capture-global-univs.sh | | |-- printers.sh | | |-- quick-include | | | |-- file1.v | | | |-- file2.v | | |-- quick-include.sh | | |-- quotation_token | | | |-- _CoqProject | | | |-- src | | | | |-- quotation.mlg | | | | |-- quotation_plugin.mlpack | | | |-- theories | | | |-- quotation.v | | |-- quotation_token.sh | | |-- redirect_printing.out | | |-- redirect_printing.sh | | |-- redirect_printing.v | | |-- side-eff-leak-univs | | | |-- _CoqProject | | | |-- src | | | | |-- evil.mlg | | | | |-- evil_plugin.mlpack | | | |-- theories | | | |-- evil.v | | |-- side-eff-leak-univs.sh | | |-- universes | | | |-- build_all_stdlib.sh | | | |-- dune | | | |-- universes.v | | |-- universes.sh | | |-- votour.sh | |-- modules | | |-- cumpoly.v | | |-- Demo.v | | |-- errors.v | | |-- fun_objects.v | | |-- grammar.v | | |-- ind.v | | |-- injection_discriminate_inversion.v | | |-- mod_decl.v | | |-- modeq.v | | |-- modul.v | | |-- Nat.v | | |-- nested_mod_types.v | | |-- objects2.v | | |-- objects.v | | |-- obj.v | | |-- pliczek.v | | |-- plik.v | | |-- polymorphism2.v | | |-- polymorphism.v | | |-- PO.v | | |-- Przyklad.v | | |-- pseudo_circular_with.v | | |-- resolver.v | | |-- SeveralWith.v | | |-- sig.v | | |-- sub_objects.v | | |-- subtyping.v | | |-- Tescik.v | | |-- WithDefUBinders.v | |-- ocaml_pwd.ml | |-- output | | |-- allBytes.out | | |-- allBytes.v | | |-- Arguments.out | | |-- Arguments_renaming.out | | |-- Arguments_renaming.v | | |-- ArgumentsScope.out | | |-- ArgumentsScope.v | | |-- Arguments.v | | |-- auto.out | | |-- auto.v | | |-- BadOptionValueType.out | | |-- BadOptionValueType.v | | |-- Binder.out | | |-- Binder.v | | |-- bug_11342.out | | |-- bug_11342.v | | |-- bug_11608.out | | |-- bug_11608.v | | |-- bug_11934.out | | |-- bug_11934.v | | |-- bug_12159.out | | |-- bug_12159.v | | |-- bug12442.out | | |-- bug12442.v | | |-- bug5778.out | | |-- bug5778.v | | |-- bug6404.out | | |-- bug6404.v | | |-- bug6821.out | | |-- bug6821.v | | |-- bug7191.out | | |-- bug7191.v | | |-- bug7348.out | | |-- bug7348.v | | |-- bug_8206.out | | |-- bug_8206.v | | |-- bug_9180.out | | |-- bug_9180.v | | |-- bug_9370.out | | |-- bug_9370.v | | |-- Cases.out | | |-- Cases.v | | |-- clear.out | | |-- clear.v | | |-- Coercions.out | | |-- Coercions.v | | |-- CompactContexts.out | | |-- CompactContexts.v | | |-- Deprecation.out | | |-- Deprecation.v | | |-- Emacs_and_diffs.out | | |-- Emacs_and_diffs.v | | |-- EqNotation.out | | |-- EqNotation.v | | |-- ErrorInCanonicalStructures2.out | | |-- ErrorInCanonicalStructures2.v | | |-- ErrorInCanonicalStructures.out | | |-- ErrorInCanonicalStructures.v | | |-- ErrorInModule.out | | |-- ErrorInModule.v | | |-- ErrorInSection.out | | |-- ErrorInSection.v | | |-- ErrorLocation_12152_1.out | | |-- ErrorLocation_12152_1.v | | |-- ErrorLocation_12152_2.out | | |-- ErrorLocation_12152_2.v | | |-- ErrorLocation_12255.out | | |-- ErrorLocation_12255.v | | |-- Error_msg_diffs.out | | |-- Error_msg_diffs.v | | |-- Errors.out | | |-- Errors.v | | |-- Existentials.out | | |-- Existentials.v | | |-- Extraction_Haskell_String_12258.out | | |-- Extraction_Haskell_String_12258.v | | |-- Extraction_infix.out | | |-- Extraction_infix.v | | |-- Extraction_matchs_2413.out | | |-- Extraction_matchs_2413.v | | |-- ExtractionString.out | | |-- ExtractionString.v | | |-- Fixpoint.out | | |-- Fixpoint.v | | |-- FloatExtraction.out | | |-- FloatExtraction.v | | |-- FloatSyntax.out | | |-- FloatSyntax.v | | |-- FunExt.out | | |-- FunExt.v | | |-- goal_output.out | | |-- goal_output.v | | |-- idtac.out | | |-- idtac.v | | |-- Implicit.out | | |-- ImplicitTypes.out | | |-- ImplicitTypes.v | | |-- Implicit.v | | |-- Inductive.out | | |-- Inductive.v | | |-- inference.out | | |-- inference.v | | |-- InitSyntax.out | | |-- InitSyntax.v | | |-- injection.out | | |-- injection.v | | |-- Int31Syntax.out | | |-- Int31Syntax.v | | |-- Int63Syntax.out | | |-- Int63Syntax.v | | |-- interleave_options_bad_order.out | | |-- interleave_options_bad_order.v | | |-- interleave_options_correct_order.out | | |-- interleave_options_correct_order.v | | |-- Intuition.out | | |-- Intuition.v | | |-- InvalidDisjunctiveIntro.out | | |-- InvalidDisjunctiveIntro.v | | |-- load | | | |-- Load_noproof.v | | | |-- Load_openproof.v | | | |-- Load_proof.v | | |-- Load.out | | |-- Load.v | | |-- locate.out | | |-- locate.v | | |-- ltac2_notations_eval_in.out | | |-- ltac2_notations_eval_in.v | | |-- ltac_extra_args.out | | |-- ltac_extra_args.v | | |-- ltac_missing_args.out | | |-- ltac_missing_args.v | | |-- ltac.out | | |-- ltac.v | | |-- Match_subterm.out | | |-- Match_subterm.v | | |-- MExtraction.v | | |-- names.out | | |-- names.v | | |-- Nametab.out | | |-- Nametab.v | | |-- Naming.out | | |-- Naming.v | | |-- NatSyntax.out | | |-- NatSyntax.v | | |-- NoAxiomFromR.out | | |-- NoAxiomFromR.v | | |-- Notations2.out | | |-- Notations2.v | | |-- Notations3.out | | |-- Notations3.v | | |-- Notations4.out | | |-- Notations4.v | | |-- Notations5.out | | |-- Notations5.v | | |-- Notations.out | | |-- NotationsSigma.out | | |-- NotationsSigma.v | | |-- Notations.v | | |-- NumeralNotations.out | | |-- NumeralNotations.v | | |-- onlyprinting.out | | |-- onlyprinting.v | | |-- optimize_heap.out | | |-- optimize_heap.v | | |-- PatternsInBinders.out | | |-- PatternsInBinders.v | | |-- PrintAssumptions.out | | |-- PrintAssumptions.v | | |-- PrintCanonicalProjections.out | | |-- PrintCanonicalProjections.v | | |-- PrintInfos.out | | |-- PrintInfos.v | | |-- PrintingParentheses.out | | |-- PrintingParentheses.v | | |-- print_ltac.out | | |-- print_ltac.v | | |-- PrintModule.out | | |-- PrintModule.v | | |-- PrintUnivsSubgraph.out | | |-- PrintUnivsSubgraph.v | | |-- Projections.out | | |-- Projections.v | | |-- QArithSyntax.out | | |-- QArithSyntax.v | | |-- qualification.out | | |-- qualification.v | | |-- RealSyntax.out | | |-- RealSyntax.v | | |-- RecognizePluginWarning.out | | |-- RecognizePluginWarning.v | | |-- RecordFieldErrors.out | | |-- RecordFieldErrors.v | | |-- RecordMissingField.out | | |-- RecordMissingField.v | | |-- Record.out | | |-- Record.v | | |-- reduction.out | | |-- reduction.v | | |-- relaxed_ambiguous_paths.out | | |-- relaxed_ambiguous_paths.v | | |-- rewrite_2172.out | | |-- rewrite_2172.v | | |-- SearchHead.out | | |-- SearchHead.v | | |-- Search.out | | |-- SearchPattern.out | | |-- SearchPattern.v | | |-- SearchRewrite.out | | |-- SearchRewrite.v | | |-- Search.v | | |-- set.out | | |-- set.v | | |-- ShowMatch.out | | |-- ShowMatch.v | | |-- Show.out | | |-- ShowProof.out | | |-- ShowProof.v | | |-- Show.v | | |-- simpl.out | | |-- simpl.v | | |-- sint63Notation.out | | |-- sint63Notation.v | | |-- ssr_clear.out | | |-- ssr_clear.v | | |-- ssr_explain_match.out | | |-- ssr_explain_match.v | | |-- ssr_under.out | | |-- ssr_under.v | | |-- StringSyntax.out | | |-- StringSyntax.v | | |-- subst.out | | |-- subst.v | | |-- SuggestProofUsing.out | | |-- SuggestProofUsing.v | | |-- Sum.out | | |-- Sum.v | | |-- Tactics.out | | |-- Tactics.v | | |-- TranspModtype.out | | |-- TranspModtype.v | | |-- TypeclassDebug.out | | |-- TypeclassDebug.v | | |-- UnclosedBlocks.out | | |-- UnclosedBlocks.v | | |-- undeclared_key.out | | |-- undeclared_key.v | | |-- Unicode.out | | |-- Unicode.v | | |-- unifconstraints.out | | |-- unifconstraints.v | | |-- unification.out | | |-- unification.v | | |-- UnivBinders.out | | |-- UnivBinders.v | | |-- UselessSyndef.out | | |-- UselessSyndef.v | | |-- UsePluginWarning.out | | |-- UsePluginWarning.v | | |-- Warnings.out | | |-- Warnings.v | | |-- ZSyntax.out | | |-- ZSyntax.v | |-- output-coqchk | | |-- bug_5030.out | | |-- bug_5030.v | |-- output-coqtop | | |-- DependentEvars2.out | | |-- DependentEvars2.v | | |-- DependentEvars.out | | |-- DependentEvars.v | | |-- ShowGoal.out | | |-- ShowGoal.v | | |-- ShowProofDiffs.out | | |-- ShowProofDiffs.v | |-- output-modulo-time | | |-- ltacprof_abstract.out | | |-- ltacprof_abstract.v | | |-- ltacprof_cutoff.out | | |-- ltacprof.out | | |-- ltacprof.v | |-- prerequisite | | |-- admit.v | | |-- bind_univs.v | | |-- make_local.v | | |-- make_notation.v | | |-- module_bug7192.v | | |-- module_bug8416.v | | |-- ssr_mini_mathcomp.v | | |-- ssr_ssrsyntax1.v | |-- primitive | | |-- float | | | |-- add.v | | | |-- classify.v | | | |-- compare.v | | | |-- coq_env_double_array.v | | | |-- div.v | | | |-- double_rounding.v | | | |-- frexp.v | | | |-- gen_compare.sh | | | |-- ldexp.v | | | |-- mul.v | | | |-- next_up_down.v | | | |-- normfr_mantissa.v | | | |-- spec_conv.v | | | |-- sqrt.v | | | |-- sub.v | | | |-- syntax.v | | | |-- valid_binary_conv.v | | | |-- zero.v | | |-- uint63 | | |-- addcarryc.v | | |-- addc.v | | |-- addmuldiv.v | | |-- add.v | | |-- compare.v | | |-- diveucl_21.v | | |-- diveucl.v | | |-- div.v | | |-- eqb.v | | |-- head0.v | | |-- isint.v | | |-- land.v | | |-- leb.v | | |-- lor.v | | |-- lsl.v | | |-- lsr.v | | |-- ltb.v | | |-- lxor.v | | |-- mod.v | | |-- mulc.v | | |-- mul.v | | |-- reduction.v | | |-- subcarryc.v | | |-- subc.v | | |-- sub.v | | |-- tail0.v | | |-- unsigned.v | |-- README.md | |-- report.sh | |-- ssr | | |-- absevarprop.v | | |-- abstract_var2.v | | |-- autoclean.v | | |-- bang_rewrite.v | | |-- binders_of.v | | |-- binders.v | | |-- case_polyuniv.v | | |-- case_TC2.v | | |-- case_TC3.v | | |-- case_TC.v | | |-- caseview.v | | |-- congr.v | | |-- deferclear.v | | |-- delayed_clear_rename.v | | |-- dependent_type_err.v | | |-- derive_inversion.v | | |-- elim2.v | | |-- elim_noquant.v | | |-- elim_pattern.v | | |-- elim.v | | |-- first_n.v | | |-- gen_have.v | | |-- gen_pattern.v | | |-- havesuff.v | | |-- have_TC.v | | |-- have_transp.v | | |-- have_view_idiom.v | | |-- if_isnt.v | | |-- intro_beta.v | | |-- intro_noop.v | | |-- ipatalternation.v | | |-- ipat_clear_if_id.v | | |-- ipat_fast_any.v | | |-- ipat_fastid.v | | |-- ipat_replace.v | | |-- ipat_seed.v | | |-- ipat_tac.v | | |-- ipat_tmp.v | | |-- ltac_have.v | | |-- ltac_in.v | | |-- misc_extended.v | | |-- misc_tc.v | | |-- move_after.v | | |-- multiview.v | | |-- nonPropType.v | | |-- occarrow.v | | |-- over.v | | |-- patnoX.v | | |-- pattern.v | | |-- predRewrite.v | | |-- primproj.v | | |-- rewpatterns.v | | |-- rew_polyuniv.v | | |-- rewrite_illtyped.v | | |-- rewrtite_err_msg.v | | |-- set_lamda.v | | |-- set_pattern.v | | |-- set_polyuniv.v | | |-- simpl_done.v | | |-- ssrpattern.v | | |-- ssrsyntax2.v | | |-- tc.v | | |-- try_case.v | | |-- typeof.v | | |-- under.v | | |-- unfold_fold_polyuniv.v | | |-- unfold_Opaque.v | | |-- unkeyed.v | | |-- view_case.v | | |-- wlogletin.v | | |-- wlog_suff.v | | |-- wlong_intro.v | |-- stm | | |-- arg_filter_1.v | | |-- classify_set_proof_mode_9093.v | | |-- delayed_restrict_univs_9093.v | | |-- Nijmegen_QArithSternBrocot_Zaux.v | |-- success | | |-- abstract_chain.v | | |-- abstract_poly.v | | |-- Abstract.v | | |-- AdvancedCanonicalStructure.v | | |-- AdvancedTypeClasses.v | | |-- all_check.v | | |-- applyTC.v | | |-- apply.v | | |-- attribute_syntax.v | | |-- autointros.v | | |-- autorewrite.v | | |-- auto.v | | |-- BidirectionalityHints.v | | |-- boundvars.v | | |-- BracketsWithGoalSelector.v | | |-- btauto.v | | |-- bteauto.v | | |-- bullet.v | | |-- CanonicalStructure.v | | |-- Case10.v | | |-- Case11.v | | |-- Case12.v | | |-- Case13.v | | |-- Case14.v | | |-- Case15.v | | |-- Case16.v | | |-- Case17.v | | |-- Case18.v | | |-- Case19.v | | |-- Case1.v | | |-- Case20.v | | |-- Case21.v | | |-- Case22.v | | |-- Case2.v | | |-- Case3.v | | |-- Case5.v | | |-- Case6.v | | |-- Case7.v | | |-- Case8.v | | |-- Case9.v | | |-- CaseAlias.v | | |-- CaseInClause.v | | |-- Cases_bug1834.v | | |-- Cases_bug3758.v | | |-- CasesDep.v | | |-- Cases.v | | |-- cbn.v | | |-- cc.v | | |-- change_pattern.v | | |-- change.v | | |-- Check.v | | |-- clear.v | | |-- coercions.v | | |-- cofixtac.v | | |-- coindprim.v | | |-- CombinedScheme.v | | |-- CompatCurrentFlag.v | | |-- CompatOldFlag.v | | |-- CompatPreviousFlag.v | | |-- Conjecture.v | | |-- contradiction.v | | |-- ConversionOrder.v | | |-- conv_pbs.v | | |-- coqbugs0181.v | | |-- cumulativity.v | | |-- custom_entry.v | | |-- Decompose.v | | |-- dependentind.v | | |-- destruct.v | | |-- DHyp.v | | |-- Discriminate_HoTT.v | | |-- Discriminate.v | | |-- DiscrR.v | | |-- dtauto_let_deps.v | | |-- eauto.v | | |-- eqdecide.v | | |-- eta.v | | |-- evars.v | | |-- export_hint.v | | |-- extraction_dep.v | | |-- extraction_impl.v | | |-- extraction_polyprop.v | | |-- extraction.v | | |-- Field.v | | |-- Fixpoint.v | | |-- fix.v | | |-- forward.v | | |-- Funind.v | | |-- Generalization.v | | |-- Generalize.v | | |-- goal_selector.v | | |-- guard.v | | |-- hintdb_in_ltac_bis.v | | |-- hintdb_in_ltac.v | | |-- HintMode.v | | |-- Hints.v | | |-- hyps_inclusion.v | | |-- if.v | | |-- ImplicitArguments.v | | |-- implicit.v | | |-- import_lib.v | | |-- import_mod.v | | |-- Import.v | | |-- indelim.v | | |-- inds_type_sec.v | | |-- Inductive.v | | |-- InductiveVsImplicitsVsTC.v | | |-- induct.v | | |-- Injection.v | | |-- intros.v | | |-- InversionSigma.v | | |-- Inversion.v | | |-- keyedrewrite.v | | |-- LetIn.v | | |-- LetPat.v | | |-- letproj.v | | |-- let_universes.v | | |-- LocalDefinition.v | | |-- LraTest.v | | |-- LtacDeprecation.v | | |-- ltac_match_pattern_names.v | | |-- ltac_plus.v | | |-- ltacprof.v | | |-- ltac.v | | |-- MatchFail.v | | |-- Mod_ltac.v | | |-- Mod_params.v | | |-- Mod_strengthen.v | | |-- Mod_type.v | | |-- module_with_def_univ_poly.v | | |-- mutual_ind.v | | |-- mutual_record.v | | |-- namedunivs.v | | |-- name_mangling.v | | |-- NatRing.v | | |-- Nia.v | | |-- NotationDeprecation.v | | |-- Notations2.v | | |-- NotationsAndLtac.v | | |-- Notations.v | | |-- Nsatz.v | | |-- NumberScopes.v | | |-- NumeralNotationsNoLocal.v | | |-- Omega0.v | | |-- Omega2.v | | |-- OmegaPre.v | | |-- Omega.v | | |-- onlyprinting.v | | |-- options.v | | |-- par_abstract.v | | |-- paralleltac.v | | |-- parsing.v | | |-- PartialImport.v | | |-- PatternsInBinders.v | | |-- pattern.v | | |-- PCase.v | | |-- polymorphism.v | | |-- pose.v | | |-- PPFix.v | | |-- primitiveproj.v | | |-- PrintSortedUniverses.v | | |-- Print.v | | |-- private_univs.v | | |-- programequality.v | | |-- ProgramWf.v | | |-- Projection.v | | |-- proof_using.v | | |-- rapply.v | | |-- record_syntax.v | | |-- Record.v | | |-- RecTutorial.v | | |-- RefineInstance.v | | |-- refine.v | | |-- Reg.v | | |-- Remark.v | | |-- remember.v | | |-- Rename.v | | |-- Reordering.v | | |-- replace.v | | |-- Require.v | | |-- rewrite_dep.v | | |-- rewrite_evar.v | | |-- rewrite_in.v | | |-- rewrite_iterated.v | | |-- RewriteRegisteredElim.v | | |-- rewrite_strat.v | | |-- rewrite.v | | |-- ROmega0.v | | |-- ROmega2.v | | |-- ROmega4.v | | |-- ROmegaPre.v | | |-- ROmega.v | | |-- SchemeEquality.v | | |-- Scheme.v | | |-- Scopes.v | | |-- search.v | | |-- section_poly.v | | |-- Section.v | | |-- setoid_ring_module.v | | |-- setoid_test2.v | | |-- setoid_test_function_space.v | | |-- setoid_test.v | | |-- setoid_unif.v | | |-- set.v | | |-- ShowExtraction.v | | |-- shrink_abstract.v | | |-- shrink_obligations.v | | |-- sideff.v | | |-- Simplify_eq.v | | |-- simpl_tuning.v | | |-- simpl.v | | |-- somatching.v | | |-- specialize.v | | |-- sprop_hcons.v | | |-- sprop.v | | |-- ssrpattern.v | | |-- strategy.v | | |-- subst.v | | |-- TacticNotation1.v | | |-- TacticNotation2.v | | |-- tac_wit_ref.v | | |-- Tauto.v | | |-- telescope_canonical.v | | |-- Template.v | | |-- TestRefine.v | | |-- transparent_abstract.v | | |-- tryif.v | | |-- Try.v | | |-- Typeclasses.v | | |-- typing_flags.v | | |-- unfold.v | | |-- unicode_utf8.v | | |-- unidecls.v | | |-- unification.v | | |-- uniform_inductive_parameters.v | | |-- universes_coercion.v | | |-- univers.v | | |-- univnames.v | | |-- univscompute.v | | |-- unshelve.v | | |-- vm_evars.v | | |-- vm_records.v | | |-- vm_univ_poly_match.v | | |-- vm_univ_poly.v | | |-- with_strategy.v | |-- tools | | |-- update-compat | | |-- run.sh | |-- typeclasses | | |-- backtrack.v | | |-- clrewrite.v | | |-- deftwice.v | | |-- NewSetoid.v | | |-- open_constr.v | | |-- unification_delta.v | |-- unit-tests | | |-- clib | | | |-- inteq.ml | | | |-- unicode_tests.ml | | |-- lib | | | |-- pp_big_vect.ml | | |-- printing | | | |-- proof_diffs_test.ml | | |-- src | | |-- utest.ml | | |-- utest.mli | |-- vio | | |-- numeral.v | | |-- print.v | | |-- section.v | | |-- seff.v | | |-- simple.v | | |-- univ_constraints_statements.v | |-- vos | |-- A.v | |-- B.v | |-- C.v | |-- run.sh |-- theories | |-- Arith | | |-- Arith_base.v | | |-- Arith.v | | |-- Between.v | | |-- Bool_nat.v | | |-- Compare_dec.v | | |-- Compare.v | | |-- Div2.v | | |-- EqNat.v | | |-- Euclid.v | | |-- Even.v | | |-- Factorial.v | | |-- Gt.v | | |-- Le.v | | |-- Lt.v | | |-- Max.v | | |-- Minus.v | | |-- Min.v | | |-- Mult.v | | |-- Peano_dec.v | | |-- PeanoNat.v | | |-- Plus.v | | |-- Wf_nat.v | |-- Bool | | |-- BoolEq.v | | |-- BoolOrder.v | | |-- Bool.v | | |-- Bvector.v | | |-- DecBool.v | | |-- IfProp.v | | |-- Sumbool.v | | |-- Zerob.v | |-- btauto | | |-- Algebra.v | | |-- Btauto.v | | |-- Reflect.v | |-- Classes | | |-- CEquivalence.v | | |-- CMorphisms.v | | |-- CRelationClasses.v | | |-- DecidableClass.v | | |-- Equivalence.v | | |-- EquivDec.v | | |-- Init.v | | |-- Morphisms_Prop.v | | |-- Morphisms_Relations.v | | |-- Morphisms.v | | |-- RelationClasses.v | | |-- RelationPairs.v | | |-- SetoidClass.v | | |-- SetoidDec.v | | |-- SetoidTactics.v | |-- Compat | | |-- AdmitAxiom.v | | |-- Coq810.v | | |-- Coq811.v | | |-- Coq812.v | |-- derive | | |-- Derive.v | |-- dune | |-- extraction | | |-- Extraction.v | | |-- ExtrHaskellBasic.v | | |-- ExtrHaskellNatInteger.v | | |-- ExtrHaskellNatInt.v | | |-- ExtrHaskellNatNum.v | | |-- ExtrHaskellString.v | | |-- ExtrHaskellZInteger.v | | |-- ExtrHaskellZInt.v | | |-- ExtrHaskellZNum.v | | |-- ExtrOcamlBasic.v | | |-- ExtrOcamlBigIntConv.v | | |-- ExtrOcamlChar.v | | |-- ExtrOCamlFloats.v | | |-- ExtrOCamlInt63.v | | |-- ExtrOcamlIntConv.v | | |-- ExtrOcamlNatBigInt.v | | |-- ExtrOcamlNatInt.v | | |-- ExtrOcamlNativeString.v | | |-- ExtrOcamlString.v | | |-- ExtrOcamlZBigInt.v | | |-- ExtrOcamlZInt.v | |-- Floats | | |-- FloatAxioms.v | | |-- FloatClass.v | | |-- FloatLemmas.v | | |-- FloatOps.v | | |-- Floats.v | | |-- PrimFloat.v | | |-- SpecFloat.v | |-- FSets | | |-- FMapAVL.v | | |-- FMapFacts.v | | |-- FMapFullAVL.v | | |-- FMapInterface.v | | |-- FMapList.v | | |-- FMapPositive.v | | |-- FMaps.v | | |-- FMapWeakList.v | | |-- FSetAVL.v | | |-- FSetBridge.v | | |-- FSetCompat.v | | |-- FSetDecide.v | | |-- FSetEqProperties.v | | |-- FSetFacts.v | | |-- FSetInterface.v | | |-- FSetList.v | | |-- FSetPositive.v | | |-- FSetProperties.v | | |-- FSets.v | | |-- FSetToFiniteSet.v | | |-- FSetWeakList.v | |-- funind | | |-- FunInd.v | | |-- Recdef.v | |-- Init | | |-- Byte.v | | |-- _CoqProject | | |-- Datatypes.v | | |-- Decimal.v | | |-- Hexadecimal.v | | |-- Logic_Type.v | | |-- Logic.v | | |-- Ltac.v | | |-- Nat.v | | |-- Notations.v | | |-- Numeral.v | | |-- Peano.v | | |-- Prelude.v | | |-- Specif.v | | |-- Tactics.v | | |-- Tauto.v | | |-- Wf.v | |-- Lists | | |-- ListDec.v | | |-- ListSet.v | | |-- ListTactics.v | | |-- List.v | | |-- SetoidList.v | | |-- SetoidPermutation.v | | |-- StreamMemo.v | | |-- Streams.v | |-- Logic | | |-- Berardi.v | | |-- ChoiceFacts.v | | |-- ClassicalChoice.v | | |-- ClassicalDescription.v | | |-- ClassicalEpsilon.v | | |-- ClassicalFacts.v | | |-- Classical_Pred_Type.v | | |-- Classical_Prop.v | | |-- ClassicalUniqueChoice.v | | |-- Classical.v | | |-- ConstructiveEpsilon.v | | |-- Decidable.v | | |-- Description.v | | |-- Diaconescu.v | | |-- Epsilon.v | | |-- Eqdep_dec.v | | |-- EqdepFacts.v | | |-- Eqdep.v | | |-- ExtensionalFunctionRepresentative.v | | |-- ExtensionalityFacts.v | | |-- FinFun.v | | |-- FunctionalExtensionality.v | | |-- HLevels.v | | |-- Hurkens.v | | |-- IndefiniteDescription.v | | |-- JMeq.v | | |-- ProofIrrelevanceFacts.v | | |-- ProofIrrelevance.v | | |-- PropExtensionalityFacts.v | | |-- PropExtensionality.v | | |-- PropFacts.v | | |-- RelationalChoice.v | | |-- SetIsType.v | | |-- SetoidChoice.v | | |-- StrictProp.v | | |-- WeakFan.v | | |-- WKL.v | |-- micromega | | |-- DeclConstant.v | | |-- EnvRing.v | | |-- Env.v | | |-- Fourier_util.v | | |-- Fourier.v | | |-- Lia.v | | |-- Lqa.v | | |-- Lra.v | | |-- MExtraction.v | | |-- OrderedRing.v | | |-- Psatz.v | | |-- QMicromega.v | | |-- Refl.v | | |-- RingMicromega.v | | |-- RMicromega.v | | |-- Tauto.v | | |-- VarMap.v | | |-- ZArith_hints.v | | |-- ZCoeff.v | | |-- ZifyBool.v | | |-- ZifyClasses.v | | |-- ZifyComparison.v | | |-- ZifyInst.v | | |-- ZifyPow.v | | |-- Zify.v | | |-- ZMicromega.v | | |-- Ztac.v | |-- MSets | | |-- MSetAVL.v | | |-- MSetDecide.v | | |-- MSetEqProperties.v | | |-- MSetFacts.v | | |-- MSetGenTree.v | | |-- MSetInterface.v | | |-- MSetList.v | | |-- MSetPositive.v | | |-- MSetProperties.v | | |-- MSetRBT.v | | |-- MSets.v | | |-- MSetToFiniteSet.v | | |-- MSetWeakList.v | |-- NArith | | |-- BinNatDef.v | | |-- BinNat.v | | |-- NArith.v | | |-- Ndec.v | | |-- Ndigits.v | | |-- Ndist.v | | |-- Ndiv_def.v | | |-- Ngcd_def.v | | |-- Nnat.v | | |-- Nsqrt_def.v | |-- nsatz | | |-- NsatzTactic.v | | |-- Nsatz.v | |-- Numbers | | |-- AltBinNotations.v | | |-- BinNums.v | | |-- Cyclic | | | |-- Abstract | | | | |-- CyclicAxioms.v | | | | |-- DoubleType.v | | | | |-- NZCyclic.v | | | |-- Int31 | | | | |-- Cyclic31.v | | | | |-- Int31.v | | | | |-- Ring31.v | | | |-- Int63 | | | | |-- Cyclic63.v | | | | |-- Int63.v | | | | |-- Ring63.v | | | |-- ZModulo | | | |-- ZModulo.v | | |-- DecimalFacts.v | | |-- DecimalNat.v | | |-- DecimalN.v | | |-- DecimalPos.v | | |-- DecimalQ.v | | |-- DecimalString.v | | |-- DecimalZ.v | | |-- HexadecimalFacts.v | | |-- HexadecimalNat.v | | |-- HexadecimalN.v | | |-- HexadecimalPos.v | | |-- HexadecimalQ.v | | |-- HexadecimalString.v | | |-- HexadecimalZ.v | | |-- Integer | | | |-- Abstract | | | | |-- ZAddOrder.v | | | | |-- ZAdd.v | | | | |-- ZAxioms.v | | | | |-- ZBase.v | | | | |-- ZBits.v | | | | |-- ZDivEucl.v | | | | |-- ZDivFloor.v | | | | |-- ZDivTrunc.v | | | | |-- ZGcd.v | | | | |-- ZLcm.v | | | | |-- ZLt.v | | | | |-- ZMaxMin.v | | | | |-- ZMulOrder.v | | | | |-- ZMul.v | | | | |-- ZParity.v | | | | |-- ZPow.v | | | | |-- ZProperties.v | | | | |-- ZSgnAbs.v | | | |-- Binary | | | | |-- ZBinary.v | | | |-- NatPairs | | | |-- ZNatPairs.v | | |-- NaryFunctions.v | | |-- NatInt | | | |-- NZAddOrder.v | | | |-- NZAdd.v | | | |-- NZAxioms.v | | | |-- NZBase.v | | | |-- NZBits.v | | | |-- NZDiv.v | | | |-- NZDomain.v | | | |-- NZGcd.v | | | |-- NZLog.v | | | |-- NZMulOrder.v | | | |-- NZMul.v | | | |-- NZOrder.v | | | |-- NZParity.v | | | |-- NZPow.v | | | |-- NZProperties.v | | | |-- NZSqrt.v | | |-- Natural | | | |-- Abstract | | | | |-- NAddOrder.v | | | | |-- NAdd.v | | | | |-- NAxioms.v | | | | |-- NBase.v | | | | |-- NBits.v | | | | |-- NDefOps.v | | | | |-- NDiv.v | | | | |-- NGcd.v | | | | |-- NIso.v | | | | |-- NLcm.v | | | | |-- NLog.v | | | | |-- NMaxMin.v | | | | |-- NMulOrder.v | | | | |-- NOrder.v | | | | |-- NParity.v | | | | |-- NPow.v | | | | |-- NProperties.v | | | | |-- NSqrt.v | | | | |-- NStrongRec.v | | | | |-- NSub.v | | | |-- Binary | | | | |-- NBinary.v | | | |-- Peano | | | |-- NPeano.v | | |-- NumPrelude.v | |-- omega | | |-- OmegaLemmas.v | | |-- OmegaPlugin.v | | |-- OmegaTactic.v | | |-- Omega.v | | |-- PreOmega.v | |-- PArith | | |-- BinPosDef.v | | |-- BinPos.v | | |-- PArith.v | | |-- Pnat.v | | |-- POrderedType.v | |-- Program | | |-- Basics.v | | |-- Combinators.v | | |-- Equality.v | | |-- Program.v | | |-- Subset.v | | |-- Syntax.v | | |-- Tactics.v | | |-- Utils.v | | |-- Wf.v | |-- QArith | | |-- Qabs.v | | |-- QArith_base.v | | |-- QArith.v | | |-- Qcabs.v | | |-- Qcanon.v | | |-- Qfield.v | | |-- Qminmax.v | | |-- QOrderedType.v | | |-- Qpower.v | | |-- Qreals.v | | |-- Qreduction.v | | |-- Qring.v | | |-- Qround.v | |-- Reals | | |-- Abstract | | | |-- ConstructiveAbs.v | | | |-- ConstructiveLimits.v | | | |-- ConstructiveLUB.v | | | |-- ConstructiveMinMax.v | | | |-- ConstructivePower.v | | | |-- ConstructiveRealsMorphisms.v | | | |-- ConstructiveReals.v | | | |-- ConstructiveSum.v | | |-- Alembert.v | | |-- AltSeries.v | | |-- ArithProp.v | | |-- Binomial.v | | |-- Cauchy | | | |-- ConstructiveCauchyAbs.v | | | |-- ConstructiveCauchyRealsMult.v | | | |-- ConstructiveCauchyReals.v | | | |-- ConstructiveRcomplete.v | | |-- Cauchy_prod.v | | |-- ClassicalConstructiveReals.v | | |-- ClassicalDedekindReals.v | | |-- Cos_plus.v | | |-- Cos_rel.v | | |-- DiscrR.v | | |-- Exp_prop.v | | |-- Integration.v | | |-- Machin.v | | |-- MVT.v | | |-- NewtonInt.v | | |-- PartSum.v | | |-- PSeries_reg.v | | |-- Ranalysis1.v | | |-- Ranalysis2.v | | |-- Ranalysis3.v | | |-- Ranalysis4.v | | |-- Ranalysis5.v | | |-- Ranalysis_reg.v | | |-- Ranalysis.v | | |-- Ratan.v | | |-- Raxioms.v | | |-- Rbase.v | | |-- Rbasic_fun.v | | |-- Rcomplete.v | | |-- Rdefinitions.v | | |-- Rderiv.v | | |-- Reals.v | | |-- Rfunctions.v | | |-- Rgeom.v | | |-- RiemannInt_SF.v | | |-- RiemannInt.v | | |-- R_Ifp.v | | |-- RIneq.v | | |-- Rlimit.v | | |-- RList.v | | |-- Rlogic.v | | |-- Rminmax.v | | |-- ROrderedType.v | | |-- Rpow_def.v | | |-- Rpower.v | | |-- Rprod.v | | |-- Rregisternames.v | | |-- Rseries.v | | |-- Rsigma.v | | |-- Rsqrt_def.v | | |-- R_sqrt.v | | |-- R_sqr.v | | |-- Rtopology.v | | |-- Rtrigo1.v | | |-- Rtrigo_alt.v | | |-- Rtrigo_calc.v | | |-- Rtrigo_def.v | | |-- Rtrigo_facts.v | | |-- Rtrigo_fun.v | | |-- Rtrigo_reg.v | | |-- Rtrigo.v | | |-- Runcountable.v | | |-- SeqProp.v | | |-- SeqSeries.v | | |-- SplitAbsolu.v | | |-- SplitRmult.v | | |-- Sqrt_reg.v | |-- Relations | | |-- Operators_Properties.v | | |-- Relation_Definitions.v | | |-- Relation_Operators.v | | |-- Relations.v | |-- rtauto | | |-- Bintree.v | | |-- Rtauto.v | |-- setoid_ring | | |-- Algebra_syntax.v | | |-- ArithRing.v | | |-- BinList.v | | |-- Cring.v | | |-- Field_tac.v | | |-- Field_theory.v | | |-- Field.v | | |-- InitialRing.v | | |-- Integral_domain.v | | |-- NArithRing.v | | |-- Ncring_initial.v | | |-- Ncring_polynom.v | | |-- Ncring_tac.v | | |-- Ncring.v | | |-- RealField.v | | |-- Ring_base.v | | |-- Ring_polynom.v | | |-- Rings_Q.v | | |-- Rings_R.v | | |-- Rings_Z.v | | |-- Ring_tac.v | | |-- Ring_theory.v | | |-- Ring.v | | |-- ZArithRing.v | |-- Setoids | | |-- Setoid.v | |-- Sets | | |-- Classical_sets.v | | |-- Constructive_sets.v | | |-- Cpo.v | | |-- Ensembles.v | | |-- Finite_sets_facts.v | | |-- Finite_sets.v | | |-- Image.v | | |-- Infinite_sets.v | | |-- Integers.v | | |-- Multiset.v | | |-- Partial_Order.v | | |-- Permut.v | | |-- Powerset_Classical_facts.v | | |-- Powerset_facts.v | | |-- Powerset.v | | |-- Relations_1_facts.v | | |-- Relations_1.v | | |-- Relations_2_facts.v | | |-- Relations_2.v | | |-- Relations_3_facts.v | | |-- Relations_3.v | | |-- Uniset.v | |-- Sorting | | |-- CPermutation.v | | |-- Heap.v | | |-- Mergesort.v | | |-- Permutation.v | | |-- PermutEq.v | | |-- PermutSetoid.v | | |-- Sorted.v | | |-- Sorting.v | |-- ssr | | |-- ssrbool.v | | |-- ssrclasses.v | | |-- ssreflect.v | | |-- ssrfun.v | | |-- ssrsetoid.v | | |-- ssrunder.v | |-- ssrmatching | | |-- ssrmatching.v | |-- ssrsearch | | |-- ssrsearch.v | |-- Strings | | |-- Ascii.v | | |-- BinaryString.v | | |-- Byte.v | | |-- ByteVector.v | | |-- HexString.v | | |-- OctalString.v | | |-- String.v | |-- Structures | | |-- DecidableTypeEx.v | | |-- DecidableType.v | | |-- EqualitiesFacts.v | | |-- Equalities.v | | |-- GenericMinMax.v | | |-- OrderedTypeAlt.v | | |-- OrderedTypeEx.v | | |-- OrderedType.v | | |-- OrdersAlt.v | | |-- OrdersEx.v | | |-- OrdersFacts.v | | |-- OrdersLists.v | | |-- OrdersTac.v | | |-- Orders.v | |-- Unicode | | |-- Utf8_core.v | | |-- Utf8.v | |-- Vectors | | |-- Fin.v | | |-- VectorDef.v | | |-- VectorEq.v | | |-- VectorSpec.v | | |-- Vector.v | |-- Wellfounded | | |-- Disjoint_Union.v | | |-- Inclusion.v | | |-- Inverse_Image.v | | |-- Lexicographic_Exponentiation.v | | |-- Lexicographic_Product.v | | |-- Transitive_Closure.v | | |-- Union.v | | |-- Wellfounded.v | | |-- Well_Ordering.v | |-- ZArith | |-- auxiliary.v | |-- BinIntDef.v | |-- BinInt.v | |-- Int.v | |-- Wf_Z.v | |-- Zabs.v | |-- ZArith_base.v | |-- ZArith_dec.v | |-- ZArith.v | |-- Zbool.v | |-- Zcompare.v | |-- Zcomplements.v | |-- Zdigits.v | |-- Zdiv.v | |-- Zeuclid.v | |-- Zeven.v | |-- Zgcd_alt.v | |-- Zhints.v | |-- Zmax.v | |-- Zminmax.v | |-- Zmin.v | |-- Zmisc.v | |-- Znat.v | |-- Znumtheory.v | |-- Zorder.v | |-- Zpow_alt.v | |-- Zpow_def.v | |-- Zpower.v | |-- Zpow_facts.v | |-- Zquot.v | |-- Zwf.v |-- tools | |-- beautify-archive | |-- coqdep_boot.ml | |-- coqdep_common.ml | |-- coqdep_common.mli | |-- coqdep_lexer.mli | |-- coqdep_lexer.mll | |-- coqdep.ml | |-- coqdoc | | |-- alpha.ml | | |-- alpha.mli | | |-- cdglobals.ml | | |-- cdglobals.mli | | |-- coqdoc.css | | |-- coqdoc.sty | | |-- cpretty.mli | | |-- cpretty.mll | | |-- dune | | |-- index.ml | | |-- index.mli | | |-- main.ml | | |-- output.ml | | |-- output.mli | | |-- style.css | | |-- tokens.ml | | |-- tokens.mli | |-- CoqMakefile.in | |-- coq_makefile.ml | |-- coq_tex.ml | |-- coqwc.mll | |-- coqworkmgr.ml | |-- dune | |-- make-both-single-timing-files.py | |-- make-both-time-files.py | |-- make-one-time-file.py | |-- md5sum.ml | |-- ocamllibdep.mll | |-- TimeFileMaker.py | |-- update-require |-- topbin | |-- coqc_bin.ml | |-- coqproofworker_bin.ml | |-- coqqueryworker_bin.ml | |-- coqtacticworker_bin.ml | |-- coqtop_bin.ml | |-- coqtop_byte_bin.ml | |-- dune |-- toplevel | |-- ccompile.ml | |-- ccompile.mli | |-- coqargs.ml | |-- coqargs.mli | |-- coqcargs.ml | |-- coqcargs.mli | |-- coqc.ml | |-- coqc.mli | |-- coqinit.ml | |-- coqinit.mli | |-- coqloop.ml | |-- coqloop.mli | |-- coqtop.ml | |-- coqtop.mli | |-- dune | |-- g_toplevel.mlg | |-- toplevel.mllib | |-- usage.ml | |-- usage.mli | |-- vernac.ml | |-- vernac.mli | |-- workerLoop.ml | |-- workerLoop.mli |-- user-contrib | |-- Ltac2 | |-- Array.v | |-- Bool.v | |-- Char.v | |-- Constr.v | |-- Control.v | |-- dune | |-- Env.v | |-- Fresh.v | |-- g_ltac2.mlg | |-- Ident.v | |-- Init.v | |-- Int.v | |-- List.v | |-- Ltac1.v | |-- ltac2_plugin.mlpack | |-- Ltac2.v | |-- Message.v | |-- Notations.v | |-- Option.v | |-- Pattern.v | |-- plugin_base.dune | |-- Std.v | |-- String.v | |-- tac2core.ml | |-- tac2core.mli | |-- tac2dyn.ml | |-- tac2dyn.mli | |-- tac2entries.ml | |-- tac2entries.mli | |-- tac2env.ml | |-- tac2env.mli | |-- tac2expr.mli | |-- tac2extffi.ml | |-- tac2extffi.mli | |-- tac2ffi.ml | |-- tac2ffi.mli | |-- tac2intern.ml | |-- tac2intern.mli | |-- tac2interp.ml | |-- tac2interp.mli | |-- tac2match.ml | |-- tac2match.mli | |-- tac2print.ml | |-- tac2print.mli | |-- tac2qexpr.mli | |-- tac2quote.ml | |-- tac2quote.mli | |-- tac2stdlib.ml | |-- tac2stdlib.mli | |-- tac2tactics.ml | |-- tac2tactics.mli | |-- tac2types.mli |-- vernac |-- assumptions.ml |-- assumptions.mli |-- attributes.ml |-- attributes.mli |-- auto_ind_decl.ml |-- auto_ind_decl.mli |-- canonical.ml |-- canonical.mli |-- classes.ml |-- classes.mli |-- comArguments.ml |-- comArguments.mli |-- comAssumption.ml |-- comAssumption.mli |-- comCoercion.ml |-- comCoercion.mli |-- comDefinition.ml |-- comDefinition.mli |-- comFixpoint.ml |-- comFixpoint.mli |-- comHints.ml |-- comHints.mli |-- comInductive.ml |-- comInductive.mli |-- comPrimitive.ml |-- comPrimitive.mli |-- comProgramFixpoint.ml |-- comProgramFixpoint.mli |-- comSearch.ml |-- comSearch.mli |-- declareDef.ml |-- declareInd.ml |-- declareInd.mli |-- declare.ml |-- declare.mli |-- declaremods.ml |-- declaremods.mli |-- declareObl.ml |-- declareObl.mli |-- declareUniv.ml |-- declareUniv.mli |-- doc.tex |-- dune |-- egramcoq.ml |-- egramcoq.mli |-- egramml.ml |-- egramml.mli |-- g_proofs.mlg |-- g_vernac.mlg |-- himsg.ml |-- himsg.mli |-- indschemes.ml |-- indschemes.mli |-- lemmas.ml |-- lemmas.mli |-- library.ml |-- library.mli |-- loadpath.ml |-- loadpath.mli |-- locality.ml |-- locality.mli |-- metasyntax.ml |-- metasyntax.mli |-- mltop.ml |-- mltop.mli |-- obligations.ml |-- obligations.mli |-- pfedit.ml |-- ppvernac.ml |-- ppvernac.mli |-- prettyp.ml |-- prettyp.mli |-- proof_global.ml |-- proof_using.ml |-- proof_using.mli |-- pvernac.ml |-- pvernac.mli |-- recLemmas.ml |-- recLemmas.mli |-- record.ml |-- record.mli |-- retrieveObl.ml |-- retrieveObl.mli |-- search.ml |-- search.mli |-- topfmt.ml |-- topfmt.mli |-- vernacentries.ml |-- vernacentries.mli |-- vernacexpr.ml |-- vernacextend.ml |-- vernacextend.mli |-- vernacinterp.ml |-- vernacinterp.mli |-- vernac.mllib |-- vernacprop.ml |-- vernacprop.mli |-- vernacstate.ml |-- vernacstate.mli 293 directories, 4411 files