Skip to content
Snippets Groups Projects
Commit ee1d6bed authored by Pierre Roux's avatar Pierre Roux
Browse files
parent d955d6af
No related branches found
No related tags found
No related merge requests found
...@@ -29,7 +29,8 @@ COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode ...@@ -29,7 +29,8 @@ COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
# These versions of Coq are known to have different output so we don't test them. # These versions of Coq are known to have different output so we don't test them.
# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later. # Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
# Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha. # Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1) #COQ_NOREF= $(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
COQ_NOREF= $(shell echo 1)
tests/.coqdeps.d: $(TESTFILES) tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES' $(SHOW)'COQDEP TESTFILES'
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
of [gFunctors]: of [gFunctors]:
See [!782](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/782) *) See [!782](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/782) *)
From Coq Require Import Logic.Eqdep. From Coq.Logic Require Import Eqdep.
(** A [sigT] that is partially applied and template-polymorphic causes universe (** A [sigT] that is partially applied and template-polymorphic causes universe
inconsistency errors, which is why [sigT] should be avoided for the definition inconsistency errors, which is why [sigT] should be avoided for the definition
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment