From a99776e10e0b2198d2b811ad82631111fb450f8a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 18 Mar 2020 12:14:26 +0100 Subject: Update headers in the whole code base. Add headers to a few files which were missing them. --- plugins/btauto/g_btauto.mlg | 4 ++-- plugins/btauto/refl_btauto.ml | 4 ++-- plugins/btauto/refl_btauto.mli | 4 ++-- plugins/cc/ccalgo.ml | 4 ++-- plugins/cc/ccalgo.mli | 4 ++-- plugins/cc/ccproof.ml | 4 ++-- plugins/cc/ccproof.mli | 4 ++-- plugins/cc/cctac.ml | 4 ++-- plugins/cc/cctac.mli | 4 ++-- plugins/cc/g_congruence.mlg | 4 ++-- plugins/derive/derive.ml | 4 ++-- plugins/derive/derive.mli | 4 ++-- plugins/derive/g_derive.mlg | 4 ++-- plugins/extraction/big.ml | 4 ++-- plugins/extraction/common.ml | 4 ++-- plugins/extraction/common.mli | 4 ++-- plugins/extraction/extract_env.ml | 4 ++-- plugins/extraction/extract_env.mli | 4 ++-- plugins/extraction/extraction.ml | 4 ++-- plugins/extraction/extraction.mli | 4 ++-- plugins/extraction/g_extraction.mlg | 4 ++-- plugins/extraction/haskell.ml | 4 ++-- plugins/extraction/haskell.mli | 4 ++-- plugins/extraction/miniml.ml | 4 ++-- plugins/extraction/miniml.mli | 4 ++-- plugins/extraction/mlutil.ml | 4 ++-- plugins/extraction/mlutil.mli | 4 ++-- plugins/extraction/modutil.ml | 4 ++-- plugins/extraction/modutil.mli | 4 ++-- plugins/extraction/ocaml.ml | 4 ++-- plugins/extraction/ocaml.mli | 4 ++-- plugins/extraction/scheme.ml | 4 ++-- plugins/extraction/scheme.mli | 4 ++-- plugins/extraction/table.ml | 4 ++-- plugins/extraction/table.mli | 4 ++-- plugins/firstorder/formula.ml | 4 ++-- plugins/firstorder/formula.mli | 4 ++-- plugins/firstorder/g_ground.mlg | 4 ++-- plugins/firstorder/ground.ml | 4 ++-- plugins/firstorder/ground.mli | 4 ++-- plugins/firstorder/instances.ml | 4 ++-- plugins/firstorder/instances.mli | 4 ++-- plugins/firstorder/rules.ml | 4 ++-- plugins/firstorder/rules.mli | 4 ++-- plugins/firstorder/sequent.ml | 4 ++-- plugins/firstorder/sequent.mli | 4 ++-- plugins/firstorder/unify.ml | 4 ++-- plugins/firstorder/unify.mli | 4 ++-- plugins/funind/functional_principles_types.ml | 4 ++-- plugins/funind/functional_principles_types.mli | 4 ++-- plugins/funind/g_indfun.mlg | 4 ++-- plugins/funind/gen_principle.ml | 4 ++-- plugins/funind/gen_principle.mli | 4 ++-- plugins/funind/glob_termops.ml | 4 ++-- plugins/funind/glob_termops.mli | 4 ++-- plugins/funind/indfun.ml | 4 ++-- plugins/funind/indfun.mli | 4 ++-- plugins/funind/invfun.ml | 4 ++-- plugins/funind/invfun.mli | 4 ++-- plugins/funind/recdef.ml | 4 ++-- plugins/ltac/coretactics.mlg | 4 ++-- plugins/ltac/evar_tactics.ml | 4 ++-- plugins/ltac/evar_tactics.mli | 4 ++-- plugins/ltac/extraargs.mlg | 4 ++-- plugins/ltac/extraargs.mli | 4 ++-- plugins/ltac/extratactics.mlg | 4 ++-- plugins/ltac/extratactics.mli | 4 ++-- plugins/ltac/g_auto.mlg | 4 ++-- plugins/ltac/g_class.mlg | 4 ++-- plugins/ltac/g_eqdecide.mlg | 4 ++-- plugins/ltac/g_ltac.mlg | 4 ++-- plugins/ltac/g_obligations.mlg | 4 ++-- plugins/ltac/g_rewrite.mlg | 4 ++-- plugins/ltac/g_tactic.mlg | 4 ++-- plugins/ltac/pltac.ml | 4 ++-- plugins/ltac/pltac.mli | 4 ++-- plugins/ltac/pptactic.ml | 4 ++-- plugins/ltac/pptactic.mli | 4 ++-- plugins/ltac/profile_ltac.ml | 4 ++-- plugins/ltac/profile_ltac.mli | 4 ++-- plugins/ltac/profile_ltac_tactics.mlg | 4 ++-- plugins/ltac/rewrite.ml | 4 ++-- plugins/ltac/rewrite.mli | 4 ++-- plugins/ltac/tacarg.ml | 4 ++-- plugins/ltac/tacarg.mli | 4 ++-- plugins/ltac/taccoerce.ml | 4 ++-- plugins/ltac/taccoerce.mli | 4 ++-- plugins/ltac/tacentries.ml | 4 ++-- plugins/ltac/tacentries.mli | 4 ++-- plugins/ltac/tacenv.ml | 4 ++-- plugins/ltac/tacenv.mli | 4 ++-- plugins/ltac/tacexpr.ml | 4 ++-- plugins/ltac/tacexpr.mli | 4 ++-- plugins/ltac/tacintern.ml | 4 ++-- plugins/ltac/tacintern.mli | 4 ++-- plugins/ltac/tacinterp.ml | 4 ++-- plugins/ltac/tacinterp.mli | 4 ++-- plugins/ltac/tacsubst.ml | 4 ++-- plugins/ltac/tacsubst.mli | 4 ++-- plugins/ltac/tactic_debug.ml | 4 ++-- plugins/ltac/tactic_debug.mli | 4 ++-- plugins/ltac/tactic_matching.ml | 4 ++-- plugins/ltac/tactic_matching.mli | 4 ++-- plugins/ltac/tactic_option.ml | 4 ++-- plugins/ltac/tactic_option.mli | 4 ++-- plugins/ltac/tauto.ml | 4 ++-- plugins/micromega/certificate.ml | 4 ++-- plugins/micromega/certificate.mli | 4 ++-- plugins/micromega/coq_micromega.ml | 4 ++-- plugins/micromega/coq_micromega.mli | 4 ++-- plugins/micromega/csdpcert.ml | 4 ++-- plugins/micromega/csdpcert.mli | 4 ++-- plugins/micromega/g_micromega.mlg | 4 ++-- plugins/micromega/g_micromega.mli | 4 ++-- plugins/micromega/g_zify.mlg | 4 ++-- plugins/micromega/itv.ml | 4 ++-- plugins/micromega/itv.mli | 4 ++-- plugins/micromega/mfourier.ml | 4 ++-- plugins/micromega/mfourier.mli | 4 ++-- plugins/micromega/mutils.ml | 4 ++-- plugins/micromega/mutils.mli | 4 ++-- plugins/micromega/numCompat.ml | 4 ++-- plugins/micromega/numCompat.mli | 4 ++-- plugins/micromega/persistent_cache.ml | 4 ++-- plugins/micromega/persistent_cache.mli | 4 ++-- plugins/micromega/polynomial.ml | 4 ++-- plugins/micromega/polynomial.mli | 4 ++-- plugins/micromega/simplex.ml | 4 ++-- plugins/micromega/simplex.mli | 4 ++-- plugins/micromega/sos.mli | 4 ++-- plugins/micromega/sos_lib.mli | 4 ++-- plugins/micromega/sos_types.ml | 4 ++-- plugins/micromega/sos_types.mli | 4 ++-- plugins/micromega/vect.ml | 4 ++-- plugins/micromega/vect.mli | 4 ++-- plugins/micromega/zify.ml | 4 ++-- plugins/micromega/zify.mli | 4 ++-- plugins/nsatz/g_nsatz.mlg | 4 ++-- plugins/nsatz/ideal.ml | 4 ++-- plugins/nsatz/ideal.mli | 4 ++-- plugins/nsatz/nsatz.ml | 4 ++-- plugins/nsatz/nsatz.mli | 4 ++-- plugins/nsatz/polynom.ml | 4 ++-- plugins/nsatz/polynom.mli | 4 ++-- plugins/omega/coq_omega.ml | 4 ++-- plugins/omega/coq_omega.mli | 4 ++-- plugins/omega/g_omega.mlg | 4 ++-- plugins/omega/omega.ml | 4 ++-- plugins/rtauto/g_rtauto.mlg | 4 ++-- plugins/rtauto/proof_search.ml | 4 ++-- plugins/rtauto/proof_search.mli | 4 ++-- plugins/rtauto/refl_tauto.ml | 4 ++-- plugins/rtauto/refl_tauto.mli | 4 ++-- plugins/setoid_ring/g_newring.mlg | 4 ++-- plugins/setoid_ring/newring.ml | 4 ++-- plugins/setoid_ring/newring.mli | 4 ++-- plugins/setoid_ring/newring_ast.ml | 4 ++-- plugins/setoid_ring/newring_ast.mli | 4 ++-- plugins/ssr/ssrast.mli | 4 ++-- plugins/ssr/ssrbwd.ml | 4 ++-- plugins/ssr/ssrbwd.mli | 4 ++-- plugins/ssr/ssrcommon.ml | 4 ++-- plugins/ssr/ssrcommon.mli | 4 ++-- plugins/ssr/ssrelim.ml | 4 ++-- plugins/ssr/ssrelim.mli | 4 ++-- plugins/ssr/ssrequality.ml | 4 ++-- plugins/ssr/ssrequality.mli | 4 ++-- plugins/ssr/ssrfwd.ml | 4 ++-- plugins/ssr/ssrfwd.mli | 4 ++-- plugins/ssr/ssripats.ml | 4 ++-- plugins/ssr/ssripats.mli | 4 ++-- plugins/ssr/ssrparser.mlg | 4 ++-- plugins/ssr/ssrparser.mli | 4 ++-- plugins/ssr/ssrprinters.ml | 4 ++-- plugins/ssr/ssrprinters.mli | 4 ++-- plugins/ssr/ssrtacticals.ml | 4 ++-- plugins/ssr/ssrtacticals.mli | 4 ++-- plugins/ssr/ssrvernac.mlg | 4 ++-- plugins/ssr/ssrvernac.mli | 4 ++-- plugins/ssr/ssrview.ml | 4 ++-- plugins/ssr/ssrview.mli | 4 ++-- plugins/ssrmatching/g_ssrmatching.mlg | 4 ++-- plugins/ssrmatching/g_ssrmatching.mli | 4 ++-- plugins/ssrmatching/ssrmatching.ml | 4 ++-- plugins/ssrmatching/ssrmatching.mli | 4 ++-- plugins/syntax/float_syntax.ml | 10 ++++++---- plugins/syntax/g_numeral.mlg | 4 ++-- plugins/syntax/g_string.mlg | 4 ++-- plugins/syntax/int63_syntax.ml | 4 ++-- plugins/syntax/numeral.ml | 4 ++-- plugins/syntax/numeral.mli | 4 ++-- plugins/syntax/r_syntax.ml | 4 ++-- plugins/syntax/r_syntax.mli | 4 ++-- plugins/syntax/string_notation.ml | 4 ++-- plugins/syntax/string_notation.mli | 4 ++-- 195 files changed, 394 insertions(+), 392 deletions(-) (limited to 'plugins') diff --git a/plugins/btauto/g_btauto.mlg b/plugins/btauto/g_btauto.mlg index cbed6e7b96..8baf01551a 100644 --- a/plugins/btauto/g_btauto.mlg +++ b/plugins/btauto/g_btauto.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(*