From f0c8ead295d04d2a641be82df290643ed1fe8706 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Mon, 13 Jan 2020 14:53:59 -0500
Subject: [PATCH] fix Stlc

---
 .circleci/config.yml | 6 +++---
 .gitignore           | 1 +
 Stlc/Connect.v       | 3 +--
 Stlc/Makefile        | 4 ++--
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index c94451f..d3363bc 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -16,13 +16,13 @@ defaults: &defaults
       command: opam install .
   - run:
       name: Fsub
-      command: make -C Fsub
+      command: make -k -C Fsub
   - run:
       name: Tutorial
-      command: make -C Tutorial
+      command: make -k -C Tutorial
   - run:
       name: Stlc
-      command: make -C Stlc
+      command: make -k -C Stlc -B
 
 jobs:
   coq.8.10:
diff --git a/.gitignore b/.gitignore
index d979972..29baa5a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,7 @@
 *.v.d
 .coqdeps.d
 *.vo*
+*.v-e
 *.glob
 .*.aux
 *.v.d
diff --git a/Stlc/Connect.v b/Stlc/Connect.v
index ef1cf8b..8bcee53 100644
--- a/Stlc/Connect.v
+++ b/Stlc/Connect.v
@@ -28,10 +28,9 @@
 
 Require Import String.
 Require Import Metalib.Metatheory.
-Require Import Stlc.Definitions.
-Require Import Stlc.Lemmas.
 
 Require Import Stlc.Nominal.
+Require Import Stlc.Lemmas.
 
 Import StlcNotations.
 
diff --git a/Stlc/Makefile b/Stlc/Makefile
index b85def5..fe93098 100644
--- a/Stlc/Makefile
+++ b/Stlc/Makefile
@@ -34,8 +34,8 @@ zipclean:
 
 clean: Stlc.mk paperclean zipclean
 	make -f Stlc.mk clean
-	rm -f Stlc.mk
-	rm -f *.cmi *.cmo coqsplit
+	rm -f Stlc.mk*
+	rm -f *.cmi *.cmo coqsplit *_full* *_sol* *.v-e
 
 
 coq: $(GENCOQ) Stlc.mk