Merge pull request #28 from coq-community/v8.11+master-fixes

improvements from master branch for 8.11

Makefile

@@ -1,16 +1,16 @@
 all: Makefile.coq
-	+$(MAKE) -f Makefile.coq all
+	@+$(MAKE) -f Makefile.coq all
 
 clean: Makefile.coq
-	+$(MAKE) -f Makefile.coq cleanall
-	rm -f Makefile.coq Makefile.coq.conf
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
 	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-_CoqProject Makefile: ;
+force _CoqProject Makefile: ;
 
-%: Makefile.coq
-	+$(MAKE) -f Makefile.coq $@
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: all clean
+.PHONY: all clean force

README.md

@@ -4,6 +4,7 @@
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Gitter][gitter-shield]][gitter-link]
+[![coqdoc][coqdoc-shield]][coqdoc-link]
 [![DOI][doi-shield]][doi-link]
 
 [travis-shield]: https://travis-ci.com/coq-community/atbr.svg?branch=master
@@ -18,6 +19,9 @@
 [gitter-shield]: https://img.shields.io/badge/chat-on%20gitter-%23c1272d.svg
 [gitter-link]: https://gitter.im/coq-community/Lobby
 
+[coqdoc-shield]: https://img.shields.io/badge/docs-coqdoc-blue.svg
+[coqdoc-link]: https://coq-community.github.io/atbr/docs/latest/coqdoc/toc.html
+
 [doi-shield]: https://zenodo.org/badge/DOI/10.2168/LMCS-8(1:16)2012.svg
 [doi-link]: https://doi.org/10.2168/LMCS-8(1:16)2012
 
@@ -37,11 +41,10 @@ rather than automata: https://github.com/damien-pous/relation-algebra
   - Damien Pous (initial)
 - Coq-community maintainer(s):
   - Tej Chajed ([**@tchajed**](https://github.com/tchajed))
-  - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU Lesser General Public License v3.0 or later](LICENSE)
 - Compatible Coq versions: 8.11 (use the corresponding branch or release for other Coq versions)
-- Compatible OCaml versions: all versions supported by Coq
-- Additional Coq dependencies: none
+- Compatible OCaml versions: 4.05.0 or later
+- Additional dependencies: none
 - Coq namespace: `ATBR`
 - Related publication(s):
   - [Deciding Kleene Algebras in Coq](https://arxiv.org/abs/1105.4537) doi:[10.2168/LMCS-8(1:16)2012](https://doi.org/10.2168/LMCS-8(1:16)2012)
@@ -68,8 +71,12 @@ make install
 
 ## Documentation
 
-Here is a succinct description of each file.
-The user can also refer to files `Examples.v` and `ChurchRosser.v`.
+The development and underlying theory of the library is described in the paper
+[Deciding Kleene Algebras in Coq][paper], Logical Methods in Computer Science,
+Volume 8, Issue 1, 2012.
+
+Below are succinct descriptions of each file and tactic. See also the
+[coqdoc presentation][coqdoc] of the Coq source files from the latest release.
 
 ### Library files
 
@@ -207,3 +214,6 @@ who participated to a preliminary version of this project. They are also gratefu
 to Assia Mahboubi, Matthieu Sozeau, Bruno Barras, and Hugo Herbelin for highly
 stimulating discussions, as well as numerous hints for solving various problems.
 
+[paper]: https://arxiv.org/abs/1105.4537
+[coqdoc]: https://coq-community.github.io/atbr/docs/latest/coqdoc/toc.html
+

coq-atbr.opam

@@ -5,9 +5,10 @@ version: "8.11.dev"
 homepage: "https://github.com/coq-community/atbr"
 dev-repo: "git+https://github.com/coq-community/atbr.git"
 bug-reports: "https://github.com/coq-community/atbr/issues"
+doc: "https://coq-community.github.io/atbr/"
 license: "LGPL-3.0-or-later"
 
-synopsis: "A Coq tactic for deciding Kleene algebras"
+synopsis: "Coq library and tactic for deciding Kleene algebras"
 description: """
 This library provides algebraic tools for working with binary relations.
 The main tactic provided is a reflexive tactic for solving (in)equations
@@ -21,7 +22,7 @@ rather than automata: https://github.com/damien-pous/relation-algebra"""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "ocaml"
+  "ocaml" {>= "4.05.0"}
   "coq" {>= "8.11" & < "8.12~"}
 ]
 

meta.yml

@@ -4,9 +4,10 @@ shortname: atbr
 organization: coq-community
 community: true
 travis: true
+coqdoc: true
 doi: 10.2168/LMCS-8(1:16)2012
 
-synopsis: A Coq tactic for deciding Kleene algebras
+synopsis: Coq library and tactic for deciding Kleene algebras
 
 description: |-
   This library provides algebraic tools for working with binary relations.
@@ -32,8 +33,6 @@ authors:
 maintainers:
 - name: Tej Chajed
   nickname: tchajed
-- name: Karl Palmskog
-  nickname: palmskog
 
 opam-file-maintainer: [email protected]
 
@@ -43,12 +42,14 @@ license:
   fullname: GNU Lesser General Public License v3.0 or later
   identifier: LGPL-3.0-or-later
 
-plugin: true
-
 supported_coq_versions:
   text: 8.11 (use the corresponding branch or release for other Coq versions)
   opam: '{>= "8.11" & < "8.12~"}'
 
+supported_ocaml_versions:
+    text: 4.05.0 or later
+    opam: '{>= "4.05.0"}'
+
 tested_coq_nix_versions:
 - version_or_url: '8.11'
 
@@ -72,8 +73,12 @@ categories:
 documentation: |
   ## Documentation
 
-  Here is a succinct description of each file.
-  The user can also refer to files `Examples.v` and `ChurchRosser.v`.
+  The development and underlying theory of the library is described in the paper
+  [Deciding Kleene Algebras in Coq][paper], Logical Methods in Computer Science,
+  Volume 8, Issue 1, 2012.
+
+  Below are succinct descriptions of each file and tactic. See also the
+  [coqdoc presentation][coqdoc] of the Coq source files from the latest release.
 
   ### Library files
 
@@ -210,4 +215,7 @@ documentation: |
   who participated to a preliminary version of this project. They are also grateful
   to Assia Mahboubi, Matthieu Sozeau, Bruno Barras, and Hugo Herbelin for highly
   stimulating discussions, as well as numerous hints for solving various problems.
+
+  [paper]: https://arxiv.org/abs/1105.4537
+  [coqdoc]: https://coq-community.github.io/atbr/docs/latest/coqdoc/toc.html
 ---

theories/KleeneAlgebra.v

@@ -197,7 +197,9 @@ Section Props2.
   Qed.
 
   Lemma a_star_a_leq_star_a: forall (a: X A A), a*a# <== a#.
-  Proof star_a_a_leq_star_a (KA:=Dual.KleeneAlgebra) (A:=A).
+  Proof.
+    exact (star_a_a_leq_star_a (KA:=Dual.KleeneAlgebra) (A:=A)).
+  Qed.
 
   Lemma star_distr (a b: X A A): (a + b)# == a# * (b*a#)#.
   Proof.
@@ -247,10 +249,14 @@ Section Props3.
   Context `{KA: KleeneAlgebra}.
 
   Lemma semicomm_iter_left: forall A B (a: X A A) (b: X B B) (c: X A B), a*c <== c*b -> a#*c <== c*b#.
-  Proof semicomm_iter_right (KA:=Dual.KleeneAlgebra).
+  Proof.
+    exact (semicomm_iter_right (KA:=Dual.KleeneAlgebra)).
+  Qed.
 
   Lemma wsemicomm_iter_left: forall A (b a : X A A), a*b <== b*a#  ->  a#*b <== b*a#.
-  Proof wsemicomm_iter_right (KA:=Dual.KleeneAlgebra).
+  Proof.
+    exact (wsemicomm_iter_right (KA:=Dual.KleeneAlgebra)).
+  Qed.
 
   Lemma comm_iter_left A B (x : X A B) a b:  a * x == x * b -> a# * x == x * b# .
   Proof.
@@ -272,6 +278,8 @@ Section Props4.
   Context `{KA: KleeneAlgebra}.
 
   Lemma comm_iter_right: forall B A (x : X A B) a b,  x * a == b * x -> x * a# == b# * x .
-  Proof comm_iter_left (KA:=Dual.KleeneAlgebra).
+  Proof.
+    exact (comm_iter_left (KA:=Dual.KleeneAlgebra)).
+  Qed.
 
 End Props4.

theories/MxGraph.v

@@ -49,7 +49,9 @@ Section Defs.
 
   Lemma mx_equal': forall n m (M N: @Classes.X mx_Graph n m) 
     (H: forall i j, i<n -> j<m -> get M i j == get N i j), M == N.
-  Proof (fun _ _ _ _ H => H).
+  Proof.
+    exact (fun _ _ _ _ H => H).
+  Qed.
 
   Definition mx_equal_at p q n m n' m' (M : MX n m) (N : MX n' m') := 
     forall i j, i < p -> j < q -> get M i j == get N i j.

theories/SemiLattice.v

@@ -202,7 +202,9 @@ Section Props1.
   Variables A B: T.
 
   Lemma zero_inf: forall (x: X A B), 0 <== x.
-  Proof (@plus_neutral_left _ _ _ A B).  
+  Proof.
+    exact (@plus_neutral_left _ _ _ A B).
+  Qed.
 
   Lemma plus_make_left: forall (x y: X A B), x <== x+y.
   Proof. intros; unfold leq. rewrite plus_assoc, plus_idem. reflexivity. Qed.

theories/Utils_WF.v

@@ -80,6 +80,7 @@ Section wf_to.
     rel_to_intro: forall a' a, R a' a -> rel_to (f a') (f a).
   Hypothesis HR: well_founded rel_to.
   Theorem rel_to_wf: well_founded R.
+  Proof.
     intro a. remember (f a) as fa. revert a Heqfa.
     induction fa as [fa IHa] using (well_founded_induction HR).
     constructor. intros a' H. subst. eapply IHa; trivial. constructor. trivial.
@@ -102,7 +103,7 @@ Section wf_lexico_incl.
     intros [a' b'] [a b] [u' u Hab]. auto. 
   Qed.
 End wf_lexico_incl.
-   
+
 
 (** Lazy partial fixpoint operators (lazy iterator):
     we use these functions to avoid the computation of a (2^n) worst-case