use the short facility of HB

- remove type-in-type versions of lifting files
affeldt-aist · Apr 21, 2022 · d5f3a65 · d5f3a65
1 parent 84d1205
commit d5f3a65
Show file tree

Hide file tree

Showing 9 changed files with 372 additions and 1,362 deletions.
diff --git a/Makefile b/Makefile
@@ -21,14 +21,3 @@ _CoqProject Makefile: ;
 install_full: all
 	$(MAKE) install
 	$(MAKE) -C impredicative_set install
-
-# This last entry is only to support work-in-progress.
-
-COQ5 = coqc -w -notation-overridden -R . monae
-
-sect5: all
-	$(COQ5) fmt_lifting.v
-	$(COQ5) parametricity_codensity.v
-
-clean5:
-	rm -f *.vo *.glob *.vok *.vos
diff --git a/category.v b/category.v
@@ -1124,7 +1124,7 @@ Require Import hierarchy.
 
 Module Monad_of_category_monad.
 Section monad_of_category_monad.
-Variable M : Monad.Exports.monad CT.
+Variable M : category.Monad.Exports.monad CT.
 
 Definition acto : Type -> Type := M.
 

diff --git a/coq-monae.opam b/coq-monae.opam
@@ -25,9 +25,9 @@ depends: [
   "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
   "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
   "coq-mathcomp-analysis" { (>= "0.3.11" & < "0.4~") }
-  "coq-infotheo" { >= "0.3.5" & < "0.4~"}
+  "coq-infotheo" { >= "0.3.7" & < "0.4~"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
-  "coq-hierarchy-builder" { >= "1.1.0" }
+  "coq-hierarchy-builder" { >= "1.2.0" }
   "coq-equations" { >= "1.3" & < "1.4~" }
 ]