Mentions légales du service

Skip to content
Snippets Groups Projects
Select Git revision
  • case-pf-pose-dependent-metas
  • fix-rlist-import
  • master default protected
  • IZR
  • iota-series
  • coquelicot-2.0
  • ball_norm
  • filterlim_locally
  • new_hierarchy
  • setoid
  • coquelicot-3.0.3
  • coquelicot-3.0.2
  • coquelicot-3.0.1
  • coquelicot-3.0.0
  • coquelicot-2.1.2
  • coquelicot-2.1.1
  • coquelicot-2.1.0
  • coquelicot-2.0.1
  • coquelicot-2.0.0
  • coquelicot-1.1.0
  • coquelicot-1.0.0
21 results
Compare
Forked from Coquelicot / coquelicot
113 commits behind, 1 commit ahead of the upstream repository.
Name Last commit Last update
examples
theories
.gitignore
.mailmap
COPYING
INSTALL.md
NEWS.md
README.md
Remakefile.in
_CoqProject
autogen.sh
configure.in
remake.cpp
README.md

COQUELICOT

This library provides vernacular files containing a formalization of real analysis for the Coq proof assistant. It is a conservative extension of the standard library Reals with a focus on usability.

PROJECT HOME

Homepage: http://coquelicot.saclay.inria.fr/

Repository: https://gitlab.inria.fr/coquelicot/coquelicot

Bug tracker: https://gitlab.inria.fr/coquelicot/coquelicot/issues

COPYRIGHT

This package is free software; you can redistribute it and/or modify it under the terms of GNU Lesser General Public License (see the COPYING file). Authors are Sylvie Boldo sylvie.boldo@inria.fr, Catherine Lelay catherine.lelay@inria.fr, and Guillaume Melquiond guillaume.melquiond@inria.fr.