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:0c8ed7cd82e5637db2023da8b9b9e9ae6849af09 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:0c8ed7cd82e5637db2023da8b9b9e9ae6849af09 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:d76226cb3cb1b0f150973ddd8481e9dc8b5ed0f1 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:d76226cb3cb1b0f150973ddd8481e9dc8b5ed0f1 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.
some work on automatic translation from TemplateMonad to TM
| File | Mode | Size |
|---|---|---|
| .gitignore | -rw-r--r-- | 22 bytes |
| g_metacoq_checker.ml4 | -rw-r--r-- | 1.2 KB |
| metacoq_checker_plugin.mlpack | -rw-r--r-- | 106 bytes |
