diff --git a/.gitattributes b/.gitattributes index 6a0f88f21cc3f5ddec2179e4435d38f98499eb6d..1216d0b978eb24585c50d9a446bda77311c49f5d 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,3 +1,282 @@ +################ +# MERGE: union # +################ + Changelog merge=union -*.pdf binary +######################### +# HEADER_SPEC: CEA_LGPL # +######################### + +config* header_spec=CEA_LGPL + +makefile* header_spec=CEA_LGPL +Make* header_spec=CEA_LGPL +*.mk header_spec=CEA_LGPL + +*.c header_spec=CEA_LGPL +*.h header_spec=CEA_LGPL + +*.js header_spec=CEA_LGPL + +*.ml header_spec=CEA_LGPL +*.ml.in header_spec=CEA_LGPL +*.mli header_spec=CEA_LGPL +*.mli.in header_spec=CEA_LGPL +*.mll header_spec=CEA_LGPL +*.mly header_spec=CEA_LGPL + +*.pl header_spec=CEA_LGPL + +*.py header_spec=CEA_LGPL + +*.rc header_spec=CEA_LGPL + +*.sh header_spec=CEA_LGPL +*.zsh header_spec=CEA_LGPL + +*.css header_spec=CEA_LGPL + +*.ts header_spec=CEA_LGPL +*.tsx header_spec=CEA_LGPL + +/bin/frama-c* header_spec=CEA_LGPL + +/headers/headache_config.txt header_spec=CEA_LGPL +/share/autocomplete_frama-c header_spec=CEA_LGPL +/share/emacs/frama-c-*.el header_spec=CEA_LGPL +/share/_frama-c header_spec=CEA_LGPL + +/src/kernel_internals/runtime/fc_config.ml.in header_spec=CEA_LGPL +/src/libraries/stdlib/transitioning.ml.in header_spec=CEA_LGPL + +####################### +# HEADER_SPEC: others # +####################### + +/configure.in header_spec=CEA_INRIA_LGPL + +/doc/aorai/Makefile header_spec=AORAI_LGPL + +/share/analysis-scripts/flamegraph.pl header_spec=CDDL +/share/emacs/acsl.el header_spec=CEA_PR_LGPL +/share/machdep.c header_spec=CIL + +/src/kernel_internals/parsing/clexer.mli header_spec=CIL +/src/kernel_internals/parsing/clexer.mll header_spec=CIL +/src/kernel_internals/parsing/cparser.mly header_spec=CIL +/src/kernel_internals/parsing/errorloc.ml header_spec=CIL +/src/kernel_internals/parsing/errorloc.mli header_spec=CIL +/src/kernel_internals/parsing/lexerhack.ml header_spec=CIL +/src/kernel_internals/parsing/lexerhack.mli header_spec=CIL +/src/kernel_internals/parsing/logic_lexer.mli header_spec=CEA_INRIA_LGPL +/src/kernel_internals/parsing/logic_lexer.mll header_spec=CEA_INRIA_LGPL +/src/kernel_internals/parsing/logic_parser.mly header_spec=CEA_INRIA_LGPL +/src/kernel_internals/parsing/logic_preprocess.mli header_spec=CEA_INRIA_LGPL +/src/kernel_internals/parsing/logic_preprocess.mll header_spec=CEA_INRIA_LGPL +/src/kernel_internals/runtime/machdeps.ml header_spec=CIL +/src/kernel_internals/runtime/machdeps.mli header_spec=CIL +/src/kernel_internals/typing/alpha.ml header_spec=CIL +/src/kernel_internals/typing/alpha.mli header_spec=CIL +/src/kernel_internals/typing/cabs2cil.ml header_spec=CIL +/src/kernel_internals/typing/cabs2cil.mli header_spec=CIL +/src/kernel_internals/typing/cfg.ml header_spec=CIL +/src/kernel_internals/typing/cfg.mli header_spec=CIL +/src/kernel_internals/typing/frontc.ml header_spec=CIL +/src/kernel_internals/typing/frontc.mli header_spec=CIL +/src/kernel_internals/typing/logic_builtin.ml header_spec=CEA_INRIA_LGPL +/src/kernel_internals/typing/logic_builtin.mli header_spec=CEA_INRIA_LGPL +/src/kernel_internals/typing/mergecil.ml header_spec=CIL +/src/kernel_internals/typing/mergecil.mli header_spec=CIL +/src/kernel_internals/typing/oneret.ml header_spec=CIL +/src/kernel_internals/typing/oneret.mli header_spec=CIL +/src/kernel_internals/typing/rmtmps.ml header_spec=CIL +/src/kernel_internals/typing/rmtmps.mli header_spec=CIL +/src/kernel_internals/typing/translate_lightweight.ml header_spec=CEA_INRIA_LGPL +/src/kernel_internals/typing/translate_lightweight.mli header_spec=CEA_INRIA_LGPL +/src/kernel_services/analysis/dataflows.ml header_spec=CIL +/src/kernel_services/analysis/dataflows.mli header_spec=CIL +/src/kernel_services/ast_data/cil_types.mli header_spec=CIL +/src/kernel_services/ast_printing/cprint.ml header_spec=CIL +/src/kernel_services/ast_printing/cprint.mli header_spec=CIL +/src/kernel_services/ast_printing/logic_print.ml header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_printing/logic_print.mli header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/cil.ml header_spec=CIL +/src/kernel_services/ast_queries/cil.mli header_spec=CIL +/src/kernel_services/ast_queries/cil_builtins.ml header_spec=CIL +/src/kernel_services/ast_queries/cil_builtins.mli header_spec=CIL +/src/kernel_services/ast_queries/cil_const.ml header_spec=CIL +/src/kernel_services/ast_queries/cil_const.mli header_spec=CIL +/src/kernel_services/ast_queries/logic_const.ml header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/logic_const.mli header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/logic_env.ml header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/logic_env.mli header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/logic_typing.ml header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/logic_typing.mli header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/logic_utils.ml header_spec=CEA_INRIA_LGPL +/src/kernel_services/ast_queries/logic_utils.mli header_spec=CEA_INRIA_LGPL +/src/kernel_services/parsetree/cabs.mli header_spec=CIL +/src/kernel_services/parsetree/cabshelper.ml header_spec=CIL +/src/kernel_services/parsetree/cabshelper.mli header_spec=CIL +/src/kernel_services/parsetree/logic_ptree.mli header_spec=CEA_INRIA_LGPL +/src/kernel_services/visitors/cabsvisit.ml header_spec=CIL +/src/kernel_services/visitors/cabsvisit.mli header_spec=CIL +/src/kernel_services/visitors/visitor_behavior.ml header_spec=CEA_INRIA_LGPL +/src/kernel_services/visitors/visitor_behavior.mli header_spec=CEA_INRIA_LGPL + +/src/libraries/datatype/unmarshal.ml header_spec=INRIA_BSD +/src/libraries/datatype/unmarshal.mli header_spec=INRIA_BSD +/src/libraries/datatype/unmarshal_hashtbl_test.ml header_spec=INRIA_BSD +/src/libraries/datatype/unmarshal_test.ml header_spec=INRIA_BSD +/src/libraries/project/state_topological.ml header_spec=MODIFIED_OCAMLGRAPH +/src/libraries/project/state_topological.mli header_spec=MODIFIED_OCAMLGRAPH +/src/libraries/utils/cilconfig.ml header_spec=CIL +/src/libraries/utils/cilconfig.mli header_spec=CIL +/src/libraries/utils/escape.ml header_spec=CIL +/src/libraries/utils/escape.mli header_spec=CIL +/src/libraries/utils/hptmap.ml header_spec=MODIFIED_MENHIR +/src/libraries/utils/hptmap.mli header_spec=MODIFIED_MENHIR +/src/libraries/utils/hptmap_sig.mli header_spec=MODIFIED_MENHIR +/src/libraries/utils/rangemap.ml header_spec=OCAML_STDLIB +/src/libraries/utils/rangemap.mli header_spec=OCAML_STDLIB +/src/libraries/utils/utf8_logic.ml header_spec=CEA_INRIA_LGPL +/src/libraries/utils/utf8_logic.mli header_spec=CEA_INRIA_LGPL + +######################## +# HEADER_SPEC: .ignore # +######################## + +.gitattributes header_spec=.ignore +.gitignore header_spec=.ignore +.gitkeep header_spec=.ignore +.git-blame-ignore-revs header_spec=.ignore + +.merlin header_spec=.ignore + +Changelog header_spec=.ignore +opam header_spec=.ignore + +README* header_spec=.ignore +*.README* header_spec=.ignore + +*.dot header_spec=.ignore +*.fig header_spec=.ignore + +*.eps header_spec=.ignore +*.ps header_spec=.ignore + +*.gif header_spec=.ignore +*.ico header_spec=.ignore +*.jpg header_spec=.ignore +*.jpeg header_spec=.ignore +*.png header_spec=.ignore +*.svg header_spec=.ignore + +*.nix header_spec=.ignore +*.md header_spec=.ignore +*.opam header_spec=.ignore + +*.pdf header_spec=.ignore + +.tex header_spec=.ignore +*.sty header_spec=.ignore +*.bib header_spec=.ignore + +*.odoc header_spec=.ignore + +/.for_devel header_spec=.ignore +/.force-reconfigure header_spec=.ignore +/.gitlab-ci.yml header_spec=.ignore +/.make-clean* header_spec=.ignore +/.mailmap header_spec=.ignore +/.ocp-indent header_spec=.ignore +/ALL_VERSIONS header_spec=.ignore +/LICENSE header_spec=.ignore +/VERSION header_spec=.ignore +/VERSION_CODENAME header_spec=.ignore + +/bin/sed_get_* header_spec=.ignore + +/devel_tools/docker/*.template header_spec=.ignore + +# TODO: header_spec=JCF_LGPL_2_only +/devel_tools/size.mli header_spec=.ignore +/devel_tools/size.ml header_spec=.ignore +/devel_tools/size_states.ml header_spec=.ignore +/devel_tools/size_states.mli header_spec=.ignore + +/doc/CC-BY-SA-4.0 header_spec=.ignore +/doc/CHANGES.obfuscator header_spec=.ignore +/doc/LICENSE header_spec=.ignore +/doc/MakeLaTeXModern header_spec=.ignore +/doc/qualification/testing header_spec=.ignore +/doc/value/watchpoints header_spec=.ignore +/doc/scope/M.v header_spec=.ignore + +/doc/aorai/example/example* header_spec=.ignore +/doc/frama-c-book.* header_spec=.ignore +/doc/*.hva header_spec=.ignore + +/doc/acsl_tutorial_slides/script header_spec=.ignore +/doc/training/**/* header_spec=.ignore +/doc/value/examples/parametrizing/*.log header_spec=.ignore +/doc/*/**/Make* header_spec=.ignore +/doc/**/make* header_spec=.ignore +/doc/**/TODO header_spec=.ignore +/doc/**/*.bnf header_spec=.ignore +/doc/**/*.c header_spec=.ignore +/doc/**/*.graphml header_spec=.ignore +/doc/**/*.h header_spec=.ignore +/doc/**/*.htm header_spec=.ignore +/doc/**/*.html header_spec=.ignore +/doc/**/*.lua header_spec=.ignore +/doc/**/*.ml header_spec=.ignore +/doc/**/*.mli header_spec=.ignore +/doc/**/*.mll header_spec=.ignore +/doc/**/*.oracle header_spec=.ignore +/doc/**/*.tex header_spec=.ignore +/doc/**/*.txt header_spec=.ignore +/doc/**/*.sh header_spec=.ignore + +/headers/open-source/* header_spec=.ignore +/headers/close-source/* header_spec=.ignore + +/ivette/configure.js header_spec=.ignore +/ivette/sandboxer.js header_spec=.ignore +/ivette/.babelrc header_spec=.ignore +/ivette/.eslint* header_spec=.ignore +/ivette/doc/**/*.js header_spec=.ignore +/ivette/dome/doc/**/*.js header_spec=.ignore +/ivette/src/dome/doc/template/static/fonts/*-webfont.* header_spec=.ignore +/ivette/src/dome/template/git-ignore header_spec=.ignore +/ivette/src/dome/doc/template/tmpl/*.tmpl header_spec=.ignore +/ivette/src/dome/doc/**/*.js header_spec=.ignore +/ivette/src/dome/doc/**/*.htm header_spec=.ignore +/ivette/src/dome/doc/**/*.txt header_spec=.ignore +/ivette/src/dome/**/*.el header_spec=.ignore +/ivette/tests/*.i header_spec=.ignore +/ivette/**/*.css header_spec=.ignore +/ivette/**/*.html header_spec=.ignore +/ivette/**/*.json header_spec=.ignore +/ivette/**/*.lua header_spec=.ignore +/ivette/*.icns header_spec=.ignore +/ivette/*.lock header_spec=.ignore + +/licenses/* header_spec=.ignore + +/man/frama-c.1 header_spec=.ignore + +/nix/empty header_spec=.ignore +/nix/frama-c-public/known_hosts header_spec=.ignore + +/share/framac.vim header_spec=.ignore +/share/META.frama-c header_spec=.ignore +/share/libc/argz.h header_spec=.ignore +/share/libc/argz.c header_spec=.ignore +/share/analysis-scripts/readme-graph.graphml header_spec=.ignore +/share/analysis-scripts/pyproject.toml header_spec=.ignore +/share/win32_installer.iss header_spec=.ignore +/share/win32_manual_installation_step.txt header_spec=.ignore +/share/compliance/*.json header_spec=.ignore + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/aorai/.gitattributes b/src/plugins/aorai/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..94782b4119b1bf3cc8abf8b3a569b2e12580b692 --- /dev/null +++ b/src/plugins/aorai/.gitattributes @@ -0,0 +1,21 @@ +########################### +# HEADER_SPEC: AORAI_LGPL # +########################### + +/configure.ac header_spec=AORAI_LGPL + +/Makefile header_spec=AORAI_LGPL +/Makefile.in header_spec=AORAI_LGPL + +*.ml header_spec=AORAI_LGPL +*.mli header_spec=AORAI_LGPL +*.mll header_spec=AORAI_LGPL +*.mly header_spec=AORAI_LGPL + +######################## +# HEADER_SPEC: .ignore # +######################## + +/INSTALL header_spec=.ignore +/VERSIONS.txt header_spec=.ignore +/tests/**/* header_spec=.ignore diff --git a/src/plugins/dive/.gitattributes b/src/plugins/dive/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..619504ea1cada7d4c8799ae6f77973c401e68d7a --- /dev/null +++ b/src/plugins/dive/.gitattributes @@ -0,0 +1,5 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/e-acsl/.gitattributes b/src/plugins/e-acsl/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..a01dd065e962904b779606011014481e8f2e7e16 --- /dev/null +++ b/src/plugins/e-acsl/.gitattributes @@ -0,0 +1,66 @@ +############################################### +# HEADER_SPEC: CEA_LGPL_OR_PROPRIETARY.E_ACSL # +############################################### + +configure.ac header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + +Makefile header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +Makefile.in header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + +*.c header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +*.h header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + +*.ml header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +*.mli header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + +*.sh header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + +/man/e-acsl-gcc.sh.1 header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + +/scripts/e-acsl-gcc.sh.comp header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +/scripts/e-acsl-gcc.sh.comp header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + +######################## +# HEADER_SPEC: .ignore # +######################## + +README header_spec=.ignore + +/.clang-format header_spec=.ignore +/doc/Makefile.common header_spec=.ignore +/doc/support/MakeLaTeXModern header_spec=.ignore +/doc/doxygen/doxygen.cfg.in header_spec=.ignore +/doc/refman/*.tex header_spec=.ignore +/doc/userman/*.tex header_spec=.ignore + +/examples/demo/TODO header_spec=.ignore +/examples/ensuresec/push-alerts/.env-example header_spec=.ignore + +/headers/close-source/* header_spec=.ignore +/headers/open-source/* header_spec=.ignore + +/license/* header_spec=.ignore + +# Becarefull at the order with the previous lines +/contrib/**/*.c header_spec=.ignore + +/doc/**/Makefile header_spec=.ignore +/doc/**/*.ml header_spec=.ignore +/doc/**/*.mll header_spec=.ignore +/doc/**/*.c header_spec=.ignore +/doc/**/*.i header_spec=.ignore + +/examples/**/Makefile header_spec=.ignore +/examples/**/*.c header_spec=.ignore +/examples/**/*.i header_spec=.ignore +/examples/**/*.ml header_spec=.ignore +/examples/**/*.sh header_spec=.ignore +/examples/**/*.py header_spec=.ignore + +/tests/**/* header_spec=.ignore + +/tests/wrapper.sh header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +/tests/E_ACSL_test.ml header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +/contrib/libdlmalloc/dlmalloc.* header_spec=MODIFIED_DLMALLOC +/share/e-acsl/internals/e_acsl_rtl_io.* header_spec=MODIFIED_SPARETIMELABS + diff --git a/src/plugins/instantiate/.gitattributes b/src/plugins/instantiate/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..619504ea1cada7d4c8799ae6f77973c401e68d7a --- /dev/null +++ b/src/plugins/instantiate/.gitattributes @@ -0,0 +1,5 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/loop_analysis/.gitattributes b/src/plugins/loop_analysis/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..619504ea1cada7d4c8799ae6f77973c401e68d7a --- /dev/null +++ b/src/plugins/loop_analysis/.gitattributes @@ -0,0 +1,5 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/markdown-report/.gitattributes b/src/plugins/markdown-report/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..1bda6ba4ccda3594bd85d7c3fb18d658c0e7c179 --- /dev/null +++ b/src/plugins/markdown-report/.gitattributes @@ -0,0 +1,9 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/META.in header_spec=.ignore + +/share/acsl.xml header_spec=.ignore + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/nonterm/.gitattributes b/src/plugins/nonterm/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..619504ea1cada7d4c8799ae6f77973c401e68d7a --- /dev/null +++ b/src/plugins/nonterm/.gitattributes @@ -0,0 +1,5 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/qed/.gitattributes b/src/plugins/qed/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..dae65a33b405a5d049d491de7d2383f21cf79ae1 --- /dev/null +++ b/src/plugins/qed/.gitattributes @@ -0,0 +1,8 @@ +*.ml header_spec=CEA_WP +*.mli header_spec=CEA_WP +*.mll header_spec=CEA_WP + +configure.ac header_spec=CEA_WP + +Makefile header_spec=CEA_WP +Makefile.in header_spec=CEA_WP diff --git a/src/plugins/report/.gitattributes b/src/plugins/report/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..619504ea1cada7d4c8799ae6f77973c401e68d7a --- /dev/null +++ b/src/plugins/report/.gitattributes @@ -0,0 +1,5 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/server/.gitattributes b/src/plugins/server/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..619504ea1cada7d4c8799ae6f77973c401e68d7a --- /dev/null +++ b/src/plugins/server/.gitattributes @@ -0,0 +1,5 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/value/.gitattributes b/src/plugins/value/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..e62b79b9279d0dae86ee89c3782e8600365bb619 --- /dev/null +++ b/src/plugins/value/.gitattributes @@ -0,0 +1,6 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/Changelog_non_free header_spec=.ignore +/legacy/TOREMOVE header_spec=.ignore diff --git a/src/plugins/variadic/.gitattributes b/src/plugins/variadic/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..c513f54253ff2aefdbcdc977d2302111e7c2cc7e --- /dev/null +++ b/src/plugins/variadic/.gitattributes @@ -0,0 +1,7 @@ +######################## +# HEADER_SPEC: .ignore # +######################## + +/todo.txt header_spec=.ignore + +/tests/**/* header_spec=.ignore diff --git a/src/plugins/wp/.gitattributes b/src/plugins/wp/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..cd25ae10f5e3a0c05c7766f01fc32d3d870346fe --- /dev/null +++ b/src/plugins/wp/.gitattributes @@ -0,0 +1,65 @@ +####################### +# HEADER_SPEC: CEA_WP # +####################### + +*.ml header_spec=CEA_WP +*.mli header_spec=CEA_WP +*.mll header_spec=CEA_WP + +*.mlw header_spec=CEA_WP +*.driver header_spec=CEA_WP +*.v header_spec=CEA_WP +*.css header_spec=CEA_WP + +configure.ac header_spec=CEA_WP + +Makefile header_spec=CEA_WP +Makefile.in header_spec=CEA_WP +Makefile.resources header_spec=CEA_WP +MakeDoc header_spec=CEA_WP + +####################### +# HEADER_SPEC: others # +####################### + +/doc/coqdoc/coq2tex/*.mll header_spec=XL_COMPCERT + +/share/coqwp/BuiltIn.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/HighOrd.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/bool/Bool.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/int/Abs.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/int/ComputerDivision.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/int/EuclideanDivision.v header_spec=MODIFIED_WHY3 +/share/coqwp/int/Exponentiation.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/int/Int.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/int/MinMax.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/int/Power.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/int/ComputerOfEuclideanDivision.v header_spec=MODIFIED_WHY3 +/share/coqwp/map/Map.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/map/Const.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/Abs.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/FromInt.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/ExpLog.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/MinMax.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/PowerReal.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/Real.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/RealInfix.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/Square.v header_spec=UNMODIFIED_WHY3 +/share/coqwp/real/Trigonometry.v header_spec=UNMODIFIED_WHY3 + +######################## +# HEADER_SPEC: .ignore # +######################## + +/intro_wp.txt header_spec=.ignore + +/doc/coqdoc/coq2tex/coq2html.js header_spec=.ignore +/doc/coqdoc/coq2tex/*.css header_spec=.ignore +/doc/coqdoc/coq2tex/*.html header_spec=.ignore +/doc/coqdoc/*.tex header_spec=.ignore + +/doc/manual/nullable.c header_spec=.ignore +/doc/manual/*.tex header_spec=.ignore + + +/tests/**/* header_spec=.ignore