diff --git a/README.md b/README.md index cdcf63b..e904fda 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ [![Build Status](https://travis-ci.org/math-comp/bigenough.svg?branch=master)](https://travis-ci.org/math-comp/bigenough) -# A small library to do epsilon - N reasonning. +# A small library to do epsilon - N reasoning. The repository contains a package to reasoning with big enough objects (mostly natural numbers). diff --git a/bigenough.v b/bigenough.v index 281d6c6..dd7baec 100644 --- a/bigenough.v +++ b/bigenough.v @@ -5,7 +5,7 @@ From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. (****************************************************************************) -(* This is a small library to do epsilon - N reasonning. *) +(* This is a small library to do epsilon - N reasoning. *) (* In order to use it, one only has to know the following tactics: *) (* *) (* pose_big_enough i == pose a big enough natural number i *) diff --git a/descr b/descr index 2d6cfb5..9b8b798 100644 --- a/descr +++ b/descr @@ -1,4 +1,4 @@ -A small library to do epsilon - N reasonning. +A small library to do epsilon - N reasoning. The repository contains a package to reasoning with big enough objects (mostly natural numbers). This repository is essentially for archiving diff --git a/opam b/opam index 156effd..356722c 100644 --- a/opam +++ b/opam @@ -13,5 +13,5 @@ install: [ make "install" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/bigenough'" ] depends: [ "coq-mathcomp-ssreflect" { (>= "1.6.0" | = "dev") } ] -tags: [ "keyword:bigenough" "keyword:asymptotic reasonning" "keyword:small scale reflection" "keyword:mathematical components" ] +tags: [ "keyword:bigenough" "keyword:asymptotic reasoning" "keyword:small scale reflection" "keyword:mathematical components" ] authors: [ "Cyril Cohen " ]