Merge pull request #5 from proux01/instantiate-value

Remove old capitalized syntax for instantiate

.github/workflows/docker-action.yml

@@ -0,0 +1,38 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:8.8'
+          - 'coqorg/coq:8.9'
+          - 'coqorg/coq:8.10'
+          - 'coqorg/coq:8.11'
+          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.13'
+          - 'coqorg/coq:8.14'
+          - 'coqorg/coq:dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-mathcomp-bigenough.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -1,18 +1,58 @@
-[![Build Status](https://travis-ci.org/math-comp/bigenough.svg?branch=master)](https://travis-ci.org/math-comp/bigenough)
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
+# bigenough
 
-# A small library to do epsilon - N reasoning.
+[![Docker CI][docker-action-shield]][docker-action-link]
 
-The repository contains a package to reasoning with big enough objects (mostly natural numbers).
+[docker-action-shield]: https://github.com/math-comp/bigenough/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/bigenough/actions?query=workflow:"Docker%20CI"
 
-This repository is essentially for archiving purposes as `bigenough` will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93).
 
-The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant, although it requires only the ssreflect package.
 
-## Installation
 
-If you already have OPAM installed:
+The package contains a package to reasoning with big enough objects
+(mostly natural numbers). This package is essentially for backward
+compatibility purposes as `bigenough` will be subsumed by the near
+tactics. The formalization is based on the Mathematical Components
+library.
 
-```
+## Meta
+
+- Author(s):
+  - Cyril Cohen
+- License: [CeCILL-B](LICENSE)
+- Compatible Coq versions: 8.8 or later
+- Additional dependencies:
+  - [MathComp ssreflect](https://math-comp.github.io) 1.6 or later
+- Coq namespace: `mathcomp.bigenough`
+- Related publication(s): none
+
+## Building and installation instructions
+
+The easiest way to install the latest released version of bigenough
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+
+```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam install coq-mathcomp-bigenough
 ```
+
+To instead build and install manually, do:
+
+``` shell
+git clone https://github.com/math-comp/bigenough.git
+cd bigenough
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+# A small library to do epsilon - N reasoning.
+
+This repository is essentially for archiving purposes as `bigenough`
+will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93).
+
+The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant,
+although it requires only the ssreflect package.

bigenough.v

@@ -84,16 +84,16 @@ Canonical big_enough_nat := BigRelOf big_rel_leq_class.
 Definition closed T (i : T) := {j : T | j = i}.
 Ltac close :=  match goal with
                  | |- context [closed ?i] =>
-                   instantiate (1 := [::]) in (Value of i); exists i
+                   instantiate (1 := [::]) in (value of i); exists i
                end.
 
 Ltac pose_big_enough i :=
   evar (i : nat); suff : closed i; first do
-    [move=> _; instantiate (1 := bigger_than leq _) in (Value of i)].
+    [move=> _; instantiate (1 := bigger_than leq _) in (value of i)].
 
 Ltac pose_big_modulus m F :=
   evar (m : F -> nat); suff : closed m; first do
-    [move=> _; instantiate (1 := (fun e => bigger_than leq _)) in (Value of m)].
+    [move=> _; instantiate (1 := (fun e => bigger_than leq _)) in (value of m)].
 
 Ltac exists_big_modulus m F := pose_big_modulus m F; first exists m.
 

coq-mathcomp-bigenough.opam

@@ -0,0 +1,37 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Cyril Cohen <[email protected]>"
+version: "dev"
+
+homepage: "https://github.com/math-comp/bigenough"
+dev-repo: "git+https://github.com/math-comp/bigenough.git"
+bug-reports: "https://github.com/math-comp/bigenough/issues"
+license: "CeCILL-B"
+
+synopsis: "A small library to do epsilon - N reasoning"
+description: """
+The package contains a package to reasoning with big enough objects
+(mostly natural numbers). This package is essentially for backward
+compatibility purposes as `bigenough` will be subsumed by the near
+tactics. The formalization is based on the Mathematical Components
+library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {(>= "8.8" & < "8.15~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {>= "1.6"}
+]
+
+tags: [
+  "keyword:bigenough"
+  "keyword:asymptotic reasonning"
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "logpath:mathcomp.bigenough"
+]
+authors: [
+  "Cyril Cohen"
+]

meta.yml

@@ -0,0 +1,73 @@
+---
+fullname: bigenough
+shortname: bigenough
+opam_name: coq-mathcomp-bigenough
+organization: math-comp
+community: false
+action: true
+coqdoc: false
+dune: false
+
+synopsis: >-
+  A small library to do epsilon - N reasoning
+
+description: |-
+  The package contains a package to reasoning with big enough objects
+  (mostly natural numbers). This package is essentially for backward
+  compatibility purposes as `bigenough` will be subsumed by the near
+  tactics. The formalization is based on the Mathematical Components
+  library.
+
+authors:
+- name: Cyril Cohen
+
+maintainers:
+- name: Cyril Cohen
+  nickname: CohenCyril
+
+opam-file-maintainer: 'Cyril Cohen <[email protected]>'
+
+opam-file-version: 'dev'
+
+license:
+  fullname: CeCILL-B
+  identifier: CeCILL-B
+
+supported_coq_versions:
+  text: '8.8 or later'
+  opam: '{(>= "8.8" & < "8.15~") | (= "dev")}'
+
+dependencies:
+- opam:
+    name: coq-mathcomp-ssreflect
+    version: '{>= "1.6"}'
+  description: |-
+    [MathComp ssreflect](https://math-comp.github.io) 1.6 or later
+
+tested_coq_opam_versions:
+- version: '8.8'
+- version: '8.9'
+- version: '8.10'
+- version: '8.11'
+- version: '8.12'
+- version: '8.13'
+- version: '8.14'
+- version: 'dev'
+
+namespace: mathcomp.bigenough
+
+keywords:
+- name: bigenough
+- name: asymptotic reasonning
+- name: small scale reflection
+- name: mathematical components
+
+documentation: |-
+  # A small library to do epsilon - N reasoning.
+
+  This repository is essentially for archiving purposes as `bigenough`
+  will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93).
+
+  The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant,
+  although it requires only the ssreflect package.
+---