From 187d18d1fc0947954f1a5d6e8929f33dbe6f3e2f Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Fri, 13 Sep 2024 01:11:23 -0400
Subject: [PATCH] Update opam informations (#197)

---
 dune-project        | 16 ++++++++++------
 mcltt.opam.template |  5 +++++
 2 files changed, 15 insertions(+), 6 deletions(-)
 create mode 100644 mcltt.opam.template

diff --git a/dune-project b/dune-project
index 22f8e4e7..2f21da40 100644
--- a/dune-project
+++ b/dune-project
@@ -4,13 +4,17 @@
 
 (generate_opam_files)
 
+(license MIT)
+(authors "Antoine Gaulin"
+         "Jason Hu"
+         "Junyoung Jang")
+(maintainers "the CompLogic group, McGill University")
+(homepage "https://beluga-lang.github.io/McLTT/")
+(documentation "https://beluga-lang.github.io/McLTT/")
+(source (github Beluga-lang/McLTT))
+
 (package
  (name mcltt)
- (license MIT)
- (authors "the CompLogic group, McGill University")
- (maintainers "the CompLogic group, McGill University")
- (homepage "https://beluga-lang.github.io/McLTT/")
- (bug_reports "https://github.com/Beluga-lang/McLTT/issues")
  (synopsis "A Bottom-up Approach to Implementing A Proof Assistant")
  (description "In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After
 the accomplishment of this project, we will obtain an executable, to which we can feed
@@ -26,4 +30,4 @@ elementary) and serves as a basis for future extensions.")
   (menhir (= "20240715"))
   (coq-menhirlib (= "20240715"))
   (coq-equations (= "1.3"))
-  (sherlodoc :coqdoc)))
+  (sherlodoc :with-doc)))
diff --git a/mcltt.opam.template b/mcltt.opam.template
new file mode 100644
index 00000000..3d7af790
--- /dev/null
+++ b/mcltt.opam.template
@@ -0,0 +1,5 @@
+build: [
+  [make]
+  [make coqdoc] {with-doc}
+]
+