aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure
ModeNameSize
-rw-r--r--Case1.v61logplain
-rw-r--r--Case10.v116logplain
-rw-r--r--Case11.v118logplain
-rw-r--r--Case12.v142logplain
-rw-r--r--Case13.v145logplain
-rw-r--r--Case14.v204logplain
-rw-r--r--Case15.v155logplain
-rw-r--r--Case16.v199logplain
-rw-r--r--Case2.v267logplain
-rw-r--r--Case3.v194logplain
-rw-r--r--Case4.v141logplain
-rw-r--r--Case5.v164logplain
-rw-r--r--Case6.v192logplain
-rw-r--r--Case7.v456logplain
-rw-r--r--Case8.v178logplain
-rw-r--r--Case9.v221logplain
-rw-r--r--ClearBody.v239logplain
-rw-r--r--ImportedCoercion.v126logplain
-rw-r--r--Notations.v148logplain
-rw-r--r--Reordering.v182logplain
-rw-r--r--Sections.v44logplain
-rw-r--r--Tauto.v923logplain
-rw-r--r--Uminus.v530logplain
-rw-r--r--autorewritein.v393logplain
-rw-r--r--cases.v155logplain
-rw-r--r--check.v54logplain
-rw-r--r--circular_subtyping.v298logplain
-rw-r--r--clash_cons.v660logplain
-rw-r--r--clashes.v203logplain
-rw-r--r--cofixpoint.v392logplain
-rw-r--r--coqbugs0266.v164logplain
-rw-r--r--evar1.v129logplain
-rw-r--r--evarclear1.v244logplain
-rw-r--r--evarclear2.v210logplain
-rw-r--r--evarlemma.v93logplain
-rw-r--r--fixpoint1.v628logplain
-rw-r--r--fixpoint2.v97logplain
-rw-r--r--fixpoint3.v335logplain
-rw-r--r--fixpoint4.v557logplain
-rw-r--r--guard-cofix.v1157logplain
-rw-r--r--guard.v865logplain
-rw-r--r--illtype1.v543logplain
-rw-r--r--inductive.v1037logplain
-rw-r--r--ltac1.v173logplain
-rw-r--r--ltac2.v157logplain
-rw-r--r--ltac4.v152logplain
-rw-r--r--pattern.v200logplain
-rw-r--r--positivity.v576logplain
-rw-r--r--proofirrelevance.v427logplain
-rw-r--r--prop-set-proof-irrelevance.v320logplain
-rw-r--r--redef.v578logplain
-rw-r--r--rewrite_in_goal.v104logplain
-rw-r--r--rewrite_in_hyp.v120logplain
-rw-r--r--rewrite_in_hyp2.v326logplain
-rw-r--r--search.v575logplain
-rw-r--r--sortelim.v4161logplain
-rw-r--r--subterm.v1050logplain
-rw-r--r--subterm2.v1249logplain
-rw-r--r--subterm3.v824logplain
-rw-r--r--subtyping.v256logplain
-rw-r--r--subtyping2.v6430logplain
-rw-r--r--univ_include.v534logplain
-rw-r--r--universes-buraliforti-redef.v6844logplain
-rw-r--r--universes-buraliforti.v6296logplain
-rw-r--r--universes-sections1.v205logplain
-rw-r--r--universes-sections2.v223logplain
-rw-r--r--universes.v108logplain
-rw-r--r--universes3.v1188logplain