Pin camlp5 version of make switch to 8.02.01, fix typos in `NAME_AS…

…SUMS_TAC` help

To fix the failure mentioned in #98 ,
This updates `make switch` to pin the camlp5 version to 8.02.01.
I previously mentioned that this version was not available on some machine in the thread,
but it seems it was available unless the opam version itself was problematic.

Furthermore, to check that `make switch` is working okay, the CI check of HOL Light is
updated to use `make switch` to set up the environment.

Another small orthogonal update is fixing typos in the help doc of `NAME_ASSUMS_TAC`.

.github/workflows/main.yml

@@ -42,15 +42,13 @@ jobs:
 
   test2:
     runs-on: ubuntu-22.04
-    name: OCaml 4.14, Camlp5 8.02
+    name: OCaml 4.14, Camlp5 8.02 (make switch)
 
     steps:
       - name: Install dependency
         run: |
           sudo apt update && sudo apt install -y opam xdot
-          opam init --disable-sandboxing --compiler=4.14.0
-          opam pin -y add camlp5 8.02.01
-          opam install -y zarith
+          opam init --disable-sandboxing
 
       - name: Checkout this repo
         uses: actions/checkout@v2
@@ -60,6 +58,7 @@ jobs:
       - name: Run
         run: |
           cd hol-light
+          make switch
           eval $(opam env)
           make
           ./hol.sh | tee log.txt

Help/NAME_ASSUMS_TAC.hlp

@@ -1,6 +1,6 @@
-\DOC NAME_ASSUMS_LIST
+\DOC NAME_ASSUMS_TAC
 
-\TYPE {NAME_ASSUMS_LIST : tactic}
+\TYPE {NAME_ASSUMS_TAC : tactic}
 
 \SYNOPSIS
 Label unnamed assumptions.
@@ -9,7 +9,7 @@ Label unnamed assumptions.
 assumption.
 
 \DESCRIBE
-{NAME_ASSUMS_LIST} labels unnamed assumptions with "H0", "H1", ....
+{NAME_ASSUMS_TAC} labels unnamed assumptions with "H0", "H1", ....
 It skips named assumptions.
 
 \FAILURE

Makefile

@@ -44,7 +44,8 @@ default: update_database.ml pa_j.cmo hol.sh;
 switch:; \
   opam switch create . ocaml-base-compiler.4.14.0 ; \
   eval $(opam env) ; \
-  opam install -y zarith camlp5 ledit
+  opam install -y zarith ledit ; \
+  opam pin -y add camlp5 8.02.01
 
 # Choose an appropriate "update_database.ml" file