Fixing Required LibSpecialize.

.github/workflows/ci-libhyps.yml

@@ -36,3 +36,27 @@ jobs:
           custom_image: ${{ matrix.image }}
         env:
           OPAMWITHTEST: 'true'
+
+  # This workflow contains a single job called "build"
+  test:
+    # The type of runner that the job will run on
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.18'
+          - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.16'
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+      # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
+      - uses: actions/checkout@v3
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-libhyps.opam'
+          custom_image: ${{ matrix.image }}
+      - name: test files
+        run: ./configure.sh 
+        run: make
+        run: make tests

LibHyps/LibHyps.v

@@ -4,7 +4,7 @@
 
 Require Export LibHyps.TacNewHyps.
 Require Export LibHyps.LibHypsNaming.
-Require Export LibHyps.LibSpecialize.
+(* Require Export LibHyps.LibSpecialize. *)
 Require Export LibHyps.LibHypsTactics.
 (* We export ; { } etc. ";;" also. *)
 

LibHyps/LibHypsRegression.v

@@ -2,7 +2,7 @@
   This file is part of LibHyps. It is distributed under the MIT
   "expat license". You should have recieved a LICENSE file with it. *)
 
-Require Import Arith ZArith LibHyps.LibHyps LibHyps.LibSpecialize List.
+Require Import Arith ZArith LibHyps.LibHyps (*LibHyps.LibSpecialize*) List.
 
 
 Import TacNewHyps.Notations.

LibHyps/LibHypsTactics.v

@@ -4,7 +4,7 @@
 
 Require Export LibHyps.TacNewHyps.
 Require Export LibHyps.LibHypsNaming.
-Require Export LibHyps.LibSpecialize.
+(* Require Export LibHyps.LibSpecialize. *)
 
 (* debug *)
 Ltac pr_goal :=

LibHyps/LibHypsTest.v

@@ -2,7 +2,7 @@
   This file is part of LibHyps. It is distributed under the MIT
   "expat license". You should have recieved a LICENSE file with it. *)
 
-Require Import Arith ZArith LibHyps.LibHyps LibHyps.LibSpecialize List.
+Require Import Arith ZArith LibHyps.LibHyps (*LibHyps.LibSpecialize*) List.
 
 Local Open Scope autonaming_scope.
 Import ListNotations.

Makefile.local

@@ -24,6 +24,10 @@ cleantests:
 	rm -f LibHyps/LibHypsTest.vo LibHyps/LibHypsTest.vok LibHyps/LibHypsTest.vos LibHyps/LibHypsTest.glob
 	rm -f Demo/*.vo Demo/*.vok Demo/*.vos Demo/*.glob
 
+clean::
+	rm -f LibHyps/*.vo LibHyps/*.vos LibHyps/*.vok LibHyps/*.glob LibHyps/*.aux
+	rm -f LibHyps/.*.vo LibHyps/.*.aux
+
 ### Local Variables: ***
 ### mode: makefile ***
 ### End: ***

_CoqProject

@@ -5,9 +5,3 @@ LibHyps/LibHypsTactics.v
 LibHyps/LibDecomp.v
 LibHyps/TacNewHyps.v
 LibHyps/LibHyps.v
-
-# especialize is broken in coq-8.18. This is due to a change in
-# specialize tactic that does not allow new evars remaining in its
-# subgoals. This is unfortunate and hopefully fixed in the next
-# version.
-# LibHyps/LibSpecialize.v

configure.sh

@@ -3,7 +3,7 @@
 FILES=`find . -name "*.v" -exec echo {} \;`
 echo "-R LibHyps LibHyps" > _CoqProject
 echo "" >> _CoqProject
-for i in `find LibHyps -name "*.v"| grep -v LibHypsNaming2 | grep -v LibHypsExamples | grep -v LibHypsDemo | grep -v LibHypsTest | grep -v LibHypsRegression`; do
+for i in `find LibHyps -name "*.v"| grep -v LibHypsNaming2 | grep -v LibSpecialize.v | grep -v LibHypsExamples | grep -v LibHypsDemo | grep -v LibHypsTest | grep -v LibHypsRegression`; do
   echo $i >> _CoqProject
 done
 coq_makefile -f _CoqProject -o Makefile