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.v159logplain
-rw-r--r--Case6.v187logplain
-rw-r--r--Case7.v451logplain
-rw-r--r--Case8.v173logplain
-rw-r--r--Case9.v224logplain
-rw-r--r--ClearBody.v234logplain
-rw-r--r--ImportedCoercion.v121logplain
-rw-r--r--Notations.v143logplain
-rw-r--r--Reordering.v177logplain
-rw-r--r--Sections.v35logplain
-rw-r--r--Tauto.v918logplain
-rw-r--r--Uminus.v1422logplain
-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--evar1.v124logplain
-rw-r--r--evarclear1.v239logplain
-rw-r--r--evarclear2.v205logplain
-rw-r--r--evarlemma.v88logplain
-rw-r--r--fixpoint1.v619logplain
-rw-r--r--fixpoint2.v92logplain
-rw-r--r--fixpoint3.v330logplain
-rw-r--r--fixpoint4.v552logplain
-rw-r--r--guard.v856logplain
-rw-r--r--illtype1.v538logplain
-rw-r--r--inductive1.v179logplain
-rw-r--r--inductive2.v179logplain
-rw-r--r--inductive3.v253logplain
-rw-r--r--inductive4.v521logplain
-rw-r--r--ltac1.v168logplain
-rw-r--r--ltac2.v152logplain
-rw-r--r--ltac4.v147logplain
-rw-r--r--pattern.v195logplain
-rw-r--r--positivity.v571logplain
-rw-r--r--proofirrelevance.v411logplain
-rw-r--r--prop-set-proof-irrelevance.v311logplain
-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.v321logplain
-rw-r--r--search.v570logplain
-rw-r--r--subtyping.v251logplain
-rw-r--r--subtyping2.v6425logplain
-rw-r--r--univ_include.v523logplain
-rw-r--r--universes-buraliforti-redef.v6825logplain
-rw-r--r--universes-buraliforti.v6291logplain
-rw-r--r--universes-sections1.v200logplain
-rw-r--r--universes-sections2.v218logplain
-rw-r--r--universes.v103logplain
-rw-r--r--universes3.v1183logplain