swh:1:snp:f21a40066c2663969c9a5e9a10322d327835126e
- HEAD
- refs/heads/TemplateMonadToTM
- refs/heads/anonymized
- refs/heads/bidirectional
- refs/heads/bidirectional_conversion
- refs/heads/case-representation-bidir
- refs/heads/case-representation-closed
- refs/heads/check-fix
- refs/heads/clean
- refs/heads/clean-ugraph
- refs/heads/complete-conversion
- refs/heads/conv_lemmas
- refs/heads/coq-8.10
- refs/heads/coq-8.11
- refs/heads/coq-8.12
- refs/heads/coq-8.5
- refs/heads/coq-8.6
- refs/heads/coq-8.7
- refs/heads/coq-8.8
- refs/heads/coq-8.9
- refs/heads/correct_check_correct_arity
- refs/heads/dependencies
- refs/heads/double_trans
- refs/heads/erasure-retyping-switch-letpattern-bug
- refs/heads/eta
- refs/heads/eta-equality
- refs/heads/eta_postpo
- refs/heads/ewcbveval-evalfix
- refs/heads/extractable-translation_utils
- refs/heads/extraction_extraction
- refs/heads/generalizing_pred
- refs/heads/gradual-CIC
- refs/heads/infer_complete
- refs/heads/itp-artefact
- refs/heads/master
- refs/heads/master-merge-8.11
- refs/heads/module-path-inequality
- refs/heads/new_repr_univs
- refs/heads/old-unsafe-checker
- refs/heads/pcuic-induction
- refs/heads/pcuic-infer
- refs/heads/pcuic-plugin-fixups
- refs/heads/phd-thesis
- refs/heads/popl-artifact-eval
- refs/heads/quickchick
- refs/heads/remove_pcuic_plugin
- refs/heads/safechecker
- refs/heads/ssr-compat
- refs/heads/tauto
- refs/heads/to_mie
- refs/heads/univalent-parametricity-errors
- refs/heads/univalent-parametricity-errors2
- refs/heads/univalent_parametricity
- refs/heads/wellformed_nlctx
- refs/heads/yannick_axioms
- refs/tags/1.0-alpha+8.8
- refs/tags/1.0-alpha+8.9
- refs/tags/CoqCoqCorrect
- refs/tags/v1.0-alpha2-8.10
- refs/tags/v1.0-alpha2-8.11
- refs/tags/v2.0-beta
- refs/tags/v2.1-beta
- refs/tags/v2.1-beta2
- refs/tags/v2.1-beta3
Cook and download a directory from the Software Heritage Vault
You have requested the cooking of the directory with identifier swh:1:dir:05b6080f6c171473eced3e34a27cdc8538adcce7 into a standard tar.gz archive.
Are you sure you want to continue ?
Download a directory from the Software Heritage Vault
You have requested the download of the directory with identifier swh:1:dir:05b6080f6c171473eced3e34a27cdc8538adcce7 as a standard tar.gz archive.
Are you sure you want to continue ?
Cook and download a revision from the Software Heritage Vault
You have requested the cooking of the history heading to revision with identifier swh:1:rev:19d43e2ba30b7f308c5e3b4613e2b9ec4677a71d into a bare git archive.
Are you sure you want to continue ?
Download a revision from the Software Heritage Vault
You have requested the download of the history heading to revision with identifier swh:1:rev:19d43e2ba30b7f308c5e3b4613e2b9ec4677a71d as a bare git archive.
Are you sure you want to continue ?
Invalid Email !
The provided email is not well-formed.
Download link has expired
The requested archive is no longer available for download from the Software Heritage Vault.
Do you want to cook it again ?
To reference or cite the objects present in the Software Heritage archive, permalinks based on SoftWare Hash IDentifiers (SWHIDs) must be used.
Select below a type of object currently browsed in order to display its associated SWHID and permalink.
WIP updating the proofs
| File | Mode | Size |
|---|---|---|
| gen-src | ||
| src | ||
| theories | ||
| Makefile | -rw-r--r-- | 455 bytes |
| Makefile.coq.local | -rw-r--r-- | 33 bytes |
| Makefile.local | -rw-r--r-- | 144 bytes |
| _CoqProject.in | -rw-r--r-- | 2.0 KB |
| demo.v | -rw-r--r-- | 107 bytes |
| update_plugin.sh | -rwxr-xr-x | 439 bytes |
