From a44e01fee79da51f5492bb9e70fa7107114bd4de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 22 Aug 2019 15:03:08 +0200
Subject: [PATCH] [wp] cleanup strange headers

---
 headers/header_spec.txt | 33 ---------------------------------
 1 file changed, 33 deletions(-)

diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 2c9b7f0cead..4171ba9c84f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1434,10 +1434,6 @@ src/plugins/wp/ProofScript.ml: CEA_WP
 src/plugins/wp/ProofScript.mli: CEA_WP
 src/plugins/wp/ProverCoq.ml: CEA_WP
 src/plugins/wp/ProverCoq.mli: CEA_WP
-src/plugins/wp/ProverDetect.ml: CEA_WP
-src/plugins/wp/ProverDetect.mli: CEA_WP
-src/plugins/wp/ProverDetect.Why3.ml: CEA_WP
-src/plugins/wp/ProverDetect.None.ml: CEA_WP
 src/plugins/wp/ProverErgo.ml: CEA_WP
 src/plugins/wp/ProverErgo.mli: CEA_WP
 src/plugins/wp/ProverScript.ml: CEA_WP
@@ -1448,8 +1444,6 @@ src/plugins/wp/ProverTask.ml: CEA_WP
 src/plugins/wp/ProverTask.mli: CEA_WP
 src/plugins/wp/ProverWhy3.ml: CEA_WP
 src/plugins/wp/ProverWhy3.mli: CEA_WP
-src/plugins/wp/ProverWhy3ide.ml: CEA_WP
-src/plugins/wp/ProverWhy3ide.mli: CEA_WP
 src/plugins/wp/REVISION: .ignore
 src/plugins/wp/RefUsage.ml: CEA_WP
 src/plugins/wp/RefUsage.mli: CEA_WP
@@ -1880,13 +1874,7 @@ src/plugins/wp/share/ergo/real.Square.mlw: MODIFIED_WHY3
 src/plugins/wp/share/ergo/real.Trigonometry.mlw: MODIFIED_WHY3
 src/plugins/wp/share/ergo/real.Truncate.mlw: MODIFIED_WHY3
 src/plugins/wp/share/install.ml: CEA_WP
-src/plugins/wp/share/src/.gitignore: .ignore
-src/plugins/wp/share/src/.merlin: .ignore
-src/plugins/wp/share/src/Bits.v: CEA_WP
-src/plugins/wp/share/src/BuiltIn/bool.mlw: CEA_WP
 src/plugins/wp/share/src/Cbits.v: .ignore
-src/plugins/wp/share/src/Cfloat.v: .ignore
-src/plugins/wp/share/src/Cint.v: .ignore
 src/plugins/wp/share/src/Cmath.v: .ignore
 src/plugins/wp/share/src/Makefile: CEA_WP
 src/plugins/wp/share/src/Memory.v: .ignore
@@ -1894,26 +1882,9 @@ src/plugins/wp/share/src/Qed.v: .ignore
 src/plugins/wp/share/src/Qedlib.v: CEA_WP
 src/plugins/wp/share/src/Vlist.v: .ignore
 src/plugins/wp/share/src/Vset.v: .ignore
-src/plugins/wp/share/src/Zbits.v: CEA_WP
-src/plugins/wp/share/src/alt_ergo_realize.ml: MODIFIED_WHY3
 src/plugins/wp/share/src/alt_ergo_why3_stdlib.drv: CEA_WP
-src/plugins/wp/share/src/cbits.why: CEA_WP
-src/plugins/wp/share/src/cfloat.why: CEA_WP
-src/plugins/wp/share/src/cint.why: CEA_WP
-src/plugins/wp/share/src/cmath.why: CEA_WP
 src/plugins/wp/share/src/coq-own-realization.drv: CEA_PROPRIETARY
 src/plugins/wp/share/src/filter_axioms.ml: CEA_WP
-src/plugins/wp/share/src/lemma_about_mod.txt: .ignore
-src/plugins/wp/share/src/memory.why: CEA_WP
-src/plugins/wp/share/src/qed.why: CEA_WP
-src/plugins/wp/share/src/realization.conf: .ignore
-src/plugins/wp/share/src/tests/import.why: .ignore
-src/plugins/wp/share/src/tests/import/import_T_G_1.v: .ignore
-src/plugins/wp/share/src/tests/import/why3session.xml: .ignore
-src/plugins/wp/share/src/upper.ml: .ignore
-src/plugins/wp/share/src/vlist.why: CEA_WP
-src/plugins/wp/share/src/vset.why: CEA_WP
-src/plugins/wp/share/src/why3-realize.drv: .ignore
 src/plugins/wp/share/why3/ArcTrigo.v: CEA_WP
 src/plugins/wp/share/why3/ArcTrigo.why: CEA_WP
 src/plugins/wp/share/why3/Bits.v: CEA_WP
@@ -1924,22 +1895,18 @@ src/plugins/wp/share/why3/Cfloat.why: CEA_WP
 src/plugins/wp/share/why3/Cint.v: CEA_WP
 src/plugins/wp/share/why3/Cint.why: CEA_WP
 src/plugins/wp/share/why3/Cmath.v: CEA_WP
-src/plugins/wp/share/why3/Cmath.why: CEA_WP
 src/plugins/wp/share/why3/ExpLog.v: CEA_WP
-src/plugins/wp/share/why3/ExpLog.why: CEA_WP
 src/plugins/wp/share/why3/Memory.v: CEA_WP
 src/plugins/wp/share/why3/Memory.why: CEA_WP
 src/plugins/wp/share/why3/Qed.v: CEA_WP
 src/plugins/wp/share/why3/Qed.why: CEA_WP
 src/plugins/wp/share/why3/Qedlib.v: CEA_WP
 src/plugins/wp/share/why3/Square.v: CEA_WP
-src/plugins/wp/share/why3/Square.why: CEA_WP
 src/plugins/wp/share/why3/Vlist.v: CEA_WP
 src/plugins/wp/share/why3/Vlist.why: CEA_WP
 src/plugins/wp/share/why3/Vset.v: CEA_WP
 src/plugins/wp/share/why3/Vset.why: CEA_WP
 src/plugins/wp/share/why3/Zbits.v: CEA_WP
-src/plugins/wp/share/why3/coq.drv: CEA_WP
 src/plugins/wp/share/why3/frama_c_wp/cbits.mlw: CEA_WP
 src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw: CEA_WP
 src/plugins/wp/share/why3/frama_c_wp/cint.mlw: CEA_WP
-- 
GitLab