dune-project: add maintenance_intent (#193)

Author: fblanqui

dune-project

@@ -1,4 +1,4 @@
-(lang dune 3.7)
+(lang dune 3.18)
 
 (name hol2dk)
 
@@ -18,10 +18,10 @@
  (name hol2dk)
  (synopsis "HOL-Light to Dedukti/Lambdapi and Rocq translator")
  (description "HOL-Light to Dedukti/Lambdapi and Rocq translator")
+ (maintenance_intent "(latest)")
  (depends
   dune
   (ocaml (>= 4.13))
-  (hol_light (= 3.0.0))
  )
 )
 

hol2dk.opam

@@ -2,17 +2,15 @@
 opam-version: "2.0"
 synopsis: "HOL-Light to Dedukti/Lambdapi and Rocq translator"
 description: "HOL-Light to Dedukti/Lambdapi and Rocq translator"
-x-maintenance-intent: ["(latest)"]
 maintainer: ["Frédéric Blanqui"]
 authors: ["Frédéric Blanqui"]
 license: "CeCILL-2.1"
 homepage: "https://github.com/Deducteam/hol2dk"
 doc: "https://github.com/Deducteam/hol2dk/blob/master/README.md"
 bug-reports: "https://github.com/Deducteam/hol2dk/issues"
 depends: [
-  "dune" {>= "3.7"}
+  "dune" {>= "3.18"}
   "ocaml" {>= "4.13"}
-  #"hol_light" {= "3.1.0"}
   "odoc" {with-doc}
 ]
 build: [
@@ -30,3 +28,4 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/Deducteam/hol2dk.git"
+x-maintenance-intent: ["(latest)"]

main.ml

@@ -20,13 +20,13 @@ hol2dk options command arguments
 Options
 -------
 
---root-path MODNAME: set lambdapi and coq's root_path (default is HOLLight)
+--root-path MODNAME: set lambdapi and coq's root_path (default to HOLLight)
 
 --max-dup INT: maximum number of theorem duplications
 
---max-proof-size INT: maximum size of proof files (default is 500_000)
+--max-proof-size INT: maximum size of proof files (default to 500_000)
 
---max-abbrev-size INT: maximum size of term abbreviation files (default is 2_000_000)
+--max-abbrev-size INT: maximum size of term abbreviation files (default to 2_000_000)
 
 --use-sharing: define term abbreviations using let's
 
@@ -95,9 +95,9 @@ hol2dk split $base
 
 hol2dk unsplit $base $module ...
   for each file $module, generate the files $module.sti, $module.pos,
-  $module.use and $module.nbp for all the theorems $thm proved in
-  $HOLLIGHT_DIR/$module.ml, remove all the files $thm.sti,
-  $thm.pos, $thm.use and $thm.nbp, and update $base.thm
+  $module.use, $module.nbp and, for each theorem $thm proved in
+  $HOLLIGHT_DIR/$module.ml, remove the files $thm.sti, $thm.pos, $thm.use and
+  $thm.nbp, and update $base.thp
 
 hol2dk theorem $base $thm.lp
   generate the lp proof of the theorem $thm