# basics Makefile

CONTEXT = fpu
FILES = add_correct.pvs add_ctl.pvs add_def.pvs add_synth.pvs add_tomcirc.pvs fpm_correct.pvs fpm_ctl.pvs fpm_def.pvs fpm_syth.pvs fpm_tomcirc.pvs fpu_import_add.pvs fpu_import_md.pvs md_correct.pvs md_ctl.pvs md_def.pvs md_synth.pvs md_tomcirc.pvs signals.pvs tag.pvs tom_ciruit.pvs unchanged.pvs fpu_import_misc.pvs


all: $(CONTEXT).pvs prove.el

$(CONTEXT).pvs: $(FILES)
	../theories.pl $(CONTEXT) $(FILES) > $@

prove.el: $(FILES)
	../prove.pl $(FILES) > $@