Merge pull request #6 from coq-community/compat-boilerplate

Compatibility with 8.18 and beyond

Author: palmskog

.github/workflows/docker-action.yml

@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'

README.md

@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[docker-action-shield]: https://github.com/coq-community/coqtail-math/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/coqtail-math/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/coqtail-math/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/coqtail-math/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md

Reals/Hopital.v

@@ -2785,10 +2785,12 @@ apply limit_div_pos_inv.
 apply limit_div_neg_ext with (fun x => (f x) / (- g x)).
 intros. field. apply g_not_0. apply H.
 assert (Dg' : forall x, open_interval a b x -> derivable_pt (- g) x). intros. reg. apply Dg; intuition.
-apply Hopital_gpinf_Lninf_right with Df Dg'; try assumption; try reg; try (now intuition). apply limit_div_pos_inv. 
+apply Hopital_gpinf_Lninf_right with Df Dg'; try assumption; try reg.
+intros; apply continuity_pt_opp; apply Cg; assumption.
+apply limit_div_pos_inv.
 apply limit_div_neg_ext with g. intros. unfold opp_fct. ring. apply Zg.
 intros. intro. apply g'_not_0 with x Hopen. rewrite (pr_nu _ _ _ (derivable_pt_opp g x (Dg x Hopen))) in H.
-rewrite  derive_pt_opp in H. apply Ropp_eq_0_compat in H. rewrite <- H. ring.
+rewrite derive_pt_opp in H. apply Ropp_eq_0_compat in H. rewrite <- H. ring.
 intros m Hm. destruct (Hlimder m Hm) as [alp [Halp Hsolve]]. 
 exists alp. split. assumption.
 intros. specialize (Hsolve x Hopen H).

coq-coqtail.opam

@@ -19,7 +19,7 @@ and complex analysis."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.11" & < "8.18~") | (= "dev")}
+  "coq" {>= "8.11"}
 ]
 
 tags: [

meta.yml

@@ -35,13 +35,14 @@ license:
 
 supported_coq_versions:
   text: 8.11 or later
-  opam: '{(>= "8.11" & < "8.18~") | (= "dev")}'
+  opam: '{>= "8.11"}'
 
 tested_coq_nix_versions:
 - coq_version: 'master'
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.18'
 - version: '8.17'
 - version: '8.16'
 - version: '8.15'