Fix regression machinery for Coq

slanterns · Mar 7, 2022 · 6a02125 · 6a02125
1 parent 8321af7
commit 6a02125
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/regression/Makefile b/regression/Makefile
@@ -66,6 +66,9 @@ clean:
 	rm -rf *~
 	rm -rf regression
 	rm -rf testRegr*
+	rm -rf .testRegr*
+	rm -rf ._ott_coqrc.aux
+	rm -rf _ott_coqrc.glob
 
 clean-regr:
 	rm -rf testRegr*

diff --git a/regression/_ott_coqrc.v b/regression/_ott_coqrc.v
@@ -1,6 +1,6 @@
 (*This file is used by the regression tests.*)
 (* Add LoadPath "../coq/metatheory".*)
-Add LoadPath "../coq".
+Add LoadPath "../coq" as Ott.
 (* Add LoadPath "". *)
 (* Add LoadPath "../coq/ln_sets". *)
 (* Add LoadPath "../examples/tapl". *)