Skip to main content
  • Home
  • Development
  • Documentation
  • Donate
  • Operational login
  • Browse the archive

swh logo
SoftwareHeritage
Software
Heritage
Archive
Features
  • Search

  • Downloads

  • Save code now

  • Add forge now

  • Help

swh:1:snp:a490b6035923e1853b7217a1b8e3e2fd9c195a6e
  • Code
  • Branches (2)
  • Releases (0)
    • Branches
    • Releases
    • HEAD
    • refs/heads/dev
    • refs/heads/main
    No releases to show
  • 0316bec
  • /
  • _CoqProject
Raw File Download

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.

  • content
  • directory
  • revision
  • snapshot
content badge Iframe embedding
swh:1:cnt:3a846bd8accddd46c59f955d0f1786b7fffe8f18
directory badge Iframe embedding
swh:1:dir:0316becdb6490aaf3f90d4626351c5e52016464e
revision badge
swh:1:rev:0239ae5607dd869ef6ad18aa41b2a27ed5e0ed5d
snapshot badge
swh:1:snp:a490b6035923e1853b7217a1b8e3e2fd9c195a6e

This interface enables to generate software citations, provided that the root directory of browsed objects contains a citation.cff or codemeta.json file.
Select below a type of object currently browsed in order to generate citations for them.

  • content
  • directory
  • revision
  • snapshot
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Tip revision: 0239ae5607dd869ef6ad18aa41b2a27ed5e0ed5d authored by Jarl G. Taxerås Flaten on 10 August 2023, 11:37:38 UTC
add doi to README.md
Tip revision: 0239ae5
_CoqProject
-docroot .
-R /home/jgtf/git/HoTT-master/theories HoTT
-R . Top
-arg -noinit
-arg -indices-matter
-arg -native-compiler -arg no

EquivalenceRelation.v
ES.v
HigherExt.v
Lemmas.v
LES.v
XII_5.v

back to top

Software Heritage — Copyright (C) 2015–2025, The Software Heritage developers. License: GNU AGPLv3+.
The source code of Software Heritage itself is available on our development forge.
The source code files archived by Software Heritage are available under their own copyright and licenses.
Terms of use: Archive access, API— Content policy— Contact— JavaScript license information— Web API