From 475204b9dab4b72cc66753f504ce494fda4cc35e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 10 Jul 2026 15:51:41 +0200
Subject: [PATCH] support for -package

cf https://github.com/rocq-prover/rfcs/pull/101 / https://github.com/rocq-prover/rocq/pull/21564
---
 coq/coq-system.el | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/coq/coq-system.el b/coq/coq-system.el
index e9b3acd7f..4ba51cb1f 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -331,6 +331,10 @@ Set to t if you want this feature, but note that it is deprecated."
                (eq (car entry) 'recnoimport)
                (cl-every 'stringp (cdr entry))
                (equal (length entry) 3))
+          (and (listp entry)
+               (eq (car entry) 'package)
+               (cl-every 'stringp (cdr entry))
+               (equal (length entry) 2))
           (and (listp entry)
                (eq (car entry) 'ocamlimport)
                (cl-every 'stringp (cdr entry))
@@ -352,6 +356,8 @@ forms of include options (`-I' `-Q' and `-R').  An element can be
 
   - A list of the form `(\\='ocamlimport dir)', specifying (in 8.5) a
     directory to be added to Ocaml path (`-I').
+  - A list of the form `(\\='package name)', specifying (since 9.3) a
+    ocamlfind package with Rocq files.
   - A list of the form `(\\='rec dir path)' (where dir and path are
     strings) specifying a directory to be recursively mapped to the
     logical path `path' (`-R dir path').
@@ -385,6 +391,10 @@ not the same (-I is for Coq path)."
                                (const recnoimport)
                                (string :tag "directory")
                                (string :tag "log path"))
+                         (list :tag
+                               "ocamlfind package for Rocq"
+                               (const package)
+                               (string :tag "name"))
                          (list :tag
                                "compatibility for of -I (-I ... -as ... in coq<=8.4)"
                                (const nonrec)
@@ -435,6 +445,8 @@ request compatibility handling of flags."
        (list "-Q" (expand-file-name dir) ""))
       (`(ocamlimport ,dir)
        (list "-I" (expand-file-name dir)))
+      (`(package ,name)
+       (list "-package" name))
       (`(recnoimport ,dir ,alias)
        (list "-Q" (expand-file-name dir) alias))
       ((or `(rec ,dir ,alias) `(,dir ,alias))
@@ -659,6 +671,7 @@ ALREADYOPEN is t if buffer already existed."
   '(("-R" . 2)
     ("-Q" . 2)
     ("-I" . 1)
+    ("-package" . 1)
     ("-arg" . 1)
     ("-opt" . 0)
     ("-byte" . 0)))
@@ -711,6 +724,8 @@ coqtop.  But -arg \"\\='a b\\='\" means to pass a and b together."
   (pcase option
     (`("-I" ,path)
      (list 'ocamlimport (expand-file-name path base-directory)))
+    (`("-package" ,name)
+     (list 'package name))
     (`("-R" ,path ,alias)
      (list 'rec (expand-file-name path base-directory) alias))
     (`("-Q" ,path ,alias)