adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: Add a warning to crunch if it does not do anything

This commit is contained in:
Corey Lewis 2018-06-05 16:35:32 +10:00
parent 3ae4d6577d
commit dceb2692e2
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
lib/crunch-cmd.ML
View File

@ -764,6 +764,7 @@ fun crunch_x atts extra prp_name wpigs consts ctxt =
val (_, thms) = funkyfold (crunch {ctxt = ctxt'', prp_name = prp_name, nmspce = nmspce,
wps = wps, igs = igs, simps = simps, ig_dels = ig_dels, rules = rules} pre' extra' [])
full_const_names [];
val _ = if null thms then warning "crunch: no theorems proven" else ();
val atts' = map (Attrib.check_src ctxt) atts;