Custom coq beautifier

mk12 · Dec 25, 2018 · 2b66fb0 · 2b66fb0
1 parent 814aa15
commit 2b66fb0
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/.gitignore b/.gitignore
@@ -11,3 +11,5 @@ build.ninja
 *.vo
 *.aux
 coq/html
+coq/Makefile.local
+coq/*.old
diff --git a/coq/Chapter2.v b/coq/Chapter2.v
@@ -155,5 +155,5 @@ Qed.
 Theorem pos_pred {a : N} (H : pos a): ∃ b : N, S b = a.
 Proof.
   induction a as [|a Ha].
-  - show (exists b : N, S b = 0).
+  - show (∃ b : N, S b = 0).
 
diff --git a/coq/Makefile b/coq/Makefile
@@ -90,6 +90,9 @@ GALLINA  ?= "$(COQBIN)gallina"
 COQDOC   ?= "$(COQBIN)coqdoc"
 COQMKFILE ?= "$(COQBIN)coq_makefile"
 
+# Beatifier program
+BEAUTIFIER ?= $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify
+
 # Timing scripts
 COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
 COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
@@ -670,7 +673,7 @@ $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-tim
 
 $(BEAUTYFILES): %.v.beautified: %.v
 	$(SHOW)'BEAUTIFY $<'
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
+	$(HIDE)$(TIMER) $(BEAUTIFIER) $<
 
 $(GFILES): %.g: %.v
 	$(SHOW)'GALLINA $<'