From 6d85df3fbc7ac2bbc9862178b3bf120e0aba8325 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 11 Jan 2023 16:55:50 +0100 Subject: [PATCH] Update --- Makefile | 2 +- src/thue_morse2.v | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 704d448..52ca050 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,7 @@ all: $(objects) # Recipe for converting a Coq file into HTML using coqdoc $(output)/%.html: $(source)/%.v - coqc $< + cd $(source); coqc `basename $<` coqdoc --html --no-index -d ./html/ $< scp $@ baruchel@sdf.org:public_html/coqbooks/ diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 1c81399..80db27a 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -604,3 +604,7 @@ Proof. rewrite <- app_assoc. reflexivity. generalize H2. apply IHj. easy. Qed. + + + +