Imported Upstream version 8.0pl1upstream/8.0pl1

2 files changed, 214 insertions, 0 deletions

diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v
new file mode 100644
index 00000000..4accbf34
--- /dev/null
+++ b/test-suite/bench/lists-100.v
@@ -0,0 +1,107 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0.
+Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1.
+Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2.
+Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3.
+Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4.
+Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5.
+Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6.
+Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7.
+Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8.
+Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9.
+Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10.
+Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11.
+Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12.
+Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13.
+Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14.
+Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15.
+Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16.
+Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17.
+Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18.
+Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19.
+Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20.
+Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21.
+Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22.
+Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23.
+Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24.
+Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25.
+Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26.
+Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27.
+Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28.
+Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29.
+Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30.
+Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31.
+Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32.
+Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33.
+Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34.
+Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35.
+Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36.
+Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37.
+Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38.
+Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39.
+Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40.
+Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41.
+Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42.
+Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43.
+Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44.
+Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45.
+Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46.
+Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47.
+Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48.
+Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49.
+Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50.
+Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51.
+Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52.
+Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53.
+Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54.
+Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55.
+Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56.
+Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57.
+Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58.
+Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59.
+Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60.
+Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61.
+Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62.
+Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63.
+Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64.
+Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65.
+Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66.
+Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67.
+Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68.
+Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69.
+Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70.
+Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71.
+Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72.
+Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73.
+Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74.
+Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75.
+Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76.
+Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77.
+Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78.
+Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79.
+Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80.
+Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81.
+Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82.
+Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83.
+Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84.
+Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85.
+Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86.
+Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87.
+Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88.
+Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89.
+Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90.
+Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91.
+Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92.
+Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93.
+Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94.
+Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95.
+Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96.
+Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97.
+Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98.
+Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99.
diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v
new file mode 100644
index 00000000..4accbf34
--- /dev/null
+++ b/test-suite/bench/lists_100.v
@@ -0,0 +1,107 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0.
+Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1.
+Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2.
+Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3.
+Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4.
+Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5.
+Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6.
+Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7.
+Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8.
+Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9.
+Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10.
+Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11.
+Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12.
+Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13.
+Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14.
+Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15.
+Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16.
+Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17.
+Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18.
+Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19.
+Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20.
+Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21.
+Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22.
+Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23.
+Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24.
+Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25.
+Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26.
+Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27.
+Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28.
+Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29.
+Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30.
+Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31.
+Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32.
+Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33.
+Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34.
+Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35.
+Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36.
+Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37.
+Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38.
+Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39.
+Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40.
+Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41.
+Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42.
+Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43.
+Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44.
+Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45.
+Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46.
+Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47.
+Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48.
+Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49.
+Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50.
+Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51.
+Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52.
+Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53.
+Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54.
+Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55.
+Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56.
+Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57.
+Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58.
+Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59.
+Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60.
+Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61.
+Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62.
+Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63.
+Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64.
+Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65.
+Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66.
+Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67.
+Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68.
+Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69.
+Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70.
+Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71.
+Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72.
+Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73.
+Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74.
+Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75.
+Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76.
+Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77.
+Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78.
+Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79.
+Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80.
+Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81.
+Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82.
+Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83.
+Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84.
+Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85.
+Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86.
+Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87.
+Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88.
+Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89.
+Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90.
+Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91.
+Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92.
+Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93.
+Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94.
+Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95.
+Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96.
+Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97.
+Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98.
+Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99.