diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 15 |
1 files changed, 9 insertions, 6 deletions
@@ -243,13 +243,16 @@ distclean: check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." -# Problems with coqchk (coq 8.3pl3): -# Integers.one_bits_range takes forever to check -# Mach#<>#instruction causes a failure -# Asm#<>#instruction causes a failure -# UnionFind.UF.elt causes an Anomaly (!) +# Problems with coqchk (coq 8.4.pl2): +# Integers.Int.Z_mod_modulus_range takes forever to check +# Floats.Float.double_of_bits_of_double takes forever to check +# AST.external_function gives "Failure: impredicative Type inductive type" +# Asm.instruction gives "Failure: impredicative Type inductive type" +# Mach.instruction gives "Failure: impredicative Type inductive type" +# UnionFind.UF.elt gives "Anomaly: Uncaught exception Reduction.NotConvertible" + check-proof: $(FILES) - $(COQCHK) -admit Integers -admit Mach -admit Asm -admit UnionFind Complements + $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements include .depend |