aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure
ModeNameSize
-rw-r--r--Case1.v56logplain
-rw-r--r--Case10.v111logplain
-rw-r--r--Case11.v113logplain
-rw-r--r--Case12.v137logplain
-rw-r--r--Case13.v140logplain
-rw-r--r--Case14.v199logplain
-rw-r--r--Case15.v150logplain
-rw-r--r--Case16.v194logplain
-rw-r--r--Case2.v262logplain
-rw-r--r--Case3.v189logplain
-rw-r--r--Case4.v136logplain
-rw-r--r--Case5.v160logplain
-rw-r--r--Case6.v187logplain
-rw-r--r--Case7.v451logplain
-rw-r--r--Case8.v173logplain
-rw-r--r--Case9.v226logplain
-rw-r--r--ClearBody.v234logplain
-rw-r--r--Notations.v143logplain
-rw-r--r--Tauto.v918logplain
-rw-r--r--Uminus.v1438logplain
-rw-r--r--autorewritein.v388logplain
-rw-r--r--cases.v150logplain
-rw-r--r--check.v49logplain
-rw-r--r--circular_subtyping1.v223logplain
-rw-r--r--circular_subtyping2.v235logplain
-rw-r--r--clash_cons.v655logplain
-rw-r--r--clashes.v198logplain
-rw-r--r--coqbugs0266.v159logplain
-rw-r--r--fixpoint1.v619logplain
-rw-r--r--fixpoint2.v92logplain
-rw-r--r--guard.v581logplain
-rw-r--r--illtype1.v538logplain
-rw-r--r--inductive1.v179logplain
-rw-r--r--inductive2.v179logplain
-rw-r--r--inductive3.v254logplain
-rw-r--r--ltac1.v168logplain
-rw-r--r--ltac2.v152logplain
-rw-r--r--ltac4.v147logplain
-rw-r--r--pattern.v203logplain
-rw-r--r--positivity.v571logplain
-rw-r--r--proofirrelevance.v412logplain
-rw-r--r--redef.v573logplain
-rw-r--r--rewrite_in_goal.v99logplain
-rw-r--r--rewrite_in_hyp.v115logplain
-rw-r--r--rewrite_in_hyp2.v322logplain
-rw-r--r--search.v570logplain
-rw-r--r--subtyping.v254logplain
-rw-r--r--subtyping2.v6525logplain
-rw-r--r--univ_include.v525logplain
-rw-r--r--universes-buraliforti-redef.v6925logplain
-rw-r--r--universes-buraliforti.v6391logplain
-rw-r--r--universes-sections1.v200logplain
-rw-r--r--universes-sections2.v218logplain
-rw-r--r--universes.v103logplain
-rw-r--r--universes2.v120logplain