https://github.com/EasyCrypt/easycrypt
Revision 98608e4339a7b96cbc0e13c449f6985fc97aaf89 authored by Benjamin Gregoire on 24 March 2021, 03:41:53 UTC, committed by Benjamin Gregoire on 24 March 2021, 03:41:53 UTC
1 parent f5ea5b3
Tip revision: 98608e4339a7b96cbc0e13c449f6985fc97aaf89 authored by Benjamin Gregoire on 24 March 2021, 03:41:53 UTC
fix translation to why3 for operator, where some of its type parameters do not appear in the its type.
fix translation to why3 for operator, where some of its type parameters do not appear in the its type.
Tip revision: 98608e4
File | Mode | Size |
---|---|---|
phl | ||
system | ||
ec.ml | -rw-r--r-- | 13.2 KB |
ecAlgTactic.ml | -rw-r--r-- | 8.5 KB |
ecAlgTactic.mli | -rw-r--r-- | 1.5 KB |
ecAlgebra.ml | -rw-r--r-- | 13.7 KB |
ecAlgebra.mli | -rw-r--r-- | 4.9 KB |
ecBaseLogic.ml | -rw-r--r-- | 842 bytes |
ecBigInt.ml | -rw-r--r-- | 5.0 KB |
ecBigInt.mli | -rw-r--r-- | 390 bytes |
ecBigIntCore.ml | -rw-r--r-- | 2.0 KB |
ecCallbyValue.ml | -rw-r--r-- | 18.0 KB |
ecCallbyValue.mli | -rw-r--r-- | 250 bytes |
ecCommands.ml | -rw-r--r-- | 32.6 KB |
ecCommands.mli | -rw-r--r-- | 2.0 KB |
ecCoreFol.ml | -rw-r--r-- | 53.8 KB |
ecCoreFol.mli | -rw-r--r-- | 14.3 KB |
ecCoreGoal.ml | -rw-r--r-- | 36.3 KB |
ecCoreGoal.mli | -rw-r--r-- | 16.6 KB |
ecCoreHiPhl.ml | -rw-r--r-- | 2.6 KB |
ecCoreHiPhl.mli | -rw-r--r-- | 985 bytes |
ecCoreLib.ml | -rw-r--r-- | 6.5 KB |
ecCoreLib.mli | -rw-r--r-- | 4.7 KB |
ecDecl.ml | -rw-r--r-- | 8.7 KB |
ecDecl.mli | -rw-r--r-- | 4.9 KB |
ecEco.ml | -rw-r--r-- | 5.0 KB |
ecEnv.ml | -rw-r--r-- | 108.2 KB |
ecEnv.mli | -rw-r--r-- | 15.0 KB |
ecField.ml | -rw-r--r-- | 6.3 KB |
ecField.mli | -rw-r--r-- | 882 bytes |
ecFol.ml | -rw-r--r-- | 29.0 KB |
ecFol.mli | -rw-r--r-- | 6.5 KB |
ecFortune.ml | -rw-r--r-- | 1.8 KB |
ecFortune.mli | -rw-r--r-- | 488 bytes |
ecGState.ml | -rw-r--r-- | 4.1 KB |
ecGState.mli | -rw-r--r-- | 1.8 KB |
ecGenRegexp.ml | -rw-r--r-- | 10.5 KB |
ecHiGoal.ml | -rw-r--r-- | 62.7 KB |
ecHiGoal.mli | -rw-r--r-- | 4.2 KB |
ecHiInductive.ml | -rw-r--r-- | 13.0 KB |
ecHiInductive.mli | -rw-r--r-- | 2.3 KB |
ecHiNotations.ml | -rw-r--r-- | 3.8 KB |
ecHiNotations.mli | -rw-r--r-- | 1022 bytes |
ecHiPredicates.ml | -rw-r--r-- | 3.3 KB |
ecHiPredicates.mli | -rw-r--r-- | 924 bytes |
ecHiTacticals.ml | -rw-r--r-- | 14.7 KB |
ecHiTacticals.mli | -rw-r--r-- | 683 bytes |
ecIdent.ml | -rw-r--r-- | 2.0 KB |
ecIdent.mli | -rw-r--r-- | 1.5 KB |
ecInductive.ml | -rw-r--r-- | 9.5 KB |
ecInductive.mli | -rw-r--r-- | 2.7 KB |
ecIo.ml | -rw-r--r-- | 7.1 KB |
ecIo.mli | -rw-r--r-- | 1.3 KB |
ecLexer.mll | -rw-r--r-- | 17.9 KB |
ecLoader.ml | -rw-r--r-- | 5.3 KB |
ecLoader.mli | -rw-r--r-- | 1.2 KB |
ecLocation.ml | -rw-r--r-- | 3.1 KB |
ecLocation.mli | -rw-r--r-- | 1.6 KB |
ecLowGoal.ml | -rw-r--r-- | 82.9 KB |
ecLowGoal.mli | -rw-r--r-- | 11.4 KB |
ecLowPhlGoal.ml | -rw-r--r-- | 21.2 KB |
ecMaps.ml | -rw-r--r-- | 4.1 KB |
ecMatching.ml | -rw-r--r-- | 38.0 KB |
ecMatching.mli | -rw-r--r-- | 6.4 KB |
ecMemory.ml | -rw-r--r-- | 3.8 KB |
ecMemory.mli | -rw-r--r-- | 2.7 KB |
ecModules.ml | -rw-r--r-- | 18.9 KB |
ecModules.mli | -rw-r--r-- | 6.6 KB |
ecOptions.ml | -rw-r--r-- | 14.3 KB |
ecOptions.mli | -rw-r--r-- | 1.8 KB |
ecPException.ml | -rw-r--r-- | 1.7 KB |
ecPException.mli | -rw-r--r-- | 583 bytes |
ecPV.ml | -rw-r--r-- | 32.8 KB |
ecPV.mli | -rw-r--r-- | 6.2 KB |
ecParser.mly | -rw-r--r-- | 88.3 KB |
ecParsetree.ml | -rw-r--r-- | 31.9 KB |
ecPath.ml | -rw-r--r-- | 10.9 KB |
ecPath.mli | -rw-r--r-- | 4.4 KB |
ecPrinting.ml | -rw-r--r-- | 98.5 KB |
ecPrinting.mli | -rw-r--r-- | 4.1 KB |
ecProofTerm.ml | -rw-r--r-- | 30.0 KB |
ecProofTerm.mli | -rw-r--r-- | 6.3 KB |
ecProofTyping.ml | -rw-r--r-- | 7.5 KB |
ecProofTyping.mli | -rw-r--r-- | 3.6 KB |
ecProvers.ml | -rw-r--r-- | 15.0 KB |
ecProvers.mli | -rw-r--r-- | 2.1 KB |
ecReduction.ml | -rw-r--r-- | 45.2 KB |
ecReduction.mli | -rw-r--r-- | 3.4 KB |
ecRegexp.ml | -rw-r--r-- | 4.3 KB |
ecRegexp.mli | -rw-r--r-- | 1.5 KB |
ecRing.ml | -rw-r--r-- | 13.6 KB |
ecRing.mli | -rw-r--r-- | 2.4 KB |
ecScope.ml | -rw-r--r-- | 82.6 KB |
ecScope.mli | -rw-r--r-- | 7.8 KB |
ecSearch.ml | -rw-r--r-- | 3.5 KB |
ecSearch.mli | -rw-r--r-- | 836 bytes |
ecSection.ml | -rw-r--r-- | 14.8 KB |
ecSection.mli | -rw-r--r-- | 1.8 KB |
ecSmt.ml | -rw-r--r-- | 53.0 KB |
ecSmt.mli | -rw-r--r-- | 1.2 KB |
ecStrongRing.ml | -rw-r--r-- | 10.7 KB |
ecSubst.ml | -rw-r--r-- | 20.7 KB |
ecSubst.mli | -rw-r--r-- | 2.5 KB |
ecSymbols.ml | -rw-r--r-- | 2.7 KB |
ecSymbols.mli | -rw-r--r-- | 1.6 KB |
ecTerminal.ml | -rw-r--r-- | 7.6 KB |
ecTerminal.mli | -rw-r--r-- | 1.1 KB |
ecThCloning.ml | -rw-r--r-- | 17.7 KB |
ecThCloning.mli | -rw-r--r-- | 2.6 KB |
ecTheory.ml | -rw-r--r-- | 3.5 KB |
ecTheory.mli | -rw-r--r-- | 3.0 KB |
ecTheoryReplay.ml | -rw-r--r-- | 22.1 KB |
ecTheoryReplay.mli | -rw-r--r-- | 2.1 KB |
ecTransMatching.ml | -rw-r--r-- | 4.1 KB |
ecTransMatching.mli | -rw-r--r-- | 802 bytes |
ecTypeClass.ml | -rw-r--r-- | 2.5 KB |
ecTypeClass.mli | -rw-r--r-- | 841 bytes |
ecTypes.ml | -rw-r--r-- | 30.8 KB |
ecTypes.mli | -rw-r--r-- | 8.6 KB |
ecTyping.ml | -rw-r--r-- | 93.1 KB |
ecTyping.mli | -rw-r--r-- | 7.0 KB |
ecUFind.ml | -rw-r--r-- | 5.6 KB |
ecUFind.mli | -rw-r--r-- | 1.8 KB |
ecUid.ml | -rw-r--r-- | 2.2 KB |
ecUid.mli | -rw-r--r-- | 1.2 KB |
ecUnify.ml | -rw-r--r-- | 14.0 KB |
ecUnify.mli | -rw-r--r-- | 1.9 KB |
ecUserMessages.ml | -rw-r--r-- | 25.8 KB |
ecUserMessages.mli | -rw-r--r-- | 2.7 KB |
ecUtils.ml | -rw-r--r-- | 20.4 KB |
ecUtils.mli | -rw-r--r-- | 11.0 KB |
ecVersion.ml.in | -rw-r--r-- | 801 bytes |
ecVersion.mli | -rw-r--r-- | 598 bytes |
ecWhy3Conv.ml | -rw-r--r-- | 6.4 KB |
ecWhy3Conv.mli | -rw-r--r-- | 645 bytes |
Computing file changes ...