Merge pull request #904 from JasonGross/quotation+fix-descr-deps

Update descriptions and dependencies of the quotation module

Author: tabareau

Makefile

@@ -12,7 +12,7 @@ ifeq '$(METACOQ_CONFIG)' 'local'
   export OCAMLPATH
 endif
 
-.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations
+.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations quotation
 
 printconf:
 ifeq '$(METACOQ_CONFIG)' 'local'
@@ -147,7 +147,7 @@ safechecker: pcuic
 template-pcuic: template-coq pcuic
 	$(MAKE) -C template-pcuic
 
-quotation: template-coq pcuic template-pcuic
+quotation: template-coq # pcuic template-pcuic
 	$(MAKE) -C quotation
 
 safechecker-plugin: safechecker template-pcuic

coq-metacoq-quotation.opam

@@ -29,9 +29,20 @@ install: [
 ]
 depends: [
   "coq-metacoq-template" {= version}
-  "coq-metacoq-pcuic" {= version}
-  "coq-metacoq-template-pcuic" {= version}
+#  "coq-metacoq-pcuic" {= version}
+#  "coq-metacoq-template-pcuic" {= version}
 ]
-synopsis: "Gallina quotation functions for Template Coq and PCUIC."
+synopsis: "Gallina quotation functions for Template Coq (PCUIC support in the works)."
 description: """
+MetaCoq is a meta-programming framework for Coq.
+
+The Quotation module is geared at providing functions `□T → □□T` for `□T :=
+Ast.term` (currently implemented) and for `□T := { t : Ast.term & Σ ;;; [] |- t
+: T }` (still in the works).  Currently `Ast.term → Ast.term` and `(Σ ;;; [] |-
+t : T) → Ast.term` functions are provided for Template terms.  Proving
+well-typedness and adding support for PCUIC are still works in progress.
+
+Ultimately the goal of this development is to prove that `□` is a lax monoidal
+semicomonad (a functor with `cojoin : □T → □□T` that codistributes over `unit`
+and `×`), which is sufficient for proving Löb's theorem.
 """