From f87695472e70c313ef2966e20979b1afcc2e543e Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 29 Mar 2022 10:01:08 +0200 Subject: [PATCH] License change: CeCILL B/C -> MIT --- AUTHORS | 27 +++ COPYRIGHT | 15 -- COPYRIGHT.yaml | 29 --- LICENSE | 24 +++ Makefile | 8 +- examples/Pedersen.ec | 6 - examples/SchnorrPK.ec | 6 - examples/Upto.ec | 7 - examples/vonNeumann.eca | 7 - scripts/srctx/license | 219 ----------------------- src/ec.ml | 8 - src/ecAlgTactic.ml | 8 - src/ecAlgTactic.mli | 8 - src/ecAlgebra.ml | 8 - src/ecAlgebra.mli | 8 - src/ecBaseLogic.ml | 8 - src/ecBigInt.ml | 8 - src/ecBigInt.mli | 8 - src/ecBigIntCore.ml | 8 - src/ecCHoare.ml | 9 - src/ecCallbyValue.ml | 8 - src/ecCallbyValue.mli | 8 - src/ecCommands.ml | 8 - src/ecCommands.mli | 8 - src/ecCoreFol.ml | 8 - src/ecCoreFol.mli | 8 - src/ecCoreGoal.ml | 8 - src/ecCoreGoal.mli | 8 - src/ecCoreHiPhl.ml | 8 - src/ecCoreHiPhl.mli | 8 - src/ecCoreLib.ml | 8 - src/ecCoreLib.mli | 8 - src/ecCoreModules.ml | 8 - src/ecCoreModules.mli | 8 - src/ecDecl.ml | 8 - src/ecDecl.mli | 8 - src/ecEco.ml | 8 - src/ecEnv.ml | 8 - src/ecEnv.mli | 8 - src/ecField.ml | 18 -- src/ecField.mli | 8 - src/ecFol.ml | 8 - src/ecFol.mli | 8 - src/ecGState.ml | 8 - src/ecGState.mli | 8 - src/ecGenRegexp.ml | 8 - src/ecHiGoal.ml | 8 - src/ecHiGoal.mli | 8 - src/ecHiInductive.ml | 8 - src/ecHiInductive.mli | 8 - src/ecHiNotations.ml | 8 - src/ecHiNotations.mli | 8 - src/ecHiPredicates.ml | 8 - src/ecHiPredicates.mli | 8 - src/ecHiTacticals.ml | 8 - src/ecHiTacticals.mli | 8 - src/ecIdent.ml | 8 - src/ecIdent.mli | 8 - src/ecInductive.ml | 8 - src/ecInductive.mli | 8 - src/ecIo.ml | 8 - src/ecIo.mli | 8 - src/ecLexer.mll | 8 - src/ecLoader.ml | 8 - src/ecLoader.mli | 8 - src/ecLocation.ml | 8 - src/ecLocation.mli | 8 - src/ecLowGoal.ml | 8 - src/ecLowGoal.mli | 8 - src/ecLowPhlGoal.ml | 8 - src/ecMaps.ml | 8 - src/ecMatching.ml | 8 - src/ecMatching.mli | 8 - src/ecMemory.ml | 8 - src/ecMemory.mli | 8 - src/ecModules.ml | 8 - src/ecModules.mli | 8 - src/ecOptions.ml | 8 - src/ecOptions.mli | 8 - src/ecPException.ml | 8 - src/ecPException.mli | 8 - src/ecPV.ml | 8 - src/ecPV.mli | 8 - src/ecParser.mly | 8 - src/ecParsetree.ml | 8 - src/ecPath.ml | 8 - src/ecPath.mli | 8 - src/ecPrinting.ml | 8 - src/ecPrinting.mli | 8 - src/ecProofTerm.ml | 8 - src/ecProofTerm.mli | 8 - src/ecProofTyping.ml | 8 - src/ecProofTyping.mli | 8 - src/ecProvers.ml | 8 - src/ecProvers.mli | 8 - src/ecReduction.ml | 8 - src/ecReduction.mli | 8 - src/ecRegexp.ml | 8 - src/ecRegexp.mli | 8 - src/ecRing.ml | 18 -- src/ecRing.mli | 8 - src/ecScope.ml | 8 - src/ecScope.mli | 8 - src/ecSearch.ml | 8 - src/ecSearch.mli | 8 - src/ecSection.ml | 8 - src/ecSection.mli | 8 - src/ecSmt.ml | 8 - src/ecSmt.mli | 8 - src/ecStrongRing.ml | 8 - src/ecSubst.ml | 8 - src/ecSubst.mli | 8 - src/ecSymbols.ml | 8 - src/ecSymbols.mli | 8 - src/ecTerminal.ml | 8 - src/ecTerminal.mli | 8 - src/ecThCloning.ml | 8 - src/ecThCloning.mli | 8 - src/ecTheory.ml | 8 - src/ecTheory.mli | 8 - src/ecTheoryReplay.ml | 8 - src/ecTheoryReplay.mli | 8 - src/ecTransMatching.ml | 8 - src/ecTransMatching.mli | 8 - src/ecTypeClass.ml | 8 - src/ecTypeClass.mli | 8 - src/ecTypes.ml | 8 - src/ecTypes.mli | 8 - src/ecTyping.ml | 8 - src/ecTyping.mli | 8 - src/ecUFind.ml | 8 - src/ecUFind.mli | 8 - src/ecUid.ml | 8 - src/ecUid.mli | 8 - src/ecUnify.ml | 8 - src/ecUnify.mli | 8 - src/ecUserMessages.ml | 8 - src/ecUserMessages.mli | 8 - src/ecUtils.ml | 8 - src/ecUtils.mli | 8 - src/ecVersion.ml | 15 +- src/ecVersion.mli | 8 - src/ecWhy3Conv.ml | 8 - src/ecWhy3Conv.mli | 8 - src/phl/ecPhlApp.ml | 8 - src/phl/ecPhlApp.mli | 8 - src/phl/ecPhlAuto.ml | 8 - src/phl/ecPhlAuto.mli | 8 - src/phl/ecPhlBdHoare.ml | 8 - src/phl/ecPhlBdHoare.mli | 8 - src/phl/ecPhlCall.ml | 8 - src/phl/ecPhlCall.mli | 8 - src/phl/ecPhlCase.ml | 8 - src/phl/ecPhlCase.mli | 8 - src/phl/ecPhlCodeTx.ml | 8 - src/phl/ecPhlCodeTx.mli | 8 - src/phl/ecPhlCond.ml | 8 - src/phl/ecPhlCond.mli | 8 - src/phl/ecPhlConseq.ml | 8 - src/phl/ecPhlConseq.mli | 8 - src/phl/ecPhlCoreView.ml | 8 - src/phl/ecPhlCoreView.mli | 8 - src/phl/ecPhlDeno.ml | 8 - src/phl/ecPhlDeno.mli | 8 - src/phl/ecPhlEager.ml | 8 - src/phl/ecPhlEager.mli | 8 - src/phl/ecPhlEqobs.ml | 8 - src/phl/ecPhlEqobs.mli | 8 - src/phl/ecPhlExists.ml | 8 - src/phl/ecPhlExists.mli | 8 - src/phl/ecPhlFel.ml | 8 - src/phl/ecPhlFel.mli | 8 - src/phl/ecPhlFun.ml | 8 - src/phl/ecPhlFun.mli | 8 - src/phl/ecPhlHiAuto.ml | 8 - src/phl/ecPhlHiAuto.mli | 8 - src/phl/ecPhlHiBdHoare.ml | 8 - src/phl/ecPhlHiBdHoare.mli | 8 - src/phl/ecPhlHiCond.ml | 8 - src/phl/ecPhlHiCond.mli | 8 - src/phl/ecPhlInline.ml | 8 - src/phl/ecPhlInline.mli | 8 - src/phl/ecPhlLoopTx.ml | 8 - src/phl/ecPhlLoopTx.mli | 8 - src/phl/ecPhlPr.ml | 8 - src/phl/ecPhlPr.mli | 8 - src/phl/ecPhlPrRw.ml | 8 - src/phl/ecPhlPrRw.mli | 8 - src/phl/ecPhlRCond.ml | 8 - src/phl/ecPhlRCond.mli | 8 - src/phl/ecPhlRnd.ml | 8 - src/phl/ecPhlRnd.mli | 8 - src/phl/ecPhlSkip.ml | 8 - src/phl/ecPhlSkip.mli | 8 - src/phl/ecPhlSp.ml | 8 - src/phl/ecPhlSp.mli | 8 - src/phl/ecPhlSwap.ml | 8 - src/phl/ecPhlSwap.mli | 8 - src/phl/ecPhlSym.ml | 8 - src/phl/ecPhlSym.mli | 8 - src/phl/ecPhlTAuto.ml | 8 - src/phl/ecPhlTAuto.mli | 8 - src/phl/ecPhlTrans.ml | 8 - src/phl/ecPhlTrans.mli | 8 - src/phl/ecPhlWhile.ml | 8 - src/phl/ecPhlWhile.mli | 8 - src/phl/ecPhlWp.ml | 8 - src/phl/ecPhlWp.mli | 8 - src/system/XDG.ml | 8 - src/system/XDG.mli | 8 - theories/algebra/Bigalg.ec | 8 - theories/algebra/Bigop.eca | 8 - theories/algebra/Binomial.ec | 8 - theories/algebra/Group.ec | 8 - theories/algebra/Ideal.ec | 8 - theories/algebra/IntDiv.ec | 8 - theories/algebra/Matrix.eca | 8 - theories/algebra/Monoid.eca | 8 - theories/algebra/Number.ec | 8 - theories/algebra/Perms.ec | 8 - theories/algebra/Poly.ec | 8 - theories/algebra/Ring.ec | 8 - theories/algebra/StdBigop.ec | 8 - theories/algebra/StdOrder.ec | 8 - theories/algebra/StdRing.ec | 8 - theories/algebra/ZModP.ec | 8 - theories/analysis/RealExp.ec | 8 - theories/analysis/RealFLub.ec | 8 - theories/analysis/RealFun.ec | 8 - theories/analysis/RealLub.ec | 8 - theories/analysis/RealSeq.ec | 8 - theories/analysis/RealSeries.ec | 8 - theories/core/AllCore.ec | 8 - theories/core/Bool.ec | 8 - theories/core/Core.ec | 8 - theories/core/CoreInt.ec | 8 - theories/core/CoreMap.ec | 8 - theories/core/CoreReal.ec | 8 - theories/crypto/AdvAbsVal.ec | 8 - theories/crypto/Birthday.ec | 8 - theories/crypto/Commitment.ec | 6 - theories/crypto/DLog.ec | 6 - theories/crypto/DiffieHellman.ec | 8 - theories/crypto/LorR.eca | 8 - theories/crypto/MAC.ec | 8 - theories/crypto/OW.ec | 8 - theories/crypto/PKE.ec | 8 - theories/crypto/PKS.ec | 8 - theories/crypto/PRF.eca | 8 - theories/crypto/PRG.eca | 8 - theories/crypto/PROM.ec | 8 - theories/crypto/PRP.eca | 8 - theories/crypto/ROM.eca | 8 - theories/crypto/RndExcept.eca | 8 - theories/crypto/SecureChannels.ec | 8 - theories/crypto/SigmaProtocol.ec | 6 - theories/crypto/SplitRO.ec | 8 - theories/crypto/SymmetricEncryption.ec | 8 - theories/crypto/assumptions/AEAD.ec | 8 - theories/crypto/assumptions/CRHash.ec | 8 - theories/crypto/assumptions/DHIES.ec | 8 - theories/crypto/assumptions/MRPKE.ec | 8 - theories/crypto/assumptions/ODH.ec | 8 - theories/crypto/assumptions/PKSMK.ec | 8 - theories/crypto/pke/PKE_CPA.eca | 8 - theories/crypto/prp_prf/Strong_RP_RF.eca | 8 - theories/crypto/ske/CCA.eca | 8 - theories/crypto/ske/CCA1.eca | 8 - theories/crypto/ske/CPA.eca | 8 - theories/crypto/ske/NewSKE.eca | 8 - theories/datatypes/Array.ec | 8 - theories/datatypes/BitEncoding.ec | 8 - theories/datatypes/BitWord.eca | 8 - theories/datatypes/FSet.ec | 8 - theories/datatypes/FloorCeil.ec | 8 - theories/datatypes/Int.ec | 8 - theories/datatypes/IntMin.ec | 8 - theories/datatypes/List.ec | 8 - theories/datatypes/Real.ec | 8 - theories/datatypes/Tuple.eca | 8 - theories/datatypes/Word.eca | 8 - theories/distributions/DBool.ec | 8 - theories/distributions/DInterval.ec | 8 - theories/distributions/DJoin.ec | 8 - theories/distributions/DList.ec | 8 - theories/distributions/DMap.ec | 8 - theories/distributions/DProd.ec | 8 - theories/distributions/Dexcepted.ec | 8 - theories/distributions/Dfilter.ec | 8 - theories/distributions/Distr.ec | 8 - theories/distributions/Mu_mem.ec | 8 - theories/distributions/SDist.ec | 8 - theories/encryption/DDH_hybrid.ec | 8 - theories/encryption/Hybrid.ec | 8 - theories/encryption/Indist.ec | 8 - theories/encryption/Means.ec | 8 - theories/encryption/PKE_hybrid.ec | 8 - theories/encryption/SampleBool.ec | 8 - theories/looping/FoldProc.eca | 8 - theories/looping/IterProc.eca | 8 - theories/modules/EventPartitioning.ec | 8 - theories/modules/PlugAndPray.eca | 8 - theories/modules/Pr_half.eca | 8 - theories/modules/RndProd.eca | 8 - theories/newth/SmtMap.ec | 8 - theories/oldlibs/CyclicGroup.ec | 7 - theories/oldlibs/Cyclic_group_prime.ec | 8 - theories/oldlibs/OldDistr.ec | 8 - theories/oldlibs/OldFMap.ec | 8 - theories/oldlibs/PrimeField.ec | 8 - theories/oldlibs/Prime_field.ec | 8 - theories/prelude/Logic.ec | 8 - theories/prelude/Pervasive.ec | 8 - theories/prelude/Tactics.ec | 8 - theories/query_counting/Counter.eca | 8 - theories/query_counting/OracleBounds.ec | 8 - theories/structure/Discrete.ec | 8 - theories/structure/FinType.ec | 8 - theories/structure/Finite.ec | 8 - theories/structure/Quotient.ec | 8 - theories/structure/Subtype.eca | 8 - theories/structure/WF.ec | 6 - theories/tactics/AlgTactic.ec | 8 - theories/tactics/CHoareTactic.ec | 8 - theories/tactics/FelTactic.ec | 8 - 325 files changed, 56 insertions(+), 2831 deletions(-) create mode 100644 AUTHORS delete mode 100644 COPYRIGHT delete mode 100644 COPYRIGHT.yaml create mode 100644 LICENSE delete mode 100755 scripts/srctx/license diff --git a/AUTHORS b/AUTHORS new file mode 100644 index 0000000000..be06bf76b6 --- /dev/null +++ b/AUTHORS @@ -0,0 +1,27 @@ +The following people have contributed code and/or ideas to EasyCrypt: + +Adrien Koutsos +Alley Stoughton +Asif Mallik +Benedikt Schmidt +Benjamin Gregoire +César Kunz +Christian Doczkal +Cécile Baritel-Ruet +Davide Ramaglietta +Davy Guillaume +François Dupressoir +Gilles Barthe +Guillermo Ramos +Juan Manuel Crespo +Kai-Chun Ning +Lavinia Damian +Martin Ceresa +Matthias Meijers +Mayram +Morten Solberg +Oskar Goldhahn +Pierre-Yves Strub +Roberto Metere +Santiago Zanella-Béguelin +Vincent Laporte diff --git a/COPYRIGHT b/COPYRIGHT deleted file mode 100644 index 5846f1a687..0000000000 --- a/COPYRIGHT +++ /dev/null @@ -1,15 +0,0 @@ -EasyCrypt (excluding the EasyCrypt standard library): - Copyright (c) - 2012-2016 - IMDEA Software Institute - Copyright (c) - 2012-2021 - Inria - Copyright (c) - 2012-2021 - X - Distributed under the terms of the CeCILL-C license - - http://www.cecill.info/licences/Licence_CeCILL-C_V1-en.txt - -EasyCrypt standard library (theories/**/*.ec): - Copyright (c) - 2012-2016 - IMDEA Software Institute - Copyright (c) - 2012-2021 - Inria - Copyright (c) - 2012-2021 - X - Distributed under the terms of the CeCILL-B licence. - - http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt diff --git a/COPYRIGHT.yaml b/COPYRIGHT.yaml deleted file mode 100644 index c8d9234876..0000000000 --- a/COPYRIGHT.yaml +++ /dev/null @@ -1,29 +0,0 @@ -entities: - IMDEA : "IMDEA Software Institute" - INRIA : "Inria" - X : "Ecole Polytechnique" - RM : "Roberto Metere " -copyrights: - - pattern: ["src/*.ml*", "src/*/*.ml*"] - style: "ocaml" - license: "CeCILL-C-V1" - copyrights: - - { who: "IMDEA", date: "2012--2016" } - - { who: "INRIA", date: "2012--2021" } - - { who: "X" , date: "2012--2021" } - - pattern: - - "theories/crypto/SigmaProtocol.ec" - - "theories/crypto/Commitment.ec" - - "theories/crypto/DLog.ec" - style: "ocaml" - license: "CeCILL-B-V1" - last: true - copyrights: - - { who: "RM", date: "2016--2017" } - - pattern: ["theories/*.ec", "theories/*/*.ec*"] - style: "ocaml" - license: "CeCILL-B-V1" - copyrights: - - { who: "IMDEA", date: "2012--2016" } - - { who: "INRIA", date: "2012--2021" } - - { who: "X" , date: "2012--2021" } diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000000..ff62ff6f6c --- /dev/null +++ b/LICENSE @@ -0,0 +1,24 @@ +MIT License + +Copyright (c) 2012 IMDEA Software Institute +Copyright (c) 2012 Inria +Copyright (c) 2017 École Polytechnique +Copyright (c) EasyCrypt contributors (see AUTHORS) + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/Makefile b/Makefile index 3466648785..4371b74607 100644 --- a/Makefile +++ b/Makefile @@ -15,7 +15,7 @@ CHECK += $(ECEXTRA) config/tests.config # -------------------------------------------------------------------- .PHONY: default build byte native tests check examples -.PHONY: clean install uninstall license +.PHONY: clean install uninstall default: build @true @@ -46,9 +46,3 @@ clean: clean_eco: find theories examples -name '*.eco' -exec rm '{}' ';' - -license: - scripts/srctx/license COPYRIGHT.yaml \ - $(shell find src -name '*.ml' -o -name '*.ml[a-z]') \ - $(shell find theories -name '*.ec' -o -name '*.ec[a-z]') \ - $(shell find proofgeneral/easycrypt -name '*.el') diff --git a/examples/Pedersen.ec b/examples/Pedersen.ec index e89e1e46c8..87dcb31858 100644 --- a/examples/Pedersen.ec +++ b/examples/Pedersen.ec @@ -1,9 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2016--2017 - Roberto Metere (r.metere2@ncl.ac.uk) - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* * A formal verification of the Pedersen commitment scheme * diff --git a/examples/SchnorrPK.ec b/examples/SchnorrPK.ec index 1f4d56651f..0afbe41df8 100644 --- a/examples/SchnorrPK.ec +++ b/examples/SchnorrPK.ec @@ -1,9 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2016--2017 - Roberto Metere (r.metere2@ncl.ac.uk) - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* * A formal verification of the Schnorr proof of knowledge *) diff --git a/examples/Upto.ec b/examples/Upto.ec index ca8a315b03..1512c76102 100644 --- a/examples/Upto.ec +++ b/examples/Upto.ec @@ -1,10 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2015 - IMDEA Software Institute - * Copyright (c) - 2012--2015 - Inria - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Int Real Distr StdOrder StdBigop. (*---*) import RealOrder Bigreal BRA. require (*--*) FelTactic. diff --git a/examples/vonNeumann.eca b/examples/vonNeumann.eca index a40b409147..a275e6a359 100644 --- a/examples/vonNeumann.eca +++ b/examples/vonNeumann.eca @@ -1,10 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2016 - Inria - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) (* In this theory, we illustrate some reasoning on distributions on diff --git a/scripts/srctx/license b/scripts/srctx/license deleted file mode 100755 index a8fb0f652d..0000000000 --- a/scripts/srctx/license +++ /dev/null @@ -1,219 +0,0 @@ -#! /usr/bin/env python3 - -# (c) Pierre-Yves Strub - 2014--2021 - -# -------------------------------------------------------------------- -import sys, os, re, yaml, yaml.loader as yloader, schema -import tempfile, fnmatch - -# -------------------------------------------------------------------- -META = schema.Schema(dict( - entities = schema.Schema({object: str}), - copyrights = [{ - "pattern" - : [str], - "style" - : str, - "license" - : str, - schema.Optional("last", default = False) - : bool, - "copyrights" - : [dict(who = str, date = str)], - }], -)) - -# -------------------------------------------------------------------- -class AttrDict(dict): - def __getattr__(self, name): - return self[name] - -class AttrDictSafeConstructor(yloader.SafeConstructor): - def construct_yaml_map(self, node): - data = AttrDict() - yield data - value = self.construct_mapping(node) - data.update(value) - -AttrDictSafeConstructor.add_constructor( - u'tag:yaml.org,2002:map', AttrDictSafeConstructor.construct_yaml_map) - -class AttrDictSafeLoader(yloader.Reader , - yloader.Scanner , - yloader.Parser , - yloader.Composer , - AttrDictSafeConstructor, - yloader.Resolver ): - - def __init__(self, stream): - yloader.Reader.__init__(self, stream) - yloader.Scanner.__init__(self) - yloader.Parser.__init__(self) - yloader.Composer.__init__(self) - AttrDictSafeConstructor.__init__(self) - yloader.Resolver.__init__(self) - -# -------------------------------------------------------------------- -class Object: - def __init__(self, **kw): - self.__dict__.update(kw) - -# -------------------------------------------------------------------- -class CopyrightError(Exception): - pass - -# -------------------------------------------------------------------- -class Copyright: - COPYRIGHT = 'Copyright (c) - %s - %s' - LICENSE = 'Distributed under the terms of the %s license' - - # ---------------------------------------------------------------- - def __init__(self, ini): - self.ini = ini - - # ---------------------------------------------------------------- - def get_copyright(self, filename): - def _norm(x): - return (self.ini['entities'].get(x.who, x.who), x.date) - - copyrights = [] - for pt in self.ini.copyrights: - for test in pt['pattern']: - if fnmatch.fnmatch(filename, test): - for cp in pt['copyrights']: - thecp = Object( - who = cp['who' ], - date = cp['date' ], - style = pt['style'], - license = pt.get('license', None)) - copyrights.append(thecp) - break - else: - continue - if pt['last']: - break - - styles = sorted(set([x.style for x in copyrights])) - if len(styles) > 1: - raise CopyrightError( \ - '%s: multiple styles: %s' % (filename, ', '.join(styles))) - - licenses = [x.license for x in copyrights if x.license is not None] - licenses = sorted(set(licenses)) - if len(licenses) > 1: - raise CopyrightError( \ - '%s: multiple licenses: %s' % (filename, ', '.join(licenses))) - - if not copyrights: - return None - return Object( - copyrights = [_norm(x) for x in copyrights], - license = (licenses or [None])[0], - style = (styles or [None])[0]) - - # ---------------------------------------------------------------- - def format(self, copyrights, license = None): - def _cp(x): - return self.COPYRIGHT % (x[1], x[0]) - aout = [_cp(x) for x in copyrights] - if license is not None: - aout.append('') - aout.append(self.LICENSE % (license,)) - return aout - -# -------------------------------------------------------------------- -class CopyrightStyle: - STYLES = dict() - - def strip(self, contents): - raise RuntimeError - - def format(self, contents): - raise RuntimeError - - @classmethod - def factory(cls, name): - if name not in cls.STYLES: - raise CopyrightError('unknown style: %s' % (name,)) - return cls.STYLES[name]() - -# -------------------------------------------------------------------- -class CoqCopyrightStyle(CopyrightStyle): - _re = r'^\s*\(\*[^A-Za-z0-9]*copyright.*?\*\)\s*' - - def strip(self, contents): - m = re.search(self._re, contents, re.S | re.I) - if m is not None: - contents = contents[m.end():] - return contents - - def format(self, contents): - contents = [' * %s' % (x,) for x in contents] - contents = ['(* %s' % ('-' * 68,)] + contents + [' * %s *)' % ('-' * 68,)] - contents = [x.rstrip() for x in contents] - contents = '\n'.join([x.rstrip('\r\n') for x in contents]) + '\n\n' - return contents - -# -------------------------------------------------------------------- -class ELispCopyrightStyle(CopyrightStyle): - _re = r'^\s*;;\*[^A-Za-z0-9]*copyright.*?;;x' - _re = r'^\s*;;(?:\s|-)*[^A-Za-z0-9]*copyright.*?;;\s*[-]+\s*' - - def strip(self, contents): - m = re.search(self._re, contents, re.S | re.I) - if m is not None: - contents = contents[m.end():] - return contents - - def format(self, contents): - contents = [';; %s' % (x,) for x in contents] - contents = [';; %s' % ('-' * 68,)] + contents + [';; %s' % ('-' * 68,)] - contents = [x.rstrip() for x in contents] - contents = '\n'.join([x.rstrip('\r\n') for x in contents]) + '\n\n' - return contents - -# -------------------------------------------------------------------- -CopyrightStyle.STYLES['coq' ] = CoqCopyrightStyle -CopyrightStyle.STYLES['ocaml'] = CoqCopyrightStyle -CopyrightStyle.STYLES['ec' ] = CoqCopyrightStyle -CopyrightStyle.STYLES['elisp'] = ELispCopyrightStyle - -# -------------------------------------------------------------------- -def _main(): - # ---------------------------------------------------------------- - if len(sys.argv)-1 < 2: - print("Usage: %s [CONFIG] [FILES...]" % (sys.argv[0],), file=sys.stderr) - exit(1) - inifile = sys.argv[1] - srcfiles = sys.argv[2:] - - # ---------------------------------------------------------------- - with open(inifile, 'r') as stream: - ini = yaml.load(stream, Loader = AttrDictSafeLoader) - ini = META.validate(ini) - ini = Copyright(ini) - - # ---------------------------------------------------------------- - for filename in srcfiles: - infos = ini.get_copyright(filename) - if infos is None: continue - - style = CopyrightStyle.factory(infos.style) - cp = ini.format(infos.copyrights, infos.license) - cp = style.format(cp) - - with open(filename, 'r') as stream: - contents = stream.read() - contents = style.strip(contents) - - try: os.unlink(filename + '~') - except OSError: pass - os.rename(filename, filename + '~') - - with open(filename, 'w') as stream: - stream.write(cp) - stream.write(contents) - -# -------------------------------------------------------------------- -if __name__ == '__main__': - _main() diff --git a/src/ec.ml b/src/ec.ml index fb32e12e44..179a9a849b 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcOptions diff --git a/src/ecAlgTactic.ml b/src/ecAlgTactic.ml index 1b6eab8cf9..e32a326b6b 100644 --- a/src/ecAlgTactic.ml +++ b/src/ecAlgTactic.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/ecAlgTactic.mli b/src/ecAlgTactic.mli index 647b81ccf6..eb4f106f52 100644 --- a/src/ecAlgTactic.mli +++ b/src/ecAlgTactic.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcTypes diff --git a/src/ecAlgebra.ml b/src/ecAlgebra.ml index b9b84ab42a..2cd7f1aa7f 100644 --- a/src/ecAlgebra.ml +++ b/src/ecAlgebra.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecAlgebra.mli b/src/ecAlgebra.mli index 0ff24a0692..5a4d823f70 100644 --- a/src/ecAlgebra.mli +++ b/src/ecAlgebra.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcFol diff --git a/src/ecBaseLogic.ml b/src/ecBaseLogic.ml index b5945c42c4..45d18d2c48 100644 --- a/src/ecBaseLogic.ml +++ b/src/ecBaseLogic.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcTypes open EcCoreFol diff --git a/src/ecBigInt.ml b/src/ecBigInt.ml index 63b0685fcf..a9a8b5a845 100644 --- a/src/ecBigInt.ml +++ b/src/ecBigInt.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) module B = Big_int diff --git a/src/ecBigInt.mli b/src/ecBigInt.mli index 087039f81f..087f7fef7a 100644 --- a/src/ecBigInt.mli +++ b/src/ecBigInt.mli @@ -1,9 +1 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - include EcBigIntCore.TheInterface diff --git a/src/ecBigIntCore.ml b/src/ecBigIntCore.ml index 89baa75d59..39d9391478 100644 --- a/src/ecBigIntCore.ml +++ b/src/ecBigIntCore.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) module type TheInterface = sig type zint diff --git a/src/ecCHoare.ml b/src/ecCHoare.ml index d4d5f4e1de..07a85472e8 100644 --- a/src/ecCHoare.ml +++ b/src/ecCHoare.ml @@ -1,12 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2018 - Inria - * Copyright (c) - 2012--2018 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - - (* -------------------------------------------------------------------- *) (* Function for cost *) open EcUtils diff --git a/src/ecCallbyValue.ml b/src/ecCallbyValue.ml index 9d868a4845..1d887eb327 100644 --- a/src/ecCallbyValue.ml +++ b/src/ecCallbyValue.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/ecCallbyValue.mli b/src/ecCallbyValue.mli index 3f43e65546..dc250fc6a2 100644 --- a/src/ecCallbyValue.mli +++ b/src/ecCallbyValue.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcFol open EcEnv diff --git a/src/ecCommands.ml b/src/ecCommands.ml index e1f4aa777b..443d4dda62 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcLocation diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 9ef5ba0f9c..83197b4688 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml index 3639d69791..faf3f45c8b 100644 --- a/src/ecCoreFol.ml +++ b/src/ecCoreFol.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli index b2fd3948a2..f72852802e 100644 --- a/src/ecCoreFol.mli +++ b/src/ecCoreFol.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcBigInt diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 93b8f51d18..c2e65f026a 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation open EcUtils diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index 628ebb335b..13e6f3e87e 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/ecCoreHiPhl.ml b/src/ecCoreHiPhl.ml index 62212c61bf..6c7e3e693f 100644 --- a/src/ecCoreHiPhl.ml +++ b/src/ecCoreHiPhl.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcTypes open EcFol diff --git a/src/ecCoreHiPhl.mli b/src/ecCoreHiPhl.mli index c0944086cd..c5808c0ed6 100644 --- a/src/ecCoreHiPhl.mli +++ b/src/ecCoreHiPhl.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcTypes diff --git a/src/ecCoreLib.ml b/src/ecCoreLib.ml index 94a044a8fe..d86450d9ac 100644 --- a/src/ecCoreLib.ml +++ b/src/ecCoreLib.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) let s_get = "_.[_]" let s_set = "_.[_<-_]" diff --git a/src/ecCoreLib.mli b/src/ecCoreLib.mli index d7f5f4e683..19385e7d75 100644 --- a/src/ecCoreLib.mli +++ b/src/ecCoreLib.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcPath diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml index 32225fe18c..a1e000aae2 100644 --- a/src/ecCoreModules.ml +++ b/src/ecCoreModules.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2018 - Inria - * Copyright (c) - 2012--2018 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli index ac36a065be..ff291fd3e2 100644 --- a/src/ecCoreModules.mli +++ b/src/ecCoreModules.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2018 - Inria - * Copyright (c) - 2012--2018 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcPath diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 7919239c68..98bf08d8d4 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/ecDecl.mli b/src/ecDecl.mli index a592d852bc..3ab3ca4034 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecEco.ml b/src/ecEco.ml index 9ed4474f2f..cd80c80205 100644 --- a/src/ecEco.ml +++ b/src/ecEco.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 75ac538766..b6596e4a61 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 6a60aad47e..4c1869cb6e 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcPath open EcSymbols diff --git a/src/ecField.ml b/src/ecField.ml index f70da510a3..e08fb7bc20 100644 --- a/src/ecField.ml +++ b/src/ecField.ml @@ -1,21 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - -(* Copyright The Coq Development Team, 1999-2010 - * Copyright INRIA - CNRS - LIX - LRI - PPS, 1999-2010 - * - * This file is distributed under the terms of the: - * GNU Lesser General Public License Version 2.1 - * - * This file originates from the `Coq Proof Assistant' - * It has been modified for the needs of EasyCrypt - *) - (* -------------------------------------------------------------------- *) open EcRing open EcBigInt.Notations diff --git a/src/ecField.mli b/src/ecField.mli index 808151ee60..82b681b980 100644 --- a/src/ecField.mli +++ b/src/ecField.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcRing open EcBigInt diff --git a/src/ecFol.ml b/src/ecFol.ml index 68151f2e8c..e9177725fc 100644 --- a/src/ecFol.ml +++ b/src/ecFol.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcIdent open EcUtils diff --git a/src/ecFol.mli b/src/ecFol.mli index ca01c8dd75..53553256ff 100644 --- a/src/ecFol.mli +++ b/src/ecFol.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcBigInt open EcPath diff --git a/src/ecGState.ml b/src/ecGState.ml index b19672b2d7..f7bdb53d9e 100644 --- a/src/ecGState.ml +++ b/src/ecGState.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps diff --git a/src/ecGState.mli b/src/ecGState.mli index 4323f47e8c..2124981bba 100644 --- a/src/ecGState.mli +++ b/src/ecGState.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) (* Global / mutable EasyCrypt state that can be attached to an diff --git a/src/ecGenRegexp.ml b/src/ecGenRegexp.ml index b463aa5a41..5328b30d44 100644 --- a/src/ecGenRegexp.ml +++ b/src/ecGenRegexp.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index fe65b97493..418709eb94 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcLocation diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index f8064cd045..e998dce9ee 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation open EcSymbols diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml index 36614161c0..97f3da4153 100644 --- a/src/ecHiInductive.ml +++ b/src/ecHiInductive.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcLocation diff --git a/src/ecHiInductive.mli b/src/ecHiInductive.mli index c02a267929..32fd116458 100644 --- a/src/ecHiInductive.mli +++ b/src/ecHiInductive.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcIdent diff --git a/src/ecHiNotations.ml b/src/ecHiNotations.ml index b3e78c6ca7..988edcd976 100644 --- a/src/ecHiNotations.ml +++ b/src/ecHiNotations.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecHiNotations.mli b/src/ecHiNotations.mli index 95fd4a9b7f..54dd54543e 100644 --- a/src/ecHiNotations.mli +++ b/src/ecHiNotations.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcParsetree diff --git a/src/ecHiPredicates.ml b/src/ecHiPredicates.ml index cfd690dca8..17dd795cc6 100644 --- a/src/ecHiPredicates.ml +++ b/src/ecHiPredicates.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecHiPredicates.mli b/src/ecHiPredicates.mli index a62848d8ea..eb56da6628 100644 --- a/src/ecHiPredicates.mli +++ b/src/ecHiPredicates.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation open EcSymbols diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 7c73594ff6..6333ba4481 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcLocation diff --git a/src/ecHiTacticals.mli b/src/ecHiTacticals.mli index 580e03f9c3..2bdbee1e3b 100644 --- a/src/ecHiTacticals.mli +++ b/src/ecHiTacticals.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcCoreGoal diff --git a/src/ecIdent.ml b/src/ecIdent.ml index 970d4ca3ba..60ab346526 100644 --- a/src/ecIdent.ml +++ b/src/ecIdent.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcUtils diff --git a/src/ecIdent.mli b/src/ecIdent.mli index 8e19257208..988430a72e 100644 --- a/src/ecIdent.mli +++ b/src/ecIdent.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps open EcSymbols diff --git a/src/ecInductive.ml b/src/ecInductive.ml index 24ebc8681b..b915fd713e 100644 --- a/src/ecInductive.ml +++ b/src/ecInductive.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecInductive.mli b/src/ecInductive.mli index 1d219629b2..2b1c5a97c5 100644 --- a/src/ecInductive.mli +++ b/src/ecInductive.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecIo.ml b/src/ecIo.ml index 86c9bd2fe7..3aabf0fbfe 100644 --- a/src/ecIo.ml +++ b/src/ecIo.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils diff --git a/src/ecIo.mli b/src/ecIo.mli index 6f31d8557b..ce52869b44 100644 --- a/src/ecIo.mli +++ b/src/ecIo.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type ecreader diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 1f13f6c2c4..b3f06247d6 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) { open EcUtils diff --git a/src/ecLoader.ml b/src/ecLoader.ml index cd226e80a3..8f9ea6ddb0 100644 --- a/src/ecLoader.ml +++ b/src/ecLoader.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils diff --git a/src/ecLoader.mli b/src/ecLoader.mli index 4a9d3bf567..3b5fe2d316 100644 --- a/src/ecLoader.mli +++ b/src/ecLoader.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type idx_t type ecloader diff --git a/src/ecLocation.ml b/src/ecLocation.ml index 434c2d52f0..bd77b14bef 100644 --- a/src/ecLocation.ml +++ b/src/ecLocation.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open Lexing diff --git a/src/ecLocation.mli b/src/ecLocation.mli index 1bf996aa45..4ab3390143 100644 --- a/src/ecLocation.mli +++ b/src/ecLocation.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open Lexing diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 61b181c99f..b9a58c7b20 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcLocation diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index afa0b4a98c..217b87dd41 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation open EcParsetree diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 90dc504f9e..9a607e9d5b 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcUtils diff --git a/src/ecMaps.ml b/src/ecMaps.ml index 668f054b43..746c71b477 100644 --- a/src/ecMaps.ml +++ b/src/ecMaps.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 87b70a5e45..3711c94c21 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) (* Expressions / formulas matching for tactics *) (* -------------------------------------------------------------------- *) diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 93714170a0..22fce19103 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps open EcUid diff --git a/src/ecMemory.ml b/src/ecMemory.ml index 16e858f4ba..c0bc63ccce 100644 --- a/src/ecMemory.ml +++ b/src/ecMemory.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcUtils diff --git a/src/ecMemory.mli b/src/ecMemory.mli index e11236b926..b7f5ba98e5 100644 --- a/src/ecMemory.mli +++ b/src/ecMemory.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcTypes diff --git a/src/ecModules.ml b/src/ecModules.ml index dbdee9bfa2..efb6c4ea51 100644 --- a/src/ecModules.ml +++ b/src/ecModules.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2018 - Inria - * Copyright (c) - 2012--2018 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcPath diff --git a/src/ecModules.mli b/src/ecModules.mli index 1bf85e83be..996e6342b1 100644 --- a/src/ecModules.mli +++ b/src/ecModules.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2018 - Inria - * Copyright (c) - 2012--2018 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcPath open EcCoreFol diff --git a/src/ecOptions.ml b/src/ecOptions.ml index 261bf68e27..b54af4986a 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 1a1a05ef3d..acd8a4c990 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type command = [ | `Compile of cmp_option diff --git a/src/ecPException.ml b/src/ecPException.ml index 9b338cd15f..2bd807271e 100644 --- a/src/ecPException.ml +++ b/src/ecPException.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type exn_printer = Format.formatter -> exn -> unit diff --git a/src/ecPException.mli b/src/ecPException.mli index f35da24222..c95abb10a2 100644 --- a/src/ecPException.mli +++ b/src/ecPException.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type exn_printer = Format.formatter -> exn -> unit diff --git a/src/ecPV.ml b/src/ecPV.ml index 0d9e8b3f1e..75ac88bc7c 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/ecPV.mli b/src/ecPV.mli index 3f1ab22356..14abba5370 100644 --- a/src/ecPV.mli +++ b/src/ecPV.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps open EcPath diff --git a/src/ecParser.mly b/src/ecParser.mly index eec6b6c19c..21fdecaafa 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - %{ open EcUtils open EcLocation diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 2317ce0ef9..4117477a32 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2018 - Inria - * Copyright (c) - 2012--2018 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcBigInt open EcMaps diff --git a/src/ecPath.ml b/src/ecPath.ml index 045dd5b288..4fa7421552 100644 --- a/src/ecPath.ml +++ b/src/ecPath.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecPath.mli b/src/ecPath.mli index 2476efc11f..7adec46bba 100644 --- a/src/ecPath.mli +++ b/src/ecPath.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcIdent open EcMaps diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 3b386ea0a4..b76c5afece 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps open EcSymbols diff --git a/src/ecPrinting.mli b/src/ecPrinting.mli index c3d6a437f8..5b5802e8eb 100644 --- a/src/ecPrinting.mli +++ b/src/ecPrinting.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcIdent open EcSymbols diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml index 51871f77d5..b11003ef4b 100644 --- a/src/ecProofTerm.ml +++ b/src/ecProofTerm.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcLocation diff --git a/src/ecProofTerm.mli b/src/ecProofTerm.mli index 04b81b8198..e3ad54ff41 100644 --- a/src/ecProofTerm.mli +++ b/src/ecProofTerm.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation open EcSymbols diff --git a/src/ecProofTyping.ml b/src/ecProofTyping.ml index 8b112d09c2..259cfcc402 100644 --- a/src/ecProofTyping.ml +++ b/src/ecProofTyping.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/ecProofTyping.mli b/src/ecProofTyping.mli index 8ea68d180a..6b7432647f 100644 --- a/src/ecProofTyping.mli +++ b/src/ecProofTyping.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcIdent diff --git a/src/ecProvers.ml b/src/ecProvers.ml index 66ddfe5c6e..5bfe5ebe4f 100644 --- a/src/ecProvers.ml +++ b/src/ecProvers.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open Why3 diff --git a/src/ecProvers.mli b/src/ecProvers.mli index ce393d827f..c647d01750 100644 --- a/src/ecProvers.mli +++ b/src/ecProvers.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcPath diff --git a/src/ecReduction.ml b/src/ecReduction.ml index 36177e593a..6999348c7b 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/ecReduction.mli b/src/ecReduction.mli index 1994c2306a..f790125b65 100644 --- a/src/ecReduction.mli +++ b/src/ecReduction.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcIdent open EcPath diff --git a/src/ecRegexp.ml b/src/ecRegexp.ml index 5b6be6ddc4..f80473bfa8 100644 --- a/src/ecRegexp.ml +++ b/src/ecRegexp.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils diff --git a/src/ecRegexp.mli b/src/ecRegexp.mli index 419e1a14da..7cefb01029 100644 --- a/src/ecRegexp.mli +++ b/src/ecRegexp.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type error type regexp diff --git a/src/ecRing.ml b/src/ecRing.ml index 19c70b2338..3d88f074c0 100644 --- a/src/ecRing.ml +++ b/src/ecRing.ml @@ -1,21 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - -(* Copyright The Coq Development Team, 1999-2010 - * Copyright INRIA - CNRS - LIX - LRI - PPS, 1999-2010 - * - * This file is distributed under the terms of the: - * GNU Lesser General Public License Version 2.1 - * - * This file originates from the `Coq Proof Assistant' - * It has been modified for the needs of EasyCrypt - *) - (* -------------------------------------------------------------------- *) open EcMaps open EcUtils diff --git a/src/ecRing.mli b/src/ecRing.mli index dbce14834c..e83ea8dc10 100644 --- a/src/ecRing.mli +++ b/src/ecRing.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcBigInt open EcMaps diff --git a/src/ecScope.ml b/src/ecScope.ml index 33122139c3..8531435f3b 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecScope.mli b/src/ecScope.mli index 53a98365bb..066a79b67d 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcLocation diff --git a/src/ecSearch.ml b/src/ecSearch.ml index ec2fe1eda1..c30937e764 100644 --- a/src/ecSearch.ml +++ b/src/ecSearch.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcPath diff --git a/src/ecSearch.mli b/src/ecSearch.mli index 86d6404033..dd076d9284 100644 --- a/src/ecSearch.mli +++ b/src/ecSearch.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcPath open EcFol diff --git a/src/ecSection.ml b/src/ecSection.ml index 75ff2d8e7d..35acf95595 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecSection.mli b/src/ecSection.mli index ac03fd1d49..b27773fd13 100644 --- a/src/ecSection.mli +++ b/src/ecSection.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcModules open EcEnv diff --git a/src/ecSmt.ml b/src/ecSmt.ml index 89bcde7736..35227a04d1 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecSmt.mli b/src/ecSmt.mli index 4b09c98c61..2072d9f0c6 100644 --- a/src/ecSmt.mli +++ b/src/ecSmt.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcPath open EcFol diff --git a/src/ecStrongRing.ml b/src/ecStrongRing.ml index 3f05bbbb75..62cdc49917 100644 --- a/src/ecStrongRing.ml +++ b/src/ecStrongRing.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 53e3093884..9ef5986db3 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/ecSubst.mli b/src/ecSubst.mli index ad27a742d3..18a4857f91 100644 --- a/src/ecSubst.mli +++ b/src/ecSubst.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcIdent open EcPath diff --git a/src/ecSymbols.ml b/src/ecSymbols.ml index ec252c4bb9..e1e37313f4 100644 --- a/src/ecSymbols.ml +++ b/src/ecSymbols.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type symbol = string type qsymbol = symbol list * symbol diff --git a/src/ecSymbols.mli b/src/ecSymbols.mli index a087d46a58..a761df52fb 100644 --- a/src/ecSymbols.mli +++ b/src/ecSymbols.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps diff --git a/src/ecTerminal.ml b/src/ecTerminal.ml index 78e0077f0c..b293743837 100644 --- a/src/ecTerminal.ml +++ b/src/ecTerminal.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils diff --git a/src/ecTerminal.mli b/src/ecTerminal.mli index b0e5468b8b..757558618e 100644 --- a/src/ecTerminal.mli +++ b/src/ecTerminal.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type terminal diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 974d23b38b..b3f3c48c5d 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* ------------------------------------------------------------------ *) open EcUtils open EcSymbols diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli index 92d5d6adc2..a1e5f43d9f 100644 --- a/src/ecThCloning.mli +++ b/src/ecThCloning.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation open EcSymbols diff --git a/src/ecTheory.ml b/src/ecTheory.ml index 746714b8e6..4c3217c950 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 522f932eef..8c91f53e6d 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcPath diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index e867baad17..1b4ada2aab 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* ------------------------------------------------------------------ *) open EcSymbols open EcUtils diff --git a/src/ecTheoryReplay.mli b/src/ecTheoryReplay.mli index 217ae8cf82..5afd716ba4 100644 --- a/src/ecTheoryReplay.mli +++ b/src/ecTheoryReplay.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* ------------------------------------------------------------------ *) open EcSymbols open EcPath diff --git a/src/ecTransMatching.ml b/src/ecTransMatching.ml index 92358e4325..0e7ce501f5 100644 --- a/src/ecTransMatching.ml +++ b/src/ecTransMatching.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/ecTransMatching.mli b/src/ecTransMatching.mli index 836e5012e7..070bd697de 100644 --- a/src/ecTransMatching.mli +++ b/src/ecTransMatching.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcMatching diff --git a/src/ecTypeClass.ml b/src/ecTypeClass.ml index 22de2fb90f..f142cc94d9 100644 --- a/src/ecTypeClass.ml +++ b/src/ecTypeClass.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcPath diff --git a/src/ecTypeClass.mli b/src/ecTypeClass.mli index d1e52e4d8e..9c8b566600 100644 --- a/src/ecTypeClass.mli +++ b/src/ecTypeClass.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcPath diff --git a/src/ecTypes.ml b/src/ecTypes.ml index e948c7fdcf..5a1712fe3b 100644 --- a/src/ecTypes.ml +++ b/src/ecTypes.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/ecTypes.mli b/src/ecTypes.mli index cbf6a68ae8..ab5bea9ee5 100644 --- a/src/ecTypes.mli +++ b/src/ecTypes.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcBigInt open EcMaps diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 3916b0a1a8..add0d32821 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcPath diff --git a/src/ecTyping.mli b/src/ecTyping.mli index 42f6b40aea..fa72e7b9c4 100644 --- a/src/ecTyping.mli +++ b/src/ecTyping.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcSymbols diff --git a/src/ecUFind.ml b/src/ecUFind.ml index 86e661632f..3fe12071d6 100644 --- a/src/ecUFind.ml +++ b/src/ecUFind.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps open EcUtils diff --git a/src/ecUFind.mli b/src/ecUFind.mli index fecbf88d03..674fb54e80 100644 --- a/src/ecUFind.mli +++ b/src/ecUFind.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) module type Item = sig type t diff --git a/src/ecUid.ml b/src/ecUid.ml index 299e2caccc..6e9124b62c 100644 --- a/src/ecUid.ml +++ b/src/ecUid.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcMaps diff --git a/src/ecUid.mli b/src/ecUid.mli index a17c181ef2..885bcbd99f 100644 --- a/src/ecUid.mli +++ b/src/ecUid.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcMaps open EcSymbols diff --git a/src/ecUnify.ml b/src/ecUnify.ml index 6c6c833ad6..508422e92e 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcIdent diff --git a/src/ecUnify.mli b/src/ecUnify.mli index 6ee0e564cc..366a69ae6b 100644 --- a/src/ecUnify.mli +++ b/src/ecUnify.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUid open EcSymbols diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml index 4f2c26b320..aa51730904 100644 --- a/src/ecUserMessages.ml +++ b/src/ecUserMessages.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcUid diff --git a/src/ecUserMessages.mli b/src/ecUserMessages.mli index 4ee1b51c56..efe97e0efc 100644 --- a/src/ecUserMessages.mli +++ b/src/ecUserMessages.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/ecUtils.ml b/src/ecUtils.ml index 310d05833b..32543f9539 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) module Enum = BatEnum diff --git a/src/ecUtils.mli b/src/ecUtils.mli index a2329578bf..c622664d3f 100644 --- a/src/ecUtils.mli +++ b/src/ecUtils.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) module Enum = BatEnum diff --git a/src/ecVersion.ml b/src/ecVersion.ml index da56176b74..a3b983868f 100644 --- a/src/ecVersion.ml +++ b/src/ecVersion.ml @@ -1,16 +1,9 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) let copyright = [ - "Copyright (c) - 2012-2016 - IMDEA Software Institute"; - "Copyright (c) - 2012-2021 - Inria"; - "Copyright (c) - 2017-2021 - Ecole Polytechnique"; + "Copyright (c) 2012 IMDEA Software Institute"; + "Copyright (c) 2012 Inria"; + "Copyright (c) 2017 Ecole Polytechnique"; + "Copyright (c) EasyCrypt contributors (see AUTHORS)"; ] let url = "https://www.easycrypt.info/" diff --git a/src/ecVersion.mli b/src/ecVersion.mli index d5e6bb7091..0fa68bc63d 100644 --- a/src/ecVersion.mli +++ b/src/ecVersion.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) val copyright : string list val url : string diff --git a/src/ecWhy3Conv.ml b/src/ecWhy3Conv.ml index aba79415d1..1f475e516d 100644 --- a/src/ecWhy3Conv.ml +++ b/src/ecWhy3Conv.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* ----------------------------------------------------------------------*) open EcUtils open Why3 diff --git a/src/ecWhy3Conv.mli b/src/ecWhy3Conv.mli index 6c783c2e71..40ae1f0212 100644 --- a/src/ecWhy3Conv.mli +++ b/src/ecWhy3Conv.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open Why3 diff --git a/src/phl/ecPhlApp.ml b/src/phl/ecPhlApp.ml index 86ce08f57d..4936004c3e 100644 --- a/src/phl/ecPhlApp.ml +++ b/src/phl/ecPhlApp.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcLocation diff --git a/src/phl/ecPhlApp.mli b/src/phl/ecPhlApp.mli index 775d2348c5..5bc16737e7 100644 --- a/src/phl/ecPhlApp.mli +++ b/src/phl/ecPhlApp.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlAuto.ml b/src/phl/ecPhlAuto.ml index d70ab3da79..9029a40439 100644 --- a/src/phl/ecPhlAuto.ml +++ b/src/phl/ecPhlAuto.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/phl/ecPhlAuto.mli b/src/phl/ecPhlAuto.mli index e16321a7df..a2af1c04fc 100644 --- a/src/phl/ecPhlAuto.mli +++ b/src/phl/ecPhlAuto.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcCoreGoal.FApi diff --git a/src/phl/ecPhlBdHoare.ml b/src/phl/ecPhlBdHoare.ml index 8fd5c76084..c3206e2a36 100644 --- a/src/phl/ecPhlBdHoare.ml +++ b/src/phl/ecPhlBdHoare.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcFol diff --git a/src/phl/ecPhlBdHoare.mli b/src/phl/ecPhlBdHoare.mli index 2d1d554479..f12652003a 100644 --- a/src/phl/ecPhlBdHoare.mli +++ b/src/phl/ecPhlBdHoare.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcFol open EcCoreGoal.FApi diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index d1dc7aabc1..6ea5d3c8a6 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlCall.mli b/src/phl/ecPhlCall.mli index fa8d7027ab..a742e9774f 100644 --- a/src/phl/ecPhlCall.mli +++ b/src/phl/ecPhlCall.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcFol diff --git a/src/phl/ecPhlCase.ml b/src/phl/ecPhlCase.ml index c7a4327aba..8e214eaebe 100644 --- a/src/phl/ecPhlCase.ml +++ b/src/phl/ecPhlCase.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* --------------------------------------------------------------------- *) open EcFol open EcCoreGoal diff --git a/src/phl/ecPhlCase.mli b/src/phl/ecPhlCase.mli index 0222a88139..863de93268 100644 --- a/src/phl/ecPhlCase.mli +++ b/src/phl/ecPhlCase.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcFol open EcCoreGoal.FApi diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index 2dc8744b0a..82940194ef 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/phl/ecPhlCodeTx.mli b/src/phl/ecPhlCodeTx.mli index 673d7538ed..e942187c51 100644 --- a/src/phl/ecPhlCodeTx.mli +++ b/src/phl/ecPhlCodeTx.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcTypes diff --git a/src/phl/ecPhlCond.ml b/src/phl/ecPhlCond.ml index a5418da23c..aab66584c5 100644 --- a/src/phl/ecPhlCond.ml +++ b/src/phl/ecPhlCond.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/phl/ecPhlCond.mli b/src/phl/ecPhlCond.mli index 020a3f95f1..cb0e0f035c 100644 --- a/src/phl/ecPhlCond.mli +++ b/src/phl/ecPhlCond.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcCoreGoal.FApi diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index ebf9d0558f..7cf8db0708 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlConseq.mli b/src/phl/ecPhlConseq.mli index 27306b0abd..ebe8ff8ced 100644 --- a/src/phl/ecPhlConseq.mli +++ b/src/phl/ecPhlConseq.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlCoreView.ml b/src/phl/ecPhlCoreView.ml index 04143e9b6d..ef34c91b1d 100644 --- a/src/phl/ecPhlCoreView.ml +++ b/src/phl/ecPhlCoreView.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcFol diff --git a/src/phl/ecPhlCoreView.mli b/src/phl/ecPhlCoreView.mli index b1e3bc0846..971237688d 100644 --- a/src/phl/ecPhlCoreView.mli +++ b/src/phl/ecPhlCoreView.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* --------------------------------------------------------------------- *) open EcCoreGoal.FApi diff --git a/src/phl/ecPhlDeno.ml b/src/phl/ecPhlDeno.ml index a3655d54ee..6045fee6b6 100644 --- a/src/phl/ecPhlDeno.ml +++ b/src/phl/ecPhlDeno.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlDeno.mli b/src/phl/ecPhlDeno.mli index 0020da9fd6..58761b9504 100644 --- a/src/phl/ecPhlDeno.mli +++ b/src/phl/ecPhlDeno.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml index 1b01c92594..9471157247 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcLocation diff --git a/src/phl/ecPhlEager.mli b/src/phl/ecPhlEager.mli index 83621fd279..0e84352332 100644 --- a/src/phl/ecPhlEager.mli +++ b/src/phl/ecPhlEager.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml index bef200d338..0d35dab50e 100644 --- a/src/phl/ecPhlEqobs.ml +++ b/src/phl/ecPhlEqobs.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/phl/ecPhlEqobs.mli b/src/phl/ecPhlEqobs.mli index bf4c2b5b49..d210124949 100644 --- a/src/phl/ecPhlEqobs.mli +++ b/src/phl/ecPhlEqobs.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml index 7441874840..c857ac9fb6 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcFol diff --git a/src/phl/ecPhlExists.mli b/src/phl/ecPhlExists.mli index f52ed8dfdb..024aed440a 100644 --- a/src/phl/ecPhlExists.mli +++ b/src/phl/ecPhlExists.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcFol diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index 7d37060b7f..93da74bfaf 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlFel.mli b/src/phl/ecPhlFel.mli index 3c6c2e781b..7335c48b18 100644 --- a/src/phl/ecPhlFel.mli +++ b/src/phl/ecPhlFel.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcPath open EcParsetree diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index f938b70cbc..6f757c60ba 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlFun.mli b/src/phl/ecPhlFun.mli index 2a6c53a0e3..f66408ad2c 100644 --- a/src/phl/ecPhlFun.mli +++ b/src/phl/ecPhlFun.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml index 7e0564195f..56307113e0 100644 --- a/src/phl/ecPhlHiAuto.ml +++ b/src/phl/ecPhlHiAuto.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlHiAuto.mli b/src/phl/ecPhlHiAuto.mli index cb702934ce..e358a933fd 100644 --- a/src/phl/ecPhlHiAuto.mli +++ b/src/phl/ecPhlHiAuto.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcCoreGoal.FApi diff --git a/src/phl/ecPhlHiBdHoare.ml b/src/phl/ecPhlHiBdHoare.ml index a42c21eb2f..43a06bc54e 100644 --- a/src/phl/ecPhlHiBdHoare.ml +++ b/src/phl/ecPhlHiBdHoare.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/phl/ecPhlHiBdHoare.mli b/src/phl/ecPhlHiBdHoare.mli index 6ac1b1f736..f066e621c0 100644 --- a/src/phl/ecPhlHiBdHoare.mli +++ b/src/phl/ecPhlHiBdHoare.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcCoreGoal.FApi diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml index 93e66f2990..747adbe1a4 100644 --- a/src/phl/ecPhlHiCond.ml +++ b/src/phl/ecPhlHiCond.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcFol diff --git a/src/phl/ecPhlHiCond.mli b/src/phl/ecPhlHiCond.mli index eb2cf33f31..290da4d181 100644 --- a/src/phl/ecPhlHiCond.mli +++ b/src/phl/ecPhlHiCond.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcCoreGoal.FApi diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml index f8c6964571..b61ff54c43 100644 --- a/src/phl/ecPhlInline.ml +++ b/src/phl/ecPhlInline.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcUtils diff --git a/src/phl/ecPhlInline.mli b/src/phl/ecPhlInline.mli index d2c5ab73a7..636f6f4936 100644 --- a/src/phl/ecPhlInline.mli +++ b/src/phl/ecPhlInline.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 5f216e7172..8db5956c6d 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlLoopTx.mli b/src/phl/ecPhlLoopTx.mli index 20b457a3a3..85ca2053d0 100644 --- a/src/phl/ecPhlLoopTx.mli +++ b/src/phl/ecPhlLoopTx.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcTypes diff --git a/src/phl/ecPhlPr.ml b/src/phl/ecPhlPr.ml index ac5f1bfa3f..00ff3abc19 100644 --- a/src/phl/ecPhlPr.ml +++ b/src/phl/ecPhlPr.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcModules diff --git a/src/phl/ecPhlPr.mli b/src/phl/ecPhlPr.mli index fe80140b5d..82f15ef2b8 100644 --- a/src/phl/ecPhlPr.mli +++ b/src/phl/ecPhlPr.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlPrRw.ml b/src/phl/ecPhlPrRw.ml index 0e58567166..117c879e9d 100644 --- a/src/phl/ecPhlPrRw.ml +++ b/src/phl/ecPhlPrRw.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcFol diff --git a/src/phl/ecPhlPrRw.mli b/src/phl/ecPhlPrRw.mli index d5fd0439db..64a50ad4cf 100644 --- a/src/phl/ecPhlPrRw.mli +++ b/src/phl/ecPhlPrRw.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcCoreGoal diff --git a/src/phl/ecPhlRCond.ml b/src/phl/ecPhlRCond.ml index 1f2c32aaa0..9a31673047 100644 --- a/src/phl/ecPhlRCond.ml +++ b/src/phl/ecPhlRCond.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcIdent diff --git a/src/phl/ecPhlRCond.mli b/src/phl/ecPhlRCond.mli index dfbbbfd761..b2ec5a9d04 100644 --- a/src/phl/ecPhlRCond.mli +++ b/src/phl/ecPhlRCond.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcSymbols open EcParsetree diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index 9cf983fa07..91a19a901a 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlRnd.mli b/src/phl/ecPhlRnd.mli index 591fbab45b..59799db715 100644 --- a/src/phl/ecPhlRnd.mli +++ b/src/phl/ecPhlRnd.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlSkip.ml b/src/phl/ecPhlSkip.ml index b6c5e7d1c1..66b807b9b2 100644 --- a/src/phl/ecPhlSkip.ml +++ b/src/phl/ecPhlSkip.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcModules diff --git a/src/phl/ecPhlSkip.mli b/src/phl/ecPhlSkip.mli index 6b7b6fd075..63be825063 100644 --- a/src/phl/ecPhlSkip.mli +++ b/src/phl/ecPhlSkip.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcCoreGoal diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index f984241eb7..7e314f3db3 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/phl/ecPhlSp.mli b/src/phl/ecPhlSp.mli index c05efda464..80b9a6abb9 100644 --- a/src/phl/ecPhlSp.mli +++ b/src/phl/ecPhlSp.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcCoreGoal.FApi diff --git a/src/phl/ecPhlSwap.ml b/src/phl/ecPhlSwap.ml index 9473b41f36..231357a31e 100644 --- a/src/phl/ecPhlSwap.ml +++ b/src/phl/ecPhlSwap.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlSwap.mli b/src/phl/ecPhlSwap.mli index bf1ced64de..68fe1ef3b4 100644 --- a/src/phl/ecPhlSwap.mli +++ b/src/phl/ecPhlSwap.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcLocation open EcParsetree diff --git a/src/phl/ecPhlSym.ml b/src/phl/ecPhlSym.ml index 73fe7e4def..898d5349f1 100644 --- a/src/phl/ecPhlSym.ml +++ b/src/phl/ecPhlSym.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (*-------------------------------------------------------------------- *) open EcFol open EcCoreGoal diff --git a/src/phl/ecPhlSym.mli b/src/phl/ecPhlSym.mli index ac68f8a35f..eaa3b44811 100644 --- a/src/phl/ecPhlSym.mli +++ b/src/phl/ecPhlSym.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcCoreGoal.FApi diff --git a/src/phl/ecPhlTAuto.ml b/src/phl/ecPhlTAuto.ml index 2a16e5cf21..28e9be1938 100644 --- a/src/phl/ecPhlTAuto.ml +++ b/src/phl/ecPhlTAuto.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcFol diff --git a/src/phl/ecPhlTAuto.mli b/src/phl/ecPhlTAuto.mli index 1e356628d9..e829f4a609 100644 --- a/src/phl/ecPhlTAuto.mli +++ b/src/phl/ecPhlTAuto.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcCoreGoal.FApi diff --git a/src/phl/ecPhlTrans.ml b/src/phl/ecPhlTrans.ml index a561bbed98..6b9a9a1739 100644 --- a/src/phl/ecPhlTrans.ml +++ b/src/phl/ecPhlTrans.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlTrans.mli b/src/phl/ecPhlTrans.mli index 9b58f54f3f..328daaa45c 100644 --- a/src/phl/ecPhlTrans.mli +++ b/src/phl/ecPhlTrans.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcCoreGoal.FApi diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index 4ca819219f..90fe24fe3b 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcTypes diff --git a/src/phl/ecPhlWhile.mli b/src/phl/ecPhlWhile.mli index 04d63d633e..da245968cf 100644 --- a/src/phl/ecPhlWhile.mli +++ b/src/phl/ecPhlWhile.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree open EcFol diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml index 7c8d1f39c2..6cc46ad33d 100644 --- a/src/phl/ecPhlWp.ml +++ b/src/phl/ecPhlWp.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcUtils open EcParsetree diff --git a/src/phl/ecPhlWp.mli b/src/phl/ecPhlWp.mli index 23d8bb5f29..cd2e573dc1 100644 --- a/src/phl/ecPhlWp.mli +++ b/src/phl/ecPhlWp.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) open EcParsetree diff --git a/src/system/XDG.ml b/src/system/XDG.ml index f3cb6e0e13..c9c3bd8dd7 100644 --- a/src/system/XDG.ml +++ b/src/system/XDG.ml @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type path = string diff --git a/src/system/XDG.mli b/src/system/XDG.mli index e632dd55d2..81220a30b9 100644 --- a/src/system/XDG.mli +++ b/src/system/XDG.mli @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-C-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type path = string diff --git a/theories/algebra/Bigalg.ec b/theories/algebra/Bigalg.ec index 9994d66f10..d874c0b66c 100644 --- a/theories/algebra/Bigalg.ec +++ b/theories/algebra/Bigalg.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - pragma +implicits. (* -------------------------------------------------------------------- *) diff --git a/theories/algebra/Bigop.eca b/theories/algebra/Bigop.eca index 7f79f891e8..2d17cbc361 100644 --- a/theories/algebra/Bigop.eca +++ b/theories/algebra/Bigop.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* This API has been mostly inspired from the [bigop] library of the * ssreflect Coq extension. *) diff --git a/theories/algebra/Binomial.ec b/theories/algebra/Binomial.ec index 9b09127af4..4a2689cd2d 100644 --- a/theories/algebra/Binomial.ec +++ b/theories/algebra/Binomial.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Ring StdBigop StdOrder. (*---*) import Bigint IntOrder. diff --git a/theories/algebra/Group.ec b/theories/algebra/Group.ec index 4f92a784ff..366bc092d0 100644 --- a/theories/algebra/Group.ec +++ b/theories/algebra/Group.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List IntMin IntDiv. require import FinType. diff --git a/theories/algebra/Ideal.ec b/theories/algebra/Ideal.ec index b9fe155ee6..f4d4e96f42 100644 --- a/theories/algebra/Ideal.ec +++ b/theories/algebra/Ideal.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Ring StdOrder Quotient Bigalg Binomial. (*---*) import IntOrder. diff --git a/theories/algebra/IntDiv.ec b/theories/algebra/IntDiv.ec index 258bcc439b..742de63b14 100644 --- a/theories/algebra/IntDiv.ec +++ b/theories/algebra/IntDiv.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Core Int IntMin Ring StdOrder. (*---*) import Ring.IntID IntOrder. diff --git a/theories/algebra/Matrix.eca b/theories/algebra/Matrix.eca index c75f0981dc..c415634a2f 100644 --- a/theories/algebra/Matrix.eca +++ b/theories/algebra/Matrix.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Distr Perms. require (*--*) Subtype Monoid Ring Subtype Bigalg StdOrder StdBigop. diff --git a/theories/algebra/Monoid.eca b/theories/algebra/Monoid.eca index e16bfb5473..80176d5313 100644 --- a/theories/algebra/Monoid.eca +++ b/theories/algebra/Monoid.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Int. (* -------------------------------------------------------------------- *) diff --git a/theories/algebra/Number.ec b/theories/algebra/Number.ec index 0ead8fb4d4..41c7500261 100644 --- a/theories/algebra/Number.ec +++ b/theories/algebra/Number.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore. require (*--*) Ring StdRing. diff --git a/theories/algebra/Perms.ec b/theories/algebra/Perms.ec index 39e4b9e26e..fafe5cdea9 100644 --- a/theories/algebra/Perms.ec +++ b/theories/algebra/Perms.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List IntDiv Binomial Ring StdOrder. (*---*) import IntID IntOrder. diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 868fe71294..9037674793 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Finite Distr DList List. require import Ring Bigalg StdBigop StdOrder. diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec index 2049513eac..e79679b382 100644 --- a/theories/algebra/Ring.ec +++ b/theories/algebra/Ring.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - pragma +implicits. (* -------------------------------------------------------------------- *) diff --git a/theories/algebra/StdBigop.ec b/theories/algebra/StdBigop.ec index 91c63d6ba6..e30e89855a 100644 --- a/theories/algebra/StdBigop.ec +++ b/theories/algebra/StdBigop.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore IntDiv Ring List StdRing StdOrder. require (*--*) Bigop Bigalg. diff --git a/theories/algebra/StdOrder.ec b/theories/algebra/StdOrder.ec index d23ab63217..bff2baab82 100644 --- a/theories/algebra/StdOrder.ec +++ b/theories/algebra/StdOrder.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Ring StdRing. require (*--*) Number. diff --git a/theories/algebra/StdRing.ec b/theories/algebra/StdRing.ec index 711a52ff80..492b821268 100644 --- a/theories/algebra/StdRing.ec +++ b/theories/algebra/StdRing.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Bool Int Real. require (*--*) Ring. diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec index b1b2a58a0c..cfefa518c3 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import List Distr Int IntDiv. require (*--*) Subtype Ring StdOrder. diff --git a/theories/analysis/RealExp.ec b/theories/analysis/RealExp.ec index 04be3ddfd1..6902233676 100644 --- a/theories/analysis/RealExp.ec +++ b/theories/analysis/RealExp.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore StdRing StdOrder RealFun. require import FinType. diff --git a/theories/analysis/RealFLub.ec b/theories/analysis/RealFLub.ec index d16741e35d..a3359c8a80 100644 --- a/theories/analysis/RealFLub.ec +++ b/theories/analysis/RealFLub.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Bool StdRing StdOrder RealLub. (*---*) import RField RealOrder. diff --git a/theories/analysis/RealFun.ec b/theories/analysis/RealFun.ec index 3817a9f111..eb82376698 100644 --- a/theories/analysis/RealFun.ec +++ b/theories/analysis/RealFun.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Bool AllCore StdRing StdOrder. (*---*) import RField RealOrder. diff --git a/theories/analysis/RealLub.ec b/theories/analysis/RealLub.ec index 045fa753e7..2aff402ed2 100644 --- a/theories/analysis/RealLub.ec +++ b/theories/analysis/RealLub.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Bool StdRing StdOrder. (*---*) import RField RealOrder. diff --git a/theories/analysis/RealSeq.ec b/theories/analysis/RealSeq.ec index a279a4af4b..2d32ea6930 100644 --- a/theories/analysis/RealSeq.ec +++ b/theories/analysis/RealSeq.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Bool Ring StdRing StdOrder StdBigop List. (*---*) import IterOp Bigreal.BRA IntID RField IntOrder RealOrder. diff --git a/theories/analysis/RealSeries.ec b/theories/analysis/RealSeries.ec index 39e6bef30c..959a9faaa5 100644 --- a/theories/analysis/RealSeries.ec +++ b/theories/analysis/RealSeries.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Bool AllCore List Finite Discrete. require import StdRing StdOrder StdBigop RealLub RealSeq. diff --git a/theories/core/AllCore.ec b/theories/core/AllCore.ec index eb29e10e15..b97984e499 100644 --- a/theories/core/AllCore.ec +++ b/theories/core/AllCore.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require (*--*) Ring. require export Core Int Real Xint. diff --git a/theories/core/Bool.ec b/theories/core/Bool.ec index 2a80bb7d5c..882c12c0b1 100644 --- a/theories/core/Bool.ec +++ b/theories/core/Bool.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Int Xint. require import FinType. diff --git a/theories/core/Core.ec b/theories/core/Core.ec index d18a408e14..bb220e1f81 100644 --- a/theories/core/Core.ec +++ b/theories/core/Core.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) lemma nosmt pw_eq ['a 'b] (x x' : 'a) (y y' : 'b): x = x' => y = y' => (x, y) = (x', y'). diff --git a/theories/core/CoreInt.ec b/theories/core/CoreInt.ec index d915106348..45ab812916 100644 --- a/theories/core/CoreInt.ec +++ b/theories/core/CoreInt.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) op zero : int = 0. op one : int = 1. diff --git a/theories/core/CoreMap.ec b/theories/core/CoreMap.ec index a5889a1731..ae7faed3a7 100644 --- a/theories/core/CoreMap.ec +++ b/theories/core/CoreMap.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* The only purposes of these types and operators are to be bound to * the relevant SMT operators. Do not use them directly and use the * Map theory instead. *) diff --git a/theories/core/CoreReal.ec b/theories/core/CoreReal.ec index 8c48140bfd..107a97ab1d 100644 --- a/theories/core/CoreReal.ec +++ b/theories/core/CoreReal.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) op from_int: int -> real. op zero = from_int 0. diff --git a/theories/crypto/AdvAbsVal.ec b/theories/crypto/AdvAbsVal.ec index 713800c722..4ec0e782c7 100644 --- a/theories/crypto/AdvAbsVal.ec +++ b/theories/crypto/AdvAbsVal.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Real. module type Adv = { diff --git a/theories/crypto/Birthday.ec b/theories/crypto/Birthday.ec index 19b1721117..3bd89f0a77 100644 --- a/theories/crypto/Birthday.ec +++ b/theories/crypto/Birthday.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Distr Ring. require import StdRing StdOrder StdBigop FelTactic. diff --git a/theories/crypto/Commitment.ec b/theories/crypto/Commitment.ec index 32ef4f4a0e..5581a4020c 100644 --- a/theories/crypto/Commitment.ec +++ b/theories/crypto/Commitment.ec @@ -1,9 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2016--2017 - Roberto Metere - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* A formalisation of generic commitment schemes *) require import DBool. diff --git a/theories/crypto/DLog.ec b/theories/crypto/DLog.ec index 0e0bd4c3f0..e6f1d94686 100644 --- a/theories/crypto/DLog.ec +++ b/theories/crypto/DLog.ec @@ -1,9 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2016--2017 - Roberto Metere - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* A formalisation of the discrete logarithm assumption. *) require import CyclicGroup. diff --git a/theories/crypto/DiffieHellman.ec b/theories/crypto/DiffieHellman.ec index db68ad23c2..ab2e17076f 100644 --- a/theories/crypto/DiffieHellman.ec +++ b/theories/crypto/DiffieHellman.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore StdRing StdOrder Distr List FSet CHoareTactic. (*---*) import RField RealOrder. require (* *) CyclicGroup. diff --git a/theories/crypto/LorR.eca b/theories/crypto/LorR.eca index 65015947c8..6278f76e71 100644 --- a/theories/crypto/LorR.eca +++ b/theories/crypto/LorR.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore Distr DBool. type input. diff --git a/theories/crypto/MAC.ec b/theories/crypto/MAC.ec index 47f245f25d..a279223b51 100644 --- a/theories/crypto/MAC.ec +++ b/theories/crypto/MAC.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import FSet. type key. diff --git a/theories/crypto/OW.ec b/theories/crypto/OW.ec index 712720610f..c2c7a4048d 100644 --- a/theories/crypto/OW.ec +++ b/theories/crypto/OW.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* One-Way Trapdoor Permutations *) require import Core Distr. diff --git a/theories/crypto/PKE.ec b/theories/crypto/PKE.ec index 580c24868d..94985334c5 100644 --- a/theories/crypto/PKE.ec +++ b/theories/crypto/PKE.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List Distr DBool. require LorR. diff --git a/theories/crypto/PKS.ec b/theories/crypto/PKS.ec index 622b235484..abd455570c 100644 --- a/theories/crypto/PKS.ec +++ b/theories/crypto/PKS.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* Definitions for Public-Key Signatures Schemes *) require import FSet. diff --git a/theories/crypto/PRF.eca b/theories/crypto/PRF.eca index 4843863b1c..120c547f15 100644 --- a/theories/crypto/PRF.eca +++ b/theories/crypto/PRF.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore Distr FSet. pragma +implicits. diff --git a/theories/crypto/PRG.eca b/theories/crypto/PRG.eca index 8ee9f98a22..bf49b35314 100644 --- a/theories/crypto/PRG.eca +++ b/theories/crypto/PRG.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (*** A formalization of pseudo-random generators **) (** A stateful random generator for type output is a pair of diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec index 1851629e2d..41fa741782 100644 --- a/theories/crypto/PROM.ec +++ b/theories/crypto/PROM.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - pragma +implicits. (* -------------------------------------------------------------------- *) diff --git a/theories/crypto/PRP.eca b/theories/crypto/PRP.eca index 70a14b4f14..517aa92fe8 100644 --- a/theories/crypto/PRP.eca +++ b/theories/crypto/PRP.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore Distr. pragma +implicits. diff --git a/theories/crypto/ROM.eca b/theories/crypto/ROM.eca index a837a0d4fe..2e7735e1c2 100644 --- a/theories/crypto/ROM.eca +++ b/theories/crypto/ROM.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - pragma +implicits. require import AllCore Distr. diff --git a/theories/crypto/RndExcept.eca b/theories/crypto/RndExcept.eca index 784eaed783..0b7bccc13c 100644 --- a/theories/crypto/RndExcept.eca +++ b/theories/crypto/RndExcept.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List Distr Dexcepted FelTactic. require import StdOrder StdBigop. import RealOrder Bigreal. diff --git a/theories/crypto/SecureChannels.ec b/theories/crypto/SecureChannels.ec index d01aa8ef40..22588088e7 100644 --- a/theories/crypto/SecureChannels.ec +++ b/theories/crypto/SecureChannels.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Bool Core Int FSet DBool. type key. diff --git a/theories/crypto/SigmaProtocol.ec b/theories/crypto/SigmaProtocol.ec index d599173017..7c537d1ea6 100644 --- a/theories/crypto/SigmaProtocol.ec +++ b/theories/crypto/SigmaProtocol.ec @@ -1,9 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2016--2017 - Roberto Metere - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* A formalisation of generic Sigma protocols *) require import DBool. require import Int. diff --git a/theories/crypto/SplitRO.ec b/theories/crypto/SplitRO.ec index ff860429c2..e5659fadb6 100644 --- a/theories/crypto/SplitRO.ec +++ b/theories/crypto/SplitRO.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore PROM SmtMap Distr DProd. abstract theory Split. diff --git a/theories/crypto/SymmetricEncryption.ec b/theories/crypto/SymmetricEncryption.ec index 34861b8995..aeee281ba8 100644 --- a/theories/crypto/SymmetricEncryption.ec +++ b/theories/crypto/SymmetricEncryption.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Bool Core List DBool. type key. diff --git a/theories/crypto/assumptions/AEAD.ec b/theories/crypto/assumptions/AEAD.ec index b0d6e24b9c..5775edd215 100644 --- a/theories/crypto/assumptions/AEAD.ec +++ b/theories/crypto/assumptions/AEAD.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List FSet SmtMap Distr DBool DList. (*require import AllCore Distr FSet SmtMap DBool. *) diff --git a/theories/crypto/assumptions/CRHash.ec b/theories/crypto/assumptions/CRHash.ec index e12709dacb..94a57a9caf 100644 --- a/theories/crypto/assumptions/CRHash.ec +++ b/theories/crypto/assumptions/CRHash.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore FSet SmtMap Distr. (* Formalisation of collision resistance: CR : Collision resistance game diff --git a/theories/crypto/assumptions/DHIES.ec b/theories/crypto/assumptions/DHIES.ec index 2ae4fde0ba..f4f23b77f6 100644 --- a/theories/crypto/assumptions/DHIES.ec +++ b/theories/crypto/assumptions/DHIES.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore FSet CoreMap SmtMap CyclicGroup List. require import Distr DList DJoin DMap StdOrder. require import AEAD. diff --git a/theories/crypto/assumptions/MRPKE.ec b/theories/crypto/assumptions/MRPKE.ec index ce9bb6106f..729453bfb7 100644 --- a/theories/crypto/assumptions/MRPKE.ec +++ b/theories/crypto/assumptions/MRPKE.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore FSet List SmtMap Distr DBool. (*******************************************) diff --git a/theories/crypto/assumptions/ODH.ec b/theories/crypto/assumptions/ODH.ec index 4a3e83cfa3..d5eee590e6 100644 --- a/theories/crypto/assumptions/ODH.ec +++ b/theories/crypto/assumptions/ODH.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import CyclicGroup DBool SmtMap FSet DList Int List. (* Multiple Oracle-DH *) diff --git a/theories/crypto/assumptions/PKSMK.ec b/theories/crypto/assumptions/PKSMK.ec index ededacfec3..645bde4024 100644 --- a/theories/crypto/assumptions/PKSMK.ec +++ b/theories/crypto/assumptions/PKSMK.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore Distr DInterval FSet List SmtMap. require PROM PlugAndPray. diff --git a/theories/crypto/pke/PKE_CPA.eca b/theories/crypto/pke/PKE_CPA.eca index 05a6c6d509..f73de9595d 100644 --- a/theories/crypto/pke/PKE_CPA.eca +++ b/theories/crypto/pke/PKE_CPA.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Bool Core Int List. require import DBool. diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca index 7c04276285..586223fcce 100644 --- a/theories/crypto/prp_prf/Strong_RP_RF.eca +++ b/theories/crypto/prp_prf/Strong_RP_RF.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore Distr List FSet SmtMap. require import Dexcepted. require (*--*) PRP. diff --git a/theories/crypto/ske/CCA.eca b/theories/crypto/ske/CCA.eca index 9dd09b9391..2cf53d06cd 100644 --- a/theories/crypto/ske/CCA.eca +++ b/theories/crypto/ske/CCA.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Bool Core FSet. require (*--*) DBool NewSKE. diff --git a/theories/crypto/ske/CCA1.eca b/theories/crypto/ske/CCA1.eca index 1309345825..dd02942c5f 100644 --- a/theories/crypto/ske/CCA1.eca +++ b/theories/crypto/ske/CCA1.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Bool Core. require (*--*) DBool NewSKE. diff --git a/theories/crypto/ske/CPA.eca b/theories/crypto/ske/CPA.eca index b5ded6e2df..1ce880dbb7 100644 --- a/theories/crypto/ske/CPA.eca +++ b/theories/crypto/ske/CPA.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Bool Core. require (*--*) DBool NewSKE. diff --git a/theories/crypto/ske/NewSKE.eca b/theories/crypto/ske/NewSKE.eca index ddea80a57a..d56ed958f0 100644 --- a/theories/crypto/ske/NewSKE.eca +++ b/theories/crypto/ske/NewSKE.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Bool FSet SmtMap. type key, plain, cipher. diff --git a/theories/datatypes/Array.ec b/theories/datatypes/Array.ec index 923ff62b29..b3a96c8514 100644 --- a/theories/datatypes/Array.ec +++ b/theories/datatypes/Array.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List. diff --git a/theories/datatypes/BitEncoding.ec b/theories/datatypes/BitEncoding.ec index 7fe240fb5a..64a6c50be3 100644 --- a/theories/datatypes/BitEncoding.ec +++ b/theories/datatypes/BitEncoding.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Bool AllCore IntDiv List Ring StdRing StdOrder StdBigop. require (*--*) FinType Word. diff --git a/theories/datatypes/BitWord.eca b/theories/datatypes/BitWord.eca index c6655e3d05..f68bea0cad 100644 --- a/theories/datatypes/BitWord.eca +++ b/theories/datatypes/BitWord.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Bool Core Int Xint List. require (*--*) FinType Word Ring. diff --git a/theories/datatypes/FSet.ec b/theories/datatypes/FSet.ec index 19cf68679a..a50c3aa9f0 100644 --- a/theories/datatypes/FSet.ec +++ b/theories/datatypes/FSet.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Core Int List StdRing StdOrder. (*---*) import IntOrder. diff --git a/theories/datatypes/FloorCeil.ec b/theories/datatypes/FloorCeil.ec index 49d56e2b42..3527531a95 100644 --- a/theories/datatypes/FloorCeil.ec +++ b/theories/datatypes/FloorCeil.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Ring StdRing StdOrder. (*---*) import RField IntOrder RealOrder. diff --git a/theories/datatypes/Int.ec b/theories/datatypes/Int.ec index 7353575bb0..0ef5af3955 100644 --- a/theories/datatypes/Int.ec +++ b/theories/datatypes/Int.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require CoreInt. diff --git a/theories/datatypes/IntMin.ec b/theories/datatypes/IntMin.ec index 3dd2c52881..cb19b0578b 100644 --- a/theories/datatypes/IntMin.ec +++ b/theories/datatypes/IntMin.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Int. require (*--*) Ring StdOrder. diff --git a/theories/datatypes/List.ec b/theories/datatypes/List.ec index fd919ffc6b..35142879f4 100644 --- a/theories/datatypes/List.ec +++ b/theories/datatypes/List.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* This API has been mostly inspired from the [seq] library of the * ssreflect Coq extension. *) diff --git a/theories/datatypes/Real.ec b/theories/datatypes/Real.ec index 94fecd7155..b4f3644fed 100644 --- a/theories/datatypes/Real.ec +++ b/theories/datatypes/Real.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Int Ring AlgTactic CoreReal. diff --git a/theories/datatypes/Tuple.eca b/theories/datatypes/Tuple.eca index f12604f182..3be293d385 100644 --- a/theories/datatypes/Tuple.eca +++ b/theories/datatypes/Tuple.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List StdOrder StdBigop. (*---*) import StdOrder.IntOrder StdBigop.Bigint.BIA. diff --git a/theories/datatypes/Word.eca b/theories/datatypes/Word.eca index bc2e907a13..758424e07e 100644 --- a/theories/datatypes/Word.eca +++ b/theories/datatypes/Word.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Distr StdOrder. require import FinType. diff --git a/theories/distributions/DBool.ec b/theories/distributions/DBool.ec index 0f9a951721..40e30b5557 100644 --- a/theories/distributions/DBool.ec +++ b/theories/distributions/DBool.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Distr Ring Number. require import StdRing StdOrder StdBigop RealSeq RealSeries. diff --git a/theories/distributions/DInterval.ec b/theories/distributions/DInterval.ec index 45093d6364..585f23b738 100644 --- a/theories/distributions/DInterval.ec +++ b/theories/distributions/DInterval.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List StdBigop StdOrder IntDiv Distr. (*---*) import IntOrder Bigint MUniform Range. diff --git a/theories/distributions/DJoin.ec b/theories/distributions/DJoin.ec index a5bbd12018..47d7fabe6c 100644 --- a/theories/distributions/DJoin.ec +++ b/theories/distributions/DJoin.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Distr Ring StdBigop StdRing StdOrder. (*---*) import IntID Bigreal Bigreal.BRM. diff --git a/theories/distributions/DList.ec b/theories/distributions/DList.ec index 8226e65ba3..a3eef8e71a 100644 --- a/theories/distributions/DList.ec +++ b/theories/distributions/DList.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List FSet Distr DProd StdBigop. (*---*) import Bigreal Bigreal.BRM MUnit. diff --git a/theories/distributions/DMap.ec b/theories/distributions/DMap.ec index 1dec1946b2..18509255ec 100644 --- a/theories/distributions/DMap.ec +++ b/theories/distributions/DMap.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Distr. diff --git a/theories/distributions/DProd.ec b/theories/distributions/DProd.ec index 442c4eb492..4d373950bb 100644 --- a/theories/distributions/DProd.ec +++ b/theories/distributions/DProd.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List StdOrder Distr StdOrder. (*---*) import RealOrder RealSeries StdBigop.Bigreal BRA. diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec index 626d612dba..2da549f4e0 100644 --- a/theories/distributions/Dexcepted.ec +++ b/theories/distributions/Dexcepted.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Distr FSet Dfilter StdRing. (*---*) import RField StdOrder.RealOrder. diff --git a/theories/distributions/Dfilter.ec b/theories/distributions/Dfilter.ec index 6f30af1b7f..a26f79dafd 100644 --- a/theories/distributions/Dfilter.ec +++ b/theories/distributions/Dfilter.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore Distr FSet StdRing StdOrder StdBigop. (*---*) import RField RealOrder Bigreal BRA. diff --git a/theories/distributions/Distr.ec b/theories/distributions/Distr.ec index d6b4c6788d..5246808850 100644 --- a/theories/distributions/Distr.ec +++ b/theories/distributions/Distr.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* * This file contains a formalization of (discrete) distributions * diff --git a/theories/distributions/Mu_mem.ec b/theories/distributions/Mu_mem.ec index ac97d204f8..001cd54e33 100644 --- a/theories/distributions/Mu_mem.ec +++ b/theories/distributions/Mu_mem.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List FSet Distr. require import Ring Number StdRing StdOrder. diff --git a/theories/distributions/SDist.ec b/theories/distributions/SDist.ec index 172b327d5a..f3c9d57603 100644 --- a/theories/distributions/SDist.ec +++ b/theories/distributions/SDist.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List FSet Distr DProd DList StdBigop StdOrder RealFLub. require import Hybrid. (*---*) import Bigreal RealSeries RealOrder RField BRA MRat. diff --git a/theories/encryption/DDH_hybrid.ec b/theories/encryption/DDH_hybrid.ec index 9c31603b2e..e301e5db0e 100644 --- a/theories/encryption/DDH_hybrid.ec +++ b/theories/encryption/DDH_hybrid.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Real. require import Int IntDiv. require import Prime_field. diff --git a/theories/encryption/Hybrid.ec b/theories/encryption/Hybrid.ec index b9718894cf..4242501088 100644 --- a/theories/encryption/Hybrid.ec +++ b/theories/encryption/Hybrid.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List Finite Distr DInterval. require (*--*) Means StdOrder. (*---*) import StdBigop.Bigreal.BRA. diff --git a/theories/encryption/Indist.ec b/theories/encryption/Indist.ec index 9a08a31fc7..d5aac33019 100644 --- a/theories/encryption/Indist.ec +++ b/theories/encryption/Indist.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore FSet Distr SampleBool. require DBool Hybrid. diff --git a/theories/encryption/Means.ec b/theories/encryption/Means.ec index 2c6b6cf0e8..48beb22a62 100644 --- a/theories/encryption/Means.ec +++ b/theories/encryption/Means.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List Distr. require import Finite. require (*--*) StdBigop. diff --git a/theories/encryption/PKE_hybrid.ec b/theories/encryption/PKE_hybrid.ec index cda933e85f..4934a61bb7 100644 --- a/theories/encryption/PKE_hybrid.ec +++ b/theories/encryption/PKE_hybrid.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List FSet Finite Distr DInterval. require import Indist. require import CHoareTactic. diff --git a/theories/encryption/SampleBool.ec b/theories/encryption/SampleBool.ec index ac086cd7e9..2e316bfda2 100644 --- a/theories/encryption/SampleBool.ec +++ b/theories/encryption/SampleBool.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List Finite Real Distr. require DBool. diff --git a/theories/looping/FoldProc.eca b/theories/looping/FoldProc.eca index 1e51ff88ef..035bc98a3f 100644 --- a/theories/looping/FoldProc.eca +++ b/theories/looping/FoldProc.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Core List. require (*--*) IterProc. diff --git a/theories/looping/IterProc.eca b/theories/looping/IterProc.eca index 989a5fa14c..5bef3bab05 100644 --- a/theories/looping/IterProc.eca +++ b/theories/looping/IterProc.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Core List. type t. diff --git a/theories/modules/EventPartitioning.ec b/theories/modules/EventPartitioning.ec index bc5b54252f..ef34230d29 100644 --- a/theories/modules/EventPartitioning.ec +++ b/theories/modules/EventPartitioning.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List Distr StdBigop StdRing StdOrder. (*---*) import Bigreal BRA RField IntOrder RealOrder. diff --git a/theories/modules/PlugAndPray.eca b/theories/modules/PlugAndPray.eca index c3a40e92f0..63c81f0d72 100644 --- a/theories/modules/PlugAndPray.eca +++ b/theories/modules/PlugAndPray.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore List Distr. type tval. diff --git a/theories/modules/Pr_half.eca b/theories/modules/Pr_half.eca index 3158ab36d3..862b065dbe 100644 --- a/theories/modules/Pr_half.eca +++ b/theories/modules/Pr_half.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore Distr. type input. diff --git a/theories/modules/RndProd.eca b/theories/modules/RndProd.eca index bf1809a54f..8a57259253 100644 --- a/theories/modules/RndProd.eca +++ b/theories/modules/RndProd.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Distr DProd SmtMap. require (****) PROM. diff --git a/theories/newth/SmtMap.ec b/theories/newth/SmtMap.ec index 18b137da41..637cf74799 100644 --- a/theories/newth/SmtMap.ec +++ b/theories/newth/SmtMap.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import AllCore CoreMap Finite List FSet Ring StdOrder. (*---*) import IntID IntOrder. diff --git a/theories/oldlibs/CyclicGroup.ec b/theories/oldlibs/CyclicGroup.ec index d33ca4825a..46a6837692 100644 --- a/theories/oldlibs/CyclicGroup.ec +++ b/theories/oldlibs/CyclicGroup.ec @@ -1,10 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) require import Int Xint. require PrimeField. diff --git a/theories/oldlibs/Cyclic_group_prime.ec b/theories/oldlibs/Cyclic_group_prime.ec index 1f8365712b..4ebf182a8a 100644 --- a/theories/oldlibs/Cyclic_group_prime.ec +++ b/theories/oldlibs/Cyclic_group_prime.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* cyclic groups of prime order *) require import Prime_field. require import Real. diff --git a/theories/oldlibs/OldDistr.ec b/theories/oldlibs/OldDistr.ec index 7537c0cb47..5808d571c9 100644 --- a/theories/oldlibs/OldDistr.ec +++ b/theories/oldlibs/OldDistr.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore StdRing StdOrder. (*---*) import RField RealOrder. diff --git a/theories/oldlibs/OldFMap.ec b/theories/oldlibs/OldFMap.ec index 04126aa68a..b3732675e6 100644 --- a/theories/oldlibs/OldFMap.ec +++ b/theories/oldlibs/OldFMap.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Int List FSet. diff --git a/theories/oldlibs/PrimeField.ec b/theories/oldlibs/PrimeField.ec index cba12d9a45..b82a7ef217 100644 --- a/theories/oldlibs/PrimeField.ec +++ b/theories/oldlibs/PrimeField.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require Int IntDiv. require import Xint. diff --git a/theories/oldlibs/Prime_field.ec b/theories/oldlibs/Prime_field.ec index afd394dddc..5c7fa14e60 100644 --- a/theories/oldlibs/Prime_field.ec +++ b/theories/oldlibs/Prime_field.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* prime fields GF(q) for q prime *) require Int. diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec index 14f98cce9c..2823b11674 100644 --- a/theories/prelude/Logic.ec +++ b/theories/prelude/Logic.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import Tactics. diff --git a/theories/prelude/Pervasive.ec b/theories/prelude/Pervasive.ec index afd940760a..5b7826e9af 100644 --- a/theories/prelude/Pervasive.ec +++ b/theories/prelude/Pervasive.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) type unit. diff --git a/theories/prelude/Tactics.ec b/theories/prelude/Tactics.ec index 542c3c09e0..862a664bb0 100644 --- a/theories/prelude/Tactics.ec +++ b/theories/prelude/Tactics.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) lemma nosmt unitW (P : unit -> bool): P tt => forall x, P x by []. diff --git a/theories/query_counting/Counter.eca b/theories/query_counting/Counter.eca index 22f9ea9ed6..23dcd08f8b 100644 --- a/theories/query_counting/Counter.eca +++ b/theories/query_counting/Counter.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Int Real Distr StdOrder. (*---*) import RealOrder. diff --git a/theories/query_counting/OracleBounds.ec b/theories/query_counting/OracleBounds.ec index 5740066016..7df552317b 100644 --- a/theories/query_counting/OracleBounds.ec +++ b/theories/query_counting/OracleBounds.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require import Int Real Distr StdOrder. (*---*) import RealOrder. diff --git a/theories/structure/Discrete.ec b/theories/structure/Discrete.ec index f1ee30194d..990a1d89e2 100644 --- a/theories/structure/Discrete.ec +++ b/theories/structure/Discrete.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore Ring StdRing StdOrder List Finite. (*---*) import IntID IntOrder. diff --git a/theories/structure/FinType.ec b/theories/structure/FinType.ec index f990bcc77d..f038745558 100644 --- a/theories/structure/FinType.ec +++ b/theories/structure/FinType.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List. diff --git a/theories/structure/Finite.ec b/theories/structure/Finite.ec index 6ffb17b5af..3778dcf8ff 100644 --- a/theories/structure/Finite.ec +++ b/theories/structure/Finite.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List. diff --git a/theories/structure/Quotient.ec b/theories/structure/Quotient.ec index 9449529ea8..ca835d603e 100644 --- a/theories/structure/Quotient.ec +++ b/theories/structure/Quotient.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - require Subtype. pragma +implicits. diff --git a/theories/structure/Subtype.eca b/theories/structure/Subtype.eca index 70f2368440..e7eac465ba 100644 --- a/theories/structure/Subtype.eca +++ b/theories/structure/Subtype.eca @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - pragma +implicits. (* -------------------------------------------------------------------- *) diff --git a/theories/structure/WF.ec b/theories/structure/WF.ec index 9fe631604b..161fa8ddab 100644 --- a/theories/structure/WF.ec +++ b/theories/structure/WF.ec @@ -1,9 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2021-2021 - Boston University - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* An axiom-free formalization of well-founded relations, induction and recursion. diff --git a/theories/tactics/AlgTactic.ec b/theories/tactics/AlgTactic.ec index 4c1cbc9531..3783237928 100644 --- a/theories/tactics/AlgTactic.ec +++ b/theories/tactics/AlgTactic.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) (* Axioms on the ring structure [0, 1, +, -, *] * - 0 != 1 diff --git a/theories/tactics/CHoareTactic.ec b/theories/tactics/CHoareTactic.ec index 5df5d064be..1278cae7b1 100644 --- a/theories/tactics/CHoareTactic.ec +++ b/theories/tactics/CHoareTactic.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2018 - Inria - * Copyright (c) - 2012--2018 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import AllCore List Ring StdOrder StdBigop. require (*--*) Bigop. diff --git a/theories/tactics/FelTactic.ec b/theories/tactics/FelTactic.ec index a16221e568..179d84435a 100644 --- a/theories/tactics/FelTactic.ec +++ b/theories/tactics/FelTactic.ec @@ -1,11 +1,3 @@ -(* -------------------------------------------------------------------- - * Copyright (c) - 2012--2016 - IMDEA Software Institute - * Copyright (c) - 2012--2021 - Inria - * Copyright (c) - 2012--2021 - Ecole Polytechnique - * - * Distributed under the terms of the CeCILL-B-V1 license - * -------------------------------------------------------------------- *) - (* -------------------------------------------------------------------- *) require import FSet StdBigop. (*---*) import Bigreal.