swh:1:snp:f21a40066c2663969c9a5e9a10322d327835126e
Tip revision: 69bb96e0476d01ff8aea5f21f83926e9b19a3b0a authored by Matthieu Sozeau on 01 September 2020, 12:36:31 UTC
Merge pull request #457 from maximedenes/fix-refine-order
Merge pull request #457 from maximedenes/fix-refine-order
Tip revision: 69bb96e
| File | Mode | Size |
|---|---|---|
| .gitignore | -rw-r--r-- | 18 bytes |
| Extraction.v | -rw-r--r-- | 3.1 KB |
| PCUICAlpha.v | -rw-r--r-- | 26.5 KB |
| PCUICArities.v | -rw-r--r-- | 29.5 KB |
| PCUICAst.v | -rw-r--r-- | 4.3 KB |
| PCUICAstUtils.v | -rw-r--r-- | 21.2 KB |
| PCUICCSubst.v | -rw-r--r-- | 2.4 KB |
| PCUICChecker.v | -rw-r--r-- | 3.2 KB |
| PCUICCheckerCompleteness.v | -rw-r--r-- | 4.4 KB |
| PCUICClosed.v | -rw-r--r-- | 40.5 KB |
| PCUICConfluence.v | -rw-r--r-- | 102.1 KB |
| PCUICContextConversion.v | -rw-r--r-- | 31.5 KB |
| PCUICContexts.v | -rw-r--r-- | 22.8 KB |
| PCUICConversion.v | -rw-r--r-- | 83.0 KB |
| PCUICCtxShape.v | -rw-r--r-- | 4.4 KB |
| PCUICCumulativity.v | -rw-r--r-- | 7.6 KB |
| PCUICElimination.v | -rw-r--r-- | 32.7 KB |
| PCUICEquality.v | -rw-r--r-- | 44.9 KB |
| PCUICErasedTerm.v | -rw-r--r-- | 1.2 KB |
| PCUICGeneration.v | -rw-r--r-- | 2.1 KB |
| PCUICInduction.v | -rw-r--r-- | 2.2 KB |
| PCUICInductiveInversion.v | -rw-r--r-- | 39.4 KB |
| PCUICInductives.v | -rw-r--r-- | 61.8 KB |
| PCUICInversion.v | -rw-r--r-- | 7.7 KB |
| PCUICLiftSubst.v | -rw-r--r-- | 57.9 KB |
| PCUICLoader.v | -rw-r--r-- | 102 bytes |
| PCUICMetaTheory.v | -rw-r--r-- | 821 bytes |
| PCUICNameless.v | -rw-r--r-- | 52.6 KB |
| PCUICNormal.v | -rw-r--r-- | 3.8 KB |
| PCUICParallelReduction.v | -rw-r--r-- | 92.0 KB |
| PCUICParallelReductionConfluence.v | -rw-r--r-- | 140.4 KB |
| PCUICPosition.v | -rw-r--r-- | 44.2 KB |
| PCUICPretty.v | -rw-r--r-- | 7.0 KB |
| PCUICPrincipality.v | -rw-r--r-- | 27.0 KB |
| PCUICReduction.v | -rw-r--r-- | 47.2 KB |
| PCUICReflect.v | -rw-r--r-- | 12.4 KB |
| PCUICRetyping.v | -rw-r--r-- | 7.0 KB |
| PCUICSN.v | -rw-r--r-- | 10.7 KB |
| PCUICSR.v | -rw-r--r-- | 93.1 KB |
| PCUICSafeLemmata.v | -rw-r--r-- | 43.5 KB |
| PCUICSigmaCalculus.v | -rw-r--r-- | 77.0 KB |
| PCUICSize.v | -rw-r--r-- | 1.1 KB |
| PCUICSpine.v | -rw-r--r-- | 73.1 KB |
| PCUICSubstitution.v | -rw-r--r-- | 105.1 KB |
| PCUICToTemplate.v | -rw-r--r-- | 3.0 KB |
| PCUICToTemplateCorrectness.v | -rw-r--r-- | 25.7 KB |
| PCUICTyping.v | -rw-r--r-- | 67.0 KB |
| PCUICUnivSubst.v | -rw-r--r-- | 5.4 KB |
| PCUICUnivSubstitution.v | -rw-r--r-- | 64.1 KB |
| PCUICUtils.v | -rw-r--r-- | 6.5 KB |
| PCUICValidity.v | -rw-r--r-- | 13.2 KB |
| PCUICWcbvEval.v | -rw-r--r-- | 36.4 KB |
| PCUICWeakening.v | -rw-r--r-- | 47.5 KB |
| PCUICWeakeningEnv.v | -rw-r--r-- | 28.2 KB |
| README.md | -rw-r--r-- | 6.9 KB |
| TemplateToPCUIC.v | -rw-r--r-- | 2.7 KB |
| TemplateToPCUICCorrectness.v | -rw-r--r-- | 46.5 KB |
