summaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bench/lists-100.v107
-rw-r--r--test-suite/bench/lists_100.v107
-rwxr-xr-xtest-suite/check129
-rw-r--r--test-suite/failure/Case1.v1
-rw-r--r--test-suite/failure/Case10.v1
-rw-r--r--test-suite/failure/Case11.v1
-rw-r--r--test-suite/failure/Case12.v7
-rw-r--r--test-suite/failure/Case13.v5
-rw-r--r--test-suite/failure/Case14.v8
-rw-r--r--test-suite/failure/Case15.v6
-rw-r--r--test-suite/failure/Case16.v9
-rw-r--r--test-suite/failure/Case2.v13
-rw-r--r--test-suite/failure/Case3.v7
-rw-r--r--test-suite/failure/Case4.v7
-rw-r--r--test-suite/failure/Case5.v3
-rw-r--r--test-suite/failure/Case6.v10
-rw-r--r--test-suite/failure/Case7.v22
-rw-r--r--test-suite/failure/Case8.v8
-rw-r--r--test-suite/failure/Case9.v6
-rw-r--r--test-suite/failure/ClearBody.v8
-rw-r--r--test-suite/failure/Tauto.v20
-rw-r--r--test-suite/failure/cases.v6
-rw-r--r--test-suite/failure/check.v3
-rw-r--r--test-suite/failure/clash_cons.v16
-rw-r--r--test-suite/failure/clashes.v8
-rw-r--r--test-suite/failure/coqbugs0266.v7
-rw-r--r--test-suite/failure/fixpoint1.v9
-rw-r--r--test-suite/failure/illtype1.v8
-rw-r--r--test-suite/failure/ltac1.v5
-rw-r--r--test-suite/failure/ltac2.v6
-rw-r--r--test-suite/failure/ltac3.v2
-rw-r--r--test-suite/failure/ltac4.v4
-rw-r--r--test-suite/failure/params_ind.v4
-rw-r--r--test-suite/failure/positivity.v8
-rw-r--r--test-suite/failure/redef.v9
-rw-r--r--test-suite/failure/search.v8
-rw-r--r--test-suite/failure/universes-buraliforti.v227
-rw-r--r--test-suite/failure/universes-sections1.v8
-rw-r--r--test-suite/failure/universes-sections2.v10
-rw-r--r--test-suite/failure/universes.v3
-rw-r--r--test-suite/failure/universes2.v5
-rw-r--r--test-suite/ideal-features/Apply.v26
-rw-r--r--test-suite/ideal-features/Case3.v28
-rw-r--r--test-suite/ideal-features/Case4.v39
-rw-r--r--test-suite/ideal-features/Case8.v40
-rw-r--r--test-suite/kernel/inds.mv3
-rw-r--r--test-suite/modules/Demo.v55
-rw-r--r--test-suite/modules/Nametab.v48
-rw-r--r--test-suite/modules/Nat.v19
-rw-r--r--test-suite/modules/PO.v57
-rw-r--r--test-suite/modules/Przyklad.v193
-rw-r--r--test-suite/modules/Tescik.v30
-rw-r--r--test-suite/modules/fun_objects.v32
-rw-r--r--test-suite/modules/grammar.v15
-rw-r--r--test-suite/modules/ind.v13
-rw-r--r--test-suite/modules/mod_decl.v55
-rw-r--r--test-suite/modules/modeq.v22
-rw-r--r--test-suite/modules/modul.v39
-rw-r--r--test-suite/modules/obj.v26
-rw-r--r--test-suite/modules/objects.v33
-rw-r--r--test-suite/modules/pliczek.v3
-rw-r--r--test-suite/modules/plik.v4
-rw-r--r--test-suite/modules/sig.v29
-rw-r--r--test-suite/modules/sub_objects.v33
-rw-r--r--test-suite/output/Arith.out4
-rw-r--r--test-suite/output/Arith.v2
-rw-r--r--test-suite/output/Cases.out4
-rw-r--r--test-suite/output/Cases.v5
-rw-r--r--test-suite/output/Coercions.out4
-rw-r--r--test-suite/output/Coercions.v9
-rw-r--r--test-suite/output/Fixpoint.v7
-rw-r--r--test-suite/output/Implicit.out5
-rw-r--r--test-suite/output/Implicit.v18
-rw-r--r--test-suite/output/InitSyntax.out6
-rw-r--r--test-suite/output/InitSyntax.v4
-rw-r--r--test-suite/output/Intuition.out7
-rw-r--r--test-suite/output/Intuition.v5
-rw-r--r--test-suite/output/Nametab.out28
-rw-r--r--test-suite/output/Nametab.v48
-rw-r--r--test-suite/output/RealSyntax.out4
-rw-r--r--test-suite/output/RealSyntax.v3
-rw-r--r--test-suite/output/Remark2.out1
-rw-r--r--test-suite/output/Remark2.v8
-rw-r--r--test-suite/output/Sum.out6
-rw-r--r--test-suite/output/Sum.v3
-rw-r--r--test-suite/output/TranspModtype.out10
-rw-r--r--test-suite/output/TranspModtype.v22
-rw-r--r--test-suite/output/ZSyntax.out26
-rw-r--r--test-suite/output/ZSyntax.v17
-rw-r--r--test-suite/output/implicits.out4
-rw-r--r--test-suite/output/implicits.v13
-rw-r--r--test-suite/success/Abstract.v826
-rw-r--r--test-suite/success/Case1.v15
-rw-r--r--test-suite/success/Case10.v26
-rw-r--r--test-suite/success/Case11.v11
-rw-r--r--test-suite/success/Case12.v60
-rw-r--r--test-suite/success/Case13.v33
-rw-r--r--test-suite/success/Case14.v16
-rw-r--r--test-suite/success/Case15.v48
-rw-r--r--test-suite/success/Case16.v9
-rw-r--r--test-suite/success/Case17.v45
-rw-r--r--test-suite/success/Case2.v11
-rw-r--r--test-suite/success/Case5.v14
-rw-r--r--test-suite/success/Case6.v19
-rw-r--r--test-suite/success/Case7.v16
-rw-r--r--test-suite/success/Case9.v55
-rw-r--r--test-suite/success/CaseAlias.v21
-rw-r--r--test-suite/success/Cases.v1597
-rw-r--r--test-suite/success/CasesDep.v405
-rw-r--r--test-suite/success/Check.v14
-rw-r--r--test-suite/success/Conjecture.v13
-rw-r--r--test-suite/success/DHyp.v14
-rw-r--r--test-suite/success/Decompose.v7
-rw-r--r--test-suite/success/Destruct.v13
-rw-r--r--test-suite/success/DiscrR.v41
-rw-r--r--test-suite/success/Discriminate.v11
-rw-r--r--test-suite/success/Field.v71
-rw-r--r--test-suite/success/Fourier.v16
-rw-r--r--test-suite/success/Funind.v440
-rw-r--r--test-suite/success/Generalize.v7
-rw-r--r--test-suite/success/Hints.v48
-rw-r--r--test-suite/success/Inductive.v34
-rw-r--r--test-suite/success/Injection.v34
-rw-r--r--test-suite/success/Inversion.v85
-rw-r--r--test-suite/success/LetIn.v11
-rw-r--r--test-suite/success/MatchFail.v28
-rw-r--r--test-suite/success/Mod_ltac.v20
-rw-r--r--test-suite/success/Mod_params.v78
-rw-r--r--test-suite/success/Mod_strengthen.v64
-rw-r--r--test-suite/success/NatRing.v10
-rw-r--r--test-suite/success/Omega.v89
-rw-r--r--test-suite/success/PPFix.v88
-rw-r--r--test-suite/success/Print.v20
-rw-r--r--test-suite/success/Projection.v45
-rw-r--r--test-suite/success/Record.v3
-rw-r--r--test-suite/success/Reg.v136
-rw-r--r--test-suite/success/Remark.v12
-rw-r--r--test-suite/success/Rename.v5
-rw-r--r--test-suite/success/Require.v3
-rw-r--r--test-suite/success/Scopes.v8
-rw-r--r--test-suite/success/Simplify_eq.v13
-rw-r--r--test-suite/success/Tauto.v240
-rw-r--r--test-suite/success/Try.v8
-rw-r--r--test-suite/success/cc.v83
-rw-r--r--test-suite/success/coercions.v11
-rw-r--r--test-suite/success/coqbugs0181.v7
-rw-r--r--test-suite/success/eauto.v49
-rw-r--r--test-suite/success/eqdecide.v29
-rw-r--r--test-suite/success/evars.v23
-rw-r--r--test-suite/success/fix.v51
-rw-r--r--test-suite/success/if.v5
-rw-r--r--test-suite/success/implicit.v31
-rw-r--r--test-suite/success/import_lib.v202
-rw-r--r--test-suite/success/import_mod.v75
-rw-r--r--test-suite/success/inds_type_sec.v10
-rw-r--r--test-suite/success/induct.v17
-rw-r--r--test-suite/success/ltac.v70
-rw-r--r--test-suite/success/mutual_ind.v41
-rw-r--r--test-suite/success/options.v34
-rw-r--r--test-suite/success/refine.v30
-rw-r--r--test-suite/success/setoid_test.v104
-rw-r--r--test-suite/success/unfold.v15
-rw-r--r--test-suite/success/univers.v19
-rw-r--r--test-suite/tactics/TestRefine.v203
164 files changed, 7141 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.
diff --git a/test-suite/check b/test-suite/check
new file mode 100755
index 00000000..1c7822d1
--- /dev/null
+++ b/test-suite/check
@@ -0,0 +1,129 @@
+#!/bin/sh
+
+# Automatic test of Coq
+
+if [ "$1" = -byte ]; then
+ command7="../bin/coqtop.byte -translate -q -batch -load-vernac-source"
+else
+ command7="../bin/coqtop -translate -q -batch -load-vernac-source"
+fi
+
+if [ "$1" = -byte ]; then
+ command="../bin/coqtop.byte -q -batch -load-vernac-source"
+else
+ command="../bin/coqtop -q -batch -load-vernac-source"
+fi
+
+# on compte le nombre de tests et de succès
+nbtests=0
+nbtestsok=0
+
+# La fonction suivante teste le compilateur sur des fichiers qu'il doit
+# accepter
+test_success() {
+ for f in $1/*.v; do
+ nbtests=`expr $nbtests + 1`
+ printf " "$f"..."
+ $command7 $f > /dev/null 2>&1
+ if [ $? = 0 ]; then
+ mv "$f"8 tmp8.v
+ $command tmp8.v > /dev/null 2>&1
+ if [ $? = 0 ]; then
+ echo "Ok"
+ nbtestsok=`expr $nbtestsok + 1`
+ else
+ echo "V8 Error! (should be accepted)"
+ fi
+ rm tmp8.v
+ else
+ echo "V7 Error! (should be accepted)"
+ fi
+ done
+ for f in $1/*.v8; do
+ nbtests=`expr $nbtests + 1`
+ printf " "$f"..."
+ cp $f tmp8.v
+ $command tmp8.v > /dev/null 2>&1
+ if [ $? = 0 ]; then
+ echo "Ok"
+ nbtestsok=`expr $nbtestsok + 1`
+ else
+ echo "V8 Error! (should be accepted)"
+ fi
+ rm tmp8.v
+ done
+}
+
+# La fonction suivante teste le compilateur sur des fichiers qu'il doit
+# refuser
+test_failure() {
+ for f in $1/*.v; do
+ nbtests=`expr $nbtests + 1`
+ printf " "$f"..."
+ $command7 $f > /dev/null 2>&1
+ if [ $? != 0 ]; then
+ echo "Ok"
+ nbtestsok=`expr $nbtestsok + 1`
+ else
+ echo "Error! (should be rejected)"
+ fi
+ done
+}
+
+# La fonction suivante teste la sortie des fichiers qu'elle exécute
+test_output() {
+ for f in $1/*.v; do
+ nbtests=`expr $nbtests + 1`
+ printf " "$f"..."
+ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+ $command7 $f | tail +3 > $tmpoutput 2>&1
+ foutput=`dirname $f`/`basename $f .v`.out
+ diff $tmpoutput $foutput > /dev/null
+ if [ $? = 0 ]; then
+ echo "Ok"
+ nbtestsok=`expr $nbtestsok + 1`
+ else
+ echo "Error! (unexpected output)"
+ fi
+ done
+}
+
+# La fonction suivante teste l'analyseur syntaxique fournit par "parser"
+# Elle fonctionne comme test_output
+test_parser() {
+ if [ -d $1 ]; then
+ for f in $1/*.v; do
+ nbtests=`expr $nbtests + 1`
+ printf " "$f"..."
+ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+ foutput=`dirname $f`/`basename $f .v`.out
+ echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1
+ perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
+ $tmpoutput | grep -i error > /dev/null
+ if [ $? = 0 ] ; then
+ echo "Error! (unexpected output)"
+ else
+ echo "Ok"
+ nbtestsok=`expr $nbtestsok + 1`
+ fi
+ done
+ fi
+}
+
+# Programme principal
+
+# echo "Output tests"
+# test_output output
+echo "[Output tests are off]"
+echo "Success tests"
+test_success success
+echo "Failure tests"
+test_failure failure
+echo "Parser tests"
+test_parser parser
+pourcentage=`expr 100 \* $nbtestsok / $nbtests`
+echo
+echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"
+
+
+
diff --git a/test-suite/failure/Case1.v b/test-suite/failure/Case1.v
new file mode 100644
index 00000000..fafcafc1
--- /dev/null
+++ b/test-suite/failure/Case1.v
@@ -0,0 +1 @@
+Type Cases O of x => O | O => (S O) end.
diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v
new file mode 100644
index 00000000..ee47544d
--- /dev/null
+++ b/test-suite/failure/Case10.v
@@ -0,0 +1 @@
+Type [x:nat]<nat> Cases x of ((S x) as b) => (S b) end.
diff --git a/test-suite/failure/Case11.v b/test-suite/failure/Case11.v
new file mode 100644
index 00000000..c39a76ca
--- /dev/null
+++ b/test-suite/failure/Case11.v
@@ -0,0 +1 @@
+Type [x:nat]<nat> Cases x of ((S x) as b) => (S b x) end.
diff --git a/test-suite/failure/Case12.v b/test-suite/failure/Case12.v
new file mode 100644
index 00000000..b56eac0d
--- /dev/null
+++ b/test-suite/failure/Case12.v
@@ -0,0 +1,7 @@
+
+Type [x:nat]<nat> Cases x of
+ ((S x) as b) => <nat>Cases x of
+ x => x
+ end
+ end.
+
diff --git a/test-suite/failure/Case13.v b/test-suite/failure/Case13.v
new file mode 100644
index 00000000..8a4d75b6
--- /dev/null
+++ b/test-suite/failure/Case13.v
@@ -0,0 +1,5 @@
+Type [x:nat]<nat> Cases x of
+ ((S x) as b) => <nat>Cases x of
+ x => (S b x)
+ end
+ end.
diff --git a/test-suite/failure/Case14.v b/test-suite/failure/Case14.v
new file mode 100644
index 00000000..a198d068
--- /dev/null
+++ b/test-suite/failure/Case14.v
@@ -0,0 +1,8 @@
+Inductive List [A:Set] :Set :=
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Definition NIL := (Nil nat).
+Type <(List nat)>Cases (Nil nat) of
+ NIL => NIL
+ | _ => NIL
+ end.
diff --git a/test-suite/failure/Case15.v b/test-suite/failure/Case15.v
new file mode 100644
index 00000000..a27b07f8
--- /dev/null
+++ b/test-suite/failure/Case15.v
@@ -0,0 +1,6 @@
+(* Non exhaustive pattern-matching *)
+
+Check [x]Cases x x of
+ O (S (S y)) => true
+ | O (S x) => false
+ | (S y) O => true end. \ No newline at end of file
diff --git a/test-suite/failure/Case16.v b/test-suite/failure/Case16.v
new file mode 100644
index 00000000..f994a8f2
--- /dev/null
+++ b/test-suite/failure/Case16.v
@@ -0,0 +1,9 @@
+(* Check for redundant clauses *)
+
+Check [x]Cases x x of
+ O (S (S y)) => true
+ | (S _) (S (S y)) => true
+ | _ (S (S x)) => false
+ | (S y) O => true
+ | _ _ => true
+end.
diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v
new file mode 100644
index 00000000..183f612b
--- /dev/null
+++ b/test-suite/failure/Case2.v
@@ -0,0 +1,13 @@
+Inductive IFExpr : Set :=
+ Var : nat -> IFExpr
+ | Tr : IFExpr
+ | Fa : IFExpr
+ | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr.
+
+Type [F:IFExpr]
+ <Prop>Cases F of
+ (IfE (Var _) H I) => True
+ | (IfE _ _ _) => False
+ | _ => True
+ end.
+
diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v
new file mode 100644
index 00000000..2c651b87
--- /dev/null
+++ b/test-suite/failure/Case3.v
@@ -0,0 +1,7 @@
+Inductive List [A:Set] :Set :=
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Type [l:(List nat)]<nat>Cases l of
+ (Nil nat) =>O
+ | (Cons a l) => (S a)
+ end.
diff --git a/test-suite/failure/Case4.v b/test-suite/failure/Case4.v
new file mode 100644
index 00000000..d00c9a05
--- /dev/null
+++ b/test-suite/failure/Case4.v
@@ -0,0 +1,7 @@
+
+Definition Berry := [x,y,z:bool]
+ Cases x y z of
+ true false _ => O
+ | false _ true => (S O)
+ | _ true false => (S (S O))
+end.
diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v
new file mode 100644
index 00000000..bdb5544b
--- /dev/null
+++ b/test-suite/failure/Case5.v
@@ -0,0 +1,3 @@
+Inductive MS: Set := X:MS->MS | Y:MS->MS.
+
+Type [p:MS]<nat>Cases p of (X x) => O end.
diff --git a/test-suite/failure/Case6.v b/test-suite/failure/Case6.v
new file mode 100644
index 00000000..f588d275
--- /dev/null
+++ b/test-suite/failure/Case6.v
@@ -0,0 +1,10 @@
+Inductive List [A:Set] :Set :=
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+
+Type <(List nat)>Cases (Nil nat) of
+ NIL => NIL
+ | (CONS _ _) => NIL
+
+ end.
+
diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v
new file mode 100644
index 00000000..3718f198
--- /dev/null
+++ b/test-suite/failure/Case7.v
@@ -0,0 +1,22 @@
+Inductive listn : nat-> Set :=
+ niln : (listn O)
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Definition length1:= [n:nat] [l:(listn n)]
+ Cases l of
+ (consn n _ (consn m _ _)) => (S (S m))
+ |(consn n _ _) => (S O)
+ | _ => O
+ end.
+
+Type [n:nat]
+ [l:(listn n)]
+ <nat>Cases n of
+ O => O
+ | (S n) =>
+ <([_:nat]nat)>Cases l of
+ niln => (S O)
+ | l' => (length1 (S n) l')
+ end
+ end.
+
diff --git a/test-suite/failure/Case8.v b/test-suite/failure/Case8.v
new file mode 100644
index 00000000..7f6bb615
--- /dev/null
+++ b/test-suite/failure/Case8.v
@@ -0,0 +1,8 @@
+Inductive List [A:Set] :Set :=
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Type <nat>Cases (Nil nat) of
+ ((Nil_) as b) =>b
+ |((Cons _ _ _) as d) => d
+ end.
+
diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v
new file mode 100644
index 00000000..e8d8e89a
--- /dev/null
+++ b/test-suite/failure/Case9.v
@@ -0,0 +1,6 @@
+Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}.
+Type <nat>Cases (compare O O) of
+ (* k<i *) (left _ _ (left _ _ _)) => O
+ | (* k=i *) (left _ _ _) => O
+ | (* k>i *) (right _ _ _) => O end.
+
diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v
new file mode 100644
index 00000000..ca8e3c68
--- /dev/null
+++ b/test-suite/failure/ClearBody.v
@@ -0,0 +1,8 @@
+(* ClearBody must check that removing the body of definition does not
+ invalidate the well-typabilility of the visible goal *)
+
+Goal True.
+LetTac n:=O.
+LetTac I:=(refl_equal nat O).
+Change (n=O) in (Type of I).
+ClearBody n.
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
new file mode 100644
index 00000000..fb9a27bb
--- /dev/null
+++ b/test-suite/failure/Tauto.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(**** Tactics Tauto and Intuition ****)
+
+(**** Tauto:
+ Tactic for automating proof in Intuionnistic Propositional Calculus, based on
+ the contraction-free LJT of Dickhoff ****)
+
+(**** Intuition:
+ Simplifications of goals, based on LJT calcul ****)
+
+(* Fails because Tauto does not perform any Apply *)
+Goal ((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y).
+Proof.
+ Tauto.
diff --git a/test-suite/failure/cases.v b/test-suite/failure/cases.v
new file mode 100644
index 00000000..a27b07f8
--- /dev/null
+++ b/test-suite/failure/cases.v
@@ -0,0 +1,6 @@
+(* Non exhaustive pattern-matching *)
+
+Check [x]Cases x x of
+ O (S (S y)) => true
+ | O (S x) => false
+ | (S y) O => true end. \ No newline at end of file
diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v
new file mode 100644
index 00000000..0bf7091c
--- /dev/null
+++ b/test-suite/failure/check.v
@@ -0,0 +1,3 @@
+Implicits eq [1].
+
+Check (eq bool true).
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
new file mode 100644
index 00000000..56cd73f4
--- /dev/null
+++ b/test-suite/failure/clash_cons.v
@@ -0,0 +1,16 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(* Teste la verification d'unicite des noms de constr *)
+
+
+Inductive X : Set :=
+ cons : X.
+
+Inductive Y : Set :=
+ cons : Y.
+
diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v
new file mode 100644
index 00000000..fcfd29fe
--- /dev/null
+++ b/test-suite/failure/clashes.v
@@ -0,0 +1,8 @@
+(* Submitted by David Nowak *)
+
+(* Simpler to forbid the definition of n as a global than to write it
+ S.n to keep n accessible... *)
+
+Section S.
+Variable n:nat.
+Inductive P : Set := n : P.
diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v
new file mode 100644
index 00000000..2ac6c4f0
--- /dev/null
+++ b/test-suite/failure/coqbugs0266.v
@@ -0,0 +1,7 @@
+(* It is forbidden to erase a variable (or a local def) that is used in
+ the current goal. *)
+Section S.
+Local a:=O.
+Definition b:=a.
+Goal b=b.
+Clear a.
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
new file mode 100644
index 00000000..742e9774
--- /dev/null
+++ b/test-suite/failure/fixpoint1.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+Fixpoint PreParadox [u:unit] : False := (PreParadox u).
+Definition Paradox := (PreParadox tt). \ No newline at end of file
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
new file mode 100644
index 00000000..aff43ff1
--- /dev/null
+++ b/test-suite/failure/illtype1.v
@@ -0,0 +1,8 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+Check (S S).
diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v
new file mode 100644
index 00000000..d0256619
--- /dev/null
+++ b/test-suite/failure/ltac1.v
@@ -0,0 +1,5 @@
+(* Check all variables are different in a Context *)
+Tactic Definition X := Match Context With [ x:?; x:? |- ? ] -> Apply x.
+Goal True->True->True.
+Intros.
+X.
diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v
new file mode 100644
index 00000000..55925a7a
--- /dev/null
+++ b/test-suite/failure/ltac2.v
@@ -0,0 +1,6 @@
+(* Check that Match arguments are forbidden *)
+Tactic Definition E x := Apply x.
+Goal True->True.
+E (Match Context With [ |- ? ] -> Intro H).
+(* Should fail with "Immediate Match producing tactics not allowed in
+ local definitions" *)
diff --git a/test-suite/failure/ltac3.v b/test-suite/failure/ltac3.v
new file mode 100644
index 00000000..bfccc546
--- /dev/null
+++ b/test-suite/failure/ltac3.v
@@ -0,0 +1,2 @@
+(* Proposed by Benjamin *)
+Definition A := Try REflexivity.
diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v
new file mode 100644
index 00000000..d1e4e892
--- /dev/null
+++ b/test-suite/failure/ltac4.v
@@ -0,0 +1,4 @@
+(* Check static globalisation of tactic names *)
+(* Proposed by Benjamin (mars 2002) *)
+Goal (n:nat)n=n.
+Induction n; Try REflexivity.
diff --git a/test-suite/failure/params_ind.v b/test-suite/failure/params_ind.v
new file mode 100644
index 00000000..20689128
--- /dev/null
+++ b/test-suite/failure/params_ind.v
@@ -0,0 +1,4 @@
+Inductive list [A:Set] : Set :=
+ nil : (list A)
+| cons : A -> (list A->A)-> (list A).
+
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
new file mode 100644
index 00000000..b43eb899
--- /dev/null
+++ b/test-suite/failure/positivity.v
@@ -0,0 +1,8 @@
+(************************************************************************)
+(* 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 t:Set := c: (t -> nat) -> t.
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
new file mode 100644
index 00000000..8f3aedac
--- /dev/null
+++ b/test-suite/failure/redef.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+Definition toto := Set.
+Definition toto := Set.
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
new file mode 100644
index 00000000..e8ca8494
--- /dev/null
+++ b/test-suite/failure/search.v
@@ -0,0 +1,8 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+SearchPattern ? = ? outside n_existe_pas.
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
new file mode 100644
index 00000000..01d46133
--- /dev/null
+++ b/test-suite/failure/universes-buraliforti.v
@@ -0,0 +1,227 @@
+(* Check that Burali-Forti paradox does not go through *)
+
+(* Source: contrib/Rocq/PARADOX/{Logics,BuraliForti},v *)
+
+(* Some properties about relations on objects in Type *)
+
+ Inductive ACC [A : Type; R : A->A->Prop] : A->Prop :=
+ ACC_intro : (x:A)((y:A)(R y x)->(ACC A R y))->(ACC A R x).
+
+ Lemma ACC_nonreflexive:
+ (A:Type)(R:A->A->Prop)(x:A)(ACC A R x)->(R x x)->False.
+Induction 1; Intros.
+Exact (H1 x0 H2 H2).
+Save.
+
+ Definition WF := [A:Type][R:A->A->Prop](x:A)(ACC A R x).
+
+
+Section Inverse_Image.
+
+ Variables A,B:Type; R:B->B->Prop; f:A->B.
+
+ Definition Rof : A->A->Prop := [x,y:A](R (f x) (f y)).
+
+ Remark ACC_lemma : (y:B)(ACC B R y)->(x:A)(y==(f x))->(ACC A Rof x).
+ Induction 1; Intros.
+ Constructor; Intros.
+ Apply (H1 (f y0)); Trivial.
+ Elim H2 using eqT_ind_r; Trivial.
+ Save.
+
+ Lemma ACC_inverse_image : (x:A)(ACC B R (f x)) -> (ACC A Rof x).
+ Intros; Apply (ACC_lemma (f x)); Trivial.
+ Save.
+
+ Lemma WF_inverse_image: (WF B R)->(WF A Rof).
+ Red; Intros; Apply ACC_inverse_image; Auto.
+ Save.
+
+End Inverse_Image.
+
+
+(* Remark: the paradox is written in Type, but also works in Prop or Set. *)
+
+Section Burali_Forti_Paradox.
+
+ Definition morphism := [A:Type][R:A->A->Prop][B:Type][S:B->B->Prop][f:A->B]
+ (x,y:A)(R x y)->(S (f x) (f y)).
+
+ (* The hypothesis of the paradox:
+ assumes there exists an universal system of notations, i.e:
+ - A type A0
+ - An injection i0 from relations on any type into A0
+ - The proof that i0 is injective modulo morphism
+ *)
+ Variable A0 : Type. (* Type_i *)
+ Variable i0 : (X:Type)(X->X->Prop)->A0. (* X: Type_j *)
+ Hypothesis inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop)
+ (i0 X1 R1)==(i0 X2 R2)
+ ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)).
+
+ (* Embedding of x in y: x and y are images of 2 well founded relations
+ R1 and R2, the ordinal of R2 being strictly greater than that of R1.
+ *)
+ Record emb [x,y:A0]: Prop := {
+ X1: Type;
+ R1: X1->X1->Prop;
+ eqx: x==(i0 X1 R1);
+ X2: Type;
+ R2: X2->X2->Prop;
+ eqy: y==(i0 X2 R2);
+ W2: (WF X2 R2);
+ f: X1->X2;
+ fmorph: (morphism X1 R1 X2 R2 f);
+ maj: X2;
+ majf: (z:X1)(R2 (f z) maj) }.
+
+
+ Lemma emb_trans: (x,y,z:A0)(emb x y)->(emb y z)->(emb x z).
+Intros.
+Case H; Intros.
+Case H0; Intros.
+Generalize eqx0; Clear eqx0.
+Elim eqy using eqT_ind_r; Intro.
+Case (inj ? ? ? ? eqx0); Intros.
+Exists X1 R1 X3 R3 [x:X1](f0 (x0 (f x))) maj0; Trivial.
+Red; Auto.
+Defined.
+
+
+ Lemma ACC_emb: (X:Type)(R:X->X->Prop)(x:X)(ACC X R x)
+ ->(Y:Type)(S:Y->Y->Prop)(f:Y->X)(morphism Y S X R f)
+ ->((y:Y)(R (f y) x))
+ ->(ACC A0 emb (i0 Y S)).
+Induction 1; Intros.
+Constructor; Intros.
+Case H4; Intros.
+Elim eqx using eqT_ind_r.
+Case (inj X2 R2 Y S).
+Apply sym_eqT; Assumption.
+
+Intros.
+Apply H1 with y:=(f (x1 maj)) f:=[x:X1](f (x1 (f0 x))); Try Red; Auto.
+Defined.
+
+ (* The embedding relation is well founded *)
+ Lemma WF_emb: (WF A0 emb).
+Constructor; Intros.
+Case H; Intros.
+Elim eqx using eqT_ind_r.
+Apply ACC_emb with X:=X2 R:=R2 x:=maj f:=f; Trivial.
+Defined.
+
+
+ (* The following definition enforces Type_j >= Type_i *)
+ Definition Omega: A0 := (i0 A0 emb).
+
+
+Section Subsets.
+
+ Variable a: A0.
+
+ (* We define the type of elements of A0 smaller than a w.r.t embedding.
+ The Record is in Type, but it is possible to avoid such structure. *)
+ Record sub: Type := {
+ witness : A0;
+ emb_wit : (emb witness a) }.
+
+ (* F is its image through i0 *)
+ Definition F : A0 := (i0 sub (Rof ? ? emb witness)).
+
+ (* F is embedded in Omega:
+ - the witness projection is a morphism
+ - a is an upper bound because emb_wit proves that witness is
+ smaller than a.
+ *)
+ Lemma F_emb_Omega: (emb F Omega).
+Exists sub (Rof ? ? emb witness) A0 emb witness a; Trivial.
+Exact WF_emb.
+
+Red; Trivial.
+
+Exact emb_wit.
+Defined.
+
+End Subsets.
+
+
+ Definition fsub: (a,b:A0)(emb a b)->(sub a)->(sub b):=
+ [_,_][H][x]
+ (Build_sub ? (witness ? x) (emb_trans ? ? ? (emb_wit ? x) H)).
+
+ (* F is a morphism: a < b => F(a) < F(b)
+ - the morphism from F(a) to F(b) is fsub above
+ - the upper bound is a, which is in F(b) since a < b
+ *)
+ Lemma F_morphism: (morphism A0 emb A0 emb F).
+Red; Intros.
+Exists (sub x) (Rof ? ? emb (witness x)) (sub y)
+ (Rof ? ? emb (witness y)) (fsub x y H) (Build_sub ? x H);
+Trivial.
+Apply WF_inverse_image.
+Exact WF_emb.
+
+Unfold morphism Rof fsub; Simpl; Intros.
+Trivial.
+
+Unfold Rof fsub; Simpl; Intros.
+Apply emb_wit.
+Defined.
+
+
+ (* Omega is embedded in itself:
+ - F is a morphism
+ - Omega is an upper bound of the image of F
+ *)
+ Lemma Omega_refl: (emb Omega Omega).
+Exists A0 emb A0 emb F Omega; Trivial.
+Exact WF_emb.
+
+Exact F_morphism.
+
+Exact F_emb_Omega.
+Defined.
+
+ (* The paradox is that Omega cannot be embedded in itself, since
+ the embedding relation is well founded.
+ *)
+ Theorem Burali_Forti: False.
+Apply ACC_nonreflexive with A0 emb Omega.
+Apply WF_emb.
+
+Exact Omega_refl.
+
+Defined.
+
+End Burali_Forti_Paradox.
+
+
+ (* The following type seems to satisfy the hypothesis of the paradox.
+ But it does not!
+ *)
+ Record A0: Type := (* Type_i' *)
+ i0 { X0: Type; R0: X0->X0->Prop }. (* X0: Type_j' *)
+
+
+ (* Note: this proof uses a large elimination of A0. *)
+ Lemma inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop)
+ (i0 X1 R1)==(i0 X2 R2)
+ ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)).
+Intros.
+Change Cases (i0 X1 R1) (i0 X2 R2) of
+ (i0 x1 r1) (i0 x2 r2) => (EXT f | (morphism x1 r1 x2 r2 f))
+ end.
+Case H; Simpl.
+Exists [x:X1]x.
+Red; Trivial.
+Defined.
+
+(* The following command raises 'Error: Universe Inconsistency'.
+ To allow large elimination of A0, i0 must not be a large constructor.
+ Hence, the constraint Type_j' < Type_i' is added, which is incompatible
+ with the constraint j >= i in the paradox.
+*)
+
+ Definition Paradox: False := (Burali_Forti A0 i0 inj).
+
diff --git a/test-suite/failure/universes-sections1.v b/test-suite/failure/universes-sections1.v
new file mode 100644
index 00000000..c4eef34b
--- /dev/null
+++ b/test-suite/failure/universes-sections1.v
@@ -0,0 +1,8 @@
+(* Check that constraints on definitions are preserved by discharging *)
+
+Section A.
+ Definition Type2 := Type.
+ Definition Type1 := Type : Type2.
+End A.
+
+Definition Inconsistency := Type2 : Type1.
diff --git a/test-suite/failure/universes-sections2.v b/test-suite/failure/universes-sections2.v
new file mode 100644
index 00000000..1872dac1
--- /dev/null
+++ b/test-suite/failure/universes-sections2.v
@@ -0,0 +1,10 @@
+(* Check that constraints on locals are preserved by discharging *)
+
+Definition Type2 := Type.
+
+Section A.
+ Local Type1 := Type : Type2.
+ Definition Type1' := Type1.
+End A.
+
+Definition Inconsistency := Type2 : Type1'.
diff --git a/test-suite/failure/universes.v b/test-suite/failure/universes.v
new file mode 100644
index 00000000..6fada6f1
--- /dev/null
+++ b/test-suite/failure/universes.v
@@ -0,0 +1,3 @@
+Definition Type2 := Type.
+Definition Type1 := Type : Type2.
+Definition Inconsistency := Type2 : Type1.
diff --git a/test-suite/failure/universes2.v b/test-suite/failure/universes2.v
new file mode 100644
index 00000000..a6c8ba43
--- /dev/null
+++ b/test-suite/failure/universes2.v
@@ -0,0 +1,5 @@
+(* Example submitted by Randy Pollack *)
+
+Parameter K: (T:Type)T->T.
+Check (K ((T:Type)T->T) K).
+(* Universe Inconsistency *)
diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
new file mode 100644
index 00000000..bba356f2
--- /dev/null
+++ b/test-suite/ideal-features/Apply.v
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* This needs unification on type *)
+
+Goal (n,m:nat)(eq nat (S m) (S n)).
+Intros.
+Apply f_equal.
+
+(* f_equal : (A,B:Set; f:(A->B); x,y:A)x=y->(f x)=(f y) *)
+(* and A cannot be deduced from the goal but only from the type of f, x or y *)
+
+
+(* This needs step by step unfolding *)
+
+Fixpoint T [n:nat] : Prop := Cases n of O => True | (S p) => n=n->(T p) end.
+Require Arith.
+
+Goal (T (3))->(T (1)).
+Intro H.
+Apply H.
diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v
new file mode 100644
index 00000000..e9dba1e3
--- /dev/null
+++ b/test-suite/ideal-features/Case3.v
@@ -0,0 +1,28 @@
+Inductive Le : nat->nat->Set :=
+ LeO: (n:nat)(Le O n)
+| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+
+Parameter iguales : (n,m:nat)(h:(Le n m))Prop .
+
+Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of
+ (LeO O) => True
+ | (LeS (S x) (S y) H) => (iguales (S x) (S y) H)
+ | _ => False end.
+
+
+Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of
+ (LeO O) => True
+ | (LeS (S x) O H) => (iguales (S x) O H)
+ | _ => False end.
+
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+Type
+[n:nat]
+ <[n:nat]n=O\/~n=O>Cases n of
+ O => (or_introl ? ~O=O (refl_equal ? O))
+ | (S O) => (or_intror (S O)=O ? (discr_l O))
+ | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x)))
+
+ end.
+
diff --git a/test-suite/ideal-features/Case4.v b/test-suite/ideal-features/Case4.v
new file mode 100644
index 00000000..d8f14a4e
--- /dev/null
+++ b/test-suite/ideal-features/Case4.v
@@ -0,0 +1,39 @@
+Inductive listn : nat-> Set :=
+ niln : (listn O)
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive empty : (n:nat)(listn n)-> Prop :=
+ intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | ((consn n O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y))
+ | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+ end.
+
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | (consn n O y) => (or_intror (empty (S n) (consn n O y)) ?
+ (inv_empty n O y))
+ | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ?
+ (inv_empty n a y))
+
+ end.
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | ((consn O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y))
+ | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+ end.
+
diff --git a/test-suite/ideal-features/Case8.v b/test-suite/ideal-features/Case8.v
new file mode 100644
index 00000000..73b55028
--- /dev/null
+++ b/test-suite/ideal-features/Case8.v
@@ -0,0 +1,40 @@
+Inductive listn : nat-> Set :=
+ niln : (listn O)
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive empty : (n:nat)(listn n)-> Prop :=
+ intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | ((consn n O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y))
+ | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+ end.
+
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | (consn n O y) => (or_intror (empty (S n) (consn n O y)) ?
+ (inv_empty n O y))
+ | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ?
+ (inv_empty n a y))
+
+ end.
+
+
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | ((consn O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y))
+ | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+ end.
diff --git a/test-suite/kernel/inds.mv b/test-suite/kernel/inds.mv
new file mode 100644
index 00000000..bd1cc49f
--- /dev/null
+++ b/test-suite/kernel/inds.mv
@@ -0,0 +1,3 @@
+Inductive [] nat : Set := O : nat | S : nat->nat.
+Check Construct nat 0 1.
+Check Construct nat 0 2.
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v
new file mode 100644
index 00000000..1e9273f0
--- /dev/null
+++ b/test-suite/modules/Demo.v
@@ -0,0 +1,55 @@
+Module M.
+ Definition t:=nat.
+ Definition x:=O.
+End M.
+
+Print M.t.
+
+
+Module Type SIG.
+ Parameter t:Set.
+ Parameter x:t.
+End SIG.
+
+
+Module F[X:SIG].
+ Definition t:=X.t->X.t.
+ Definition x:t.
+ Intro.
+ Exact X.x.
+ Defined.
+ Definition y:=X.x.
+End F.
+
+
+Module N := F M.
+
+Print N.t.
+Eval Compute in N.t.
+
+
+Module N' : SIG := N.
+
+Print N'.t.
+Eval Compute in N'.t.
+
+
+Module N'' <: SIG := F N.
+
+Print N''.t.
+Eval Compute in N''.t.
+
+Eval Compute in N''.x.
+
+
+Module N''' : SIG with Definition t:=nat->nat := N.
+
+Print N'''.t.
+Eval Compute in N'''.t.
+
+Print N'''.x.
+
+
+Import N'''.
+
+Print t. \ No newline at end of file
diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v
new file mode 100644
index 00000000..61966c7c
--- /dev/null
+++ b/test-suite/modules/Nametab.v
@@ -0,0 +1,48 @@
+Module Q.
+ Module N.
+ Module K.
+ Definition id:=Set.
+ End K.
+ End N.
+End Q.
+
+(* Bad *) Locate id.
+(* Bad *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK *) Locate Q.N.K.id.
+(* OK *) Locate Top.Q.N.K.id.
+
+(* Bad *) Locate K.
+(* Bad *) Locate N.K.
+(* OK *) Locate Q.N.K.
+(* OK *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK *) Locate Q.N.
+(* OK *) Locate Top.Q.N.
+
+(* OK *) Locate Q.
+(* OK *) Locate Top.Q.
+
+
+
+Import Q.N.
+
+
+(* Bad *) Locate id.
+(* OK *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK *) Locate Q.N.K.id.
+(* OK *) Locate Top.Q.N.K.id.
+
+(* OK *) Locate K.
+(* Bad *) Locate N.K.
+(* OK *) Locate Q.N.K.
+(* OK *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK *) Locate Q.N.
+(* OK *) Locate Top.Q.N.
+
+(* OK *) Locate Q.
+(* OK *) Locate Top.Q.
diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
new file mode 100644
index 00000000..d3e98ae4
--- /dev/null
+++ b/test-suite/modules/Nat.v
@@ -0,0 +1,19 @@
+Definition T:=nat.
+
+Definition le:=Peano.le.
+
+Hints Unfold le.
+
+Lemma le_refl:(n:nat)(le n n).
+ Auto.
+Qed.
+
+Require Le.
+
+Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
+ EAuto with arith.
+Qed.
+
+Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
+ EAuto with arith.
+Qed.
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
new file mode 100644
index 00000000..9ba3fb2e
--- /dev/null
+++ b/test-suite/modules/PO.v
@@ -0,0 +1,57 @@
+Implicit Arguments On.
+
+Implicits fst.
+Implicits snd.
+
+Module Type PO.
+ Parameter T:Set.
+ Parameter le:T->T->Prop.
+
+ Axiom le_refl : (x:T)(le x x).
+ Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z).
+ Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y).
+
+ Hints Resolve le_refl le_trans le_antis.
+End PO.
+
+
+Module Pair[X:PO][Y:PO] <: PO.
+ Definition T:=X.T*Y.T.
+ Definition le:=[p1,p2]
+ (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
+
+ Hints Unfold le.
+
+ Lemma le_refl : (p:T)(le p p).
+ Info Auto.
+ Qed.
+
+ Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
+ Unfold le; Intuition; Info EAuto.
+ Qed.
+
+ Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2).
+ NewDestruct p1.
+ NewDestruct p2.
+ Unfold le.
+ Intuition.
+ CutRewrite t=t1.
+ CutRewrite t0=t2.
+ Reflexivity.
+
+ Info Auto.
+
+ Info Auto.
+ Qed.
+
+End Pair.
+
+
+
+Read Module Nat.
+
+Module NN := Pair Nat Nat.
+
+Lemma zz_min : (p:NN.T)(NN.le (O,O) p).
+ Info Auto with arith.
+Qed.
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
new file mode 100644
index 00000000..4f4c2066
--- /dev/null
+++ b/test-suite/modules/Przyklad.v
@@ -0,0 +1,193 @@
+Definition ifte := [T:Set][A:Prop][B:Prop][s:(sumbool A B)][th:T][el:T]
+ if s then [_]th else [_]el.
+
+Implicits ifte.
+
+Lemma Reflexivity_provable :
+ (A:Set)(a:A)(s:{a=a}+{~a=a})(EXT x| s==(left ? ? x)).
+Intros.
+Elim s.
+Intro x.
+Split with x; Reflexivity.
+
+Intro.
+Absurd a=a; Auto.
+
+Save.
+
+Lemma Disequality_provable :
+ (A:Set)(a,b:A)(~a=b)->(s:{a=b}+{~a=b})(EXT x| s==(right ? ? x)).
+Intros.
+Elim s.
+Intro.
+Absurd a=a; Auto.
+
+Intro.
+Split with b0; Reflexivity.
+
+Save.
+
+Module Type ELEM.
+ Parameter T : Set.
+ Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}.
+End ELEM.
+
+Module Type SET[Elt : ELEM].
+ Parameter T : Set.
+ Parameter empty : T.
+ Parameter add : Elt.T -> T -> T.
+ Parameter find : Elt.T -> T -> bool.
+
+ (* Axioms *)
+
+ Axiom find_empty_false :
+ (e:Elt.T) (find e empty) = false.
+
+ Axiom find_add_true :
+ (s:T) (e:Elt.T) (find e (add e s)) = true.
+
+ Axiom find_add_false :
+ (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') ->
+ (find e (add e' s))=(find e s).
+
+End SET.
+
+Module FuncDict[E : ELEM].
+ Definition T := E.T -> bool.
+ Definition empty := [e':E.T] false.
+ Definition find := [e':E.T] [s:T] (s e').
+ Definition add := [e:E.T][s:T][e':E.T]
+ (ifte (E.eq_dec e e') true (find e' s)).
+
+ Lemma find_empty_false : (e:E.T) (find e empty) = false.
+ Auto.
+ Qed.
+
+ Lemma find_add_true :
+ (s:T) (e:E.T) (find e (add e s)) = true.
+
+ Intros.
+ Unfold find add.
+ Elim (Reflexivity_provable ? ? (E.eq_dec e e)).
+ Intros.
+ Rewrite H.
+ Auto.
+
+ Qed.
+
+ Lemma find_add_false :
+ (s:T) (e:E.T) (e':E.T) ~(e=e') ->
+ (find e (add e' s))=(find e s).
+ Intros.
+ Unfold add find.
+ Cut (EXT x:? | (E.eq_dec e' e)==(right ? ? x)).
+ Intros.
+ Elim H0.
+ Intros.
+ Rewrite H1.
+ Unfold ifte.
+ Reflexivity.
+
+ Apply Disequality_provable.
+ Auto.
+
+ Qed.
+
+End FuncDict.
+
+Module F : SET := FuncDict.
+
+
+Module Nat.
+ Definition T:=nat.
+ Lemma eq_dec : (a,a':T){a=a'}+{~ a=a'}.
+ Decide Equality.
+ Qed.
+End Nat.
+
+
+Module SetNat:=F Nat.
+
+
+Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false.
+Apply SetNat.find_empty_false.
+Save.
+
+(***************************************************************************)
+Module Lemmas[G:SET][E:ELEM].
+
+ Module ESet:=G E.
+
+ Lemma commute : (S:ESet.T)(a1,a2:E.T)
+ let S1 = (ESet.add a1 (ESet.add a2 S)) in
+ let S2 = (ESet.add a2 (ESet.add a1 S)) in
+ (a:E.T)(ESet.find a S1)=(ESet.find a S2).
+
+ Intros.
+ Unfold S1 S2.
+ Elim (E.eq_dec a a1); Elim (E.eq_dec a a2); Intros H1 H2;
+ Try Rewrite <- H1; Try Rewrite <- H2;
+ Repeat
+ (Try (Rewrite ESet.find_add_true; Auto);
+ Try (Rewrite ESet.find_add_false; Auto);
+ Auto).
+ Save.
+End Lemmas.
+
+
+Inductive list [A:Set] : Set := nil : (list A)
+ | cons : A -> (list A) -> (list A).
+
+Module ListDict[E : ELEM].
+ Definition T := (list E.T).
+ Definition elt := E.T.
+
+ Definition empty := (nil elt).
+ Definition add := [e:elt][s:T] (cons elt e s).
+ Fixpoint find [e:elt; s:T] : bool :=
+ Cases s of
+ nil => false
+ | (cons e' s') => (ifte (E.eq_dec e e')
+ true
+ (find e s'))
+ end.
+
+ Definition find_empty_false := [e:elt] (refl_equal bool false).
+
+ Lemma find_add_true :
+ (s:T) (e:E.T) (find e (add e s)) = true.
+ Intros.
+ Simpl.
+ Elim (Reflexivity_provable ? ? (E.eq_dec e e)).
+ Intros.
+ Rewrite H.
+ Auto.
+
+ Qed.
+
+
+ Lemma find_add_false :
+ (s:T) (e:E.T) (e':E.T) ~(e=e') ->
+ (find e (add e' s))=(find e s).
+ Intros.
+ Simpl.
+ Elim (Disequality_provable ? ? ? H (E.eq_dec e e')).
+ Intros.
+ Rewrite H0.
+ Simpl.
+ Reflexivity.
+ Save.
+
+
+End ListDict.
+
+
+Module L : SET := ListDict.
+
+
+
+
+
+
+
+
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
new file mode 100644
index 00000000..13c28418
--- /dev/null
+++ b/test-suite/modules/Tescik.v
@@ -0,0 +1,30 @@
+
+Module Type ELEM.
+ Parameter A:Set.
+ Parameter x:A.
+End ELEM.
+
+Module Nat.
+ Definition A:=nat.
+ Definition x:=O.
+End Nat.
+
+Module List[X:ELEM].
+ Inductive list : Set := nil : list
+ | cons : X.A -> list -> list.
+
+ Definition head :=
+ [l:list]Cases l of
+ nil => X.x
+ | (cons x _) => x
+ end.
+
+ Definition singl := [x:X.A] (cons x nil).
+
+ Lemma head_singl : (x:X.A)(head (singl x))=x.
+ Auto.
+ Qed.
+
+End List.
+
+Module N:=(List Nat).
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
new file mode 100644
index 00000000..0f8eef84
--- /dev/null
+++ b/test-suite/modules/fun_objects.v
@@ -0,0 +1,32 @@
+Implicit Arguments On.
+
+Module Type SIG.
+ Parameter id:(A:Set)A->A.
+End SIG.
+
+Module M[X:SIG].
+ Definition idid := (X.id X.id).
+ Definition id := (idid X.id).
+End M.
+
+Module N:=M.
+
+Module Nat.
+ Definition T := nat.
+ Definition x := O.
+ Definition id := [A:Set][x:A]x.
+End Nat.
+
+Module Z:=(N Nat).
+
+Check (Z.idid O).
+
+Module P[Y:SIG] := N.
+
+Module Y:=P Nat Z.
+
+Check (Y.id O).
+
+
+
+
diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v
new file mode 100644
index 00000000..fb734b5d
--- /dev/null
+++ b/test-suite/modules/grammar.v
@@ -0,0 +1,15 @@
+Module N.
+Definition f:=plus.
+Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
+Check (f O O).
+End N.
+Check (N.f O O).
+Import N.
+Check (N.f O O).
+Check (f O O).
+Module M:=N.
+Check (f O O).
+Check (N.f O O).
+Import M.
+Check (f O O).
+Check (N.f O O).
diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v
new file mode 100644
index 00000000..94c344bb
--- /dev/null
+++ b/test-suite/modules/ind.v
@@ -0,0 +1,13 @@
+Module Type SIG.
+ Inductive w:Set:=A:w.
+ Parameter f : w->w.
+End SIG.
+
+Module M:SIG.
+ Inductive w:Set:=A:w.
+ Definition f:=[x]Cases x of A => A end.
+End M.
+
+Module N:=M.
+
+Check (N.f M.A).
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
new file mode 100644
index 00000000..867b8a11
--- /dev/null
+++ b/test-suite/modules/mod_decl.v
@@ -0,0 +1,55 @@
+Module Type SIG.
+ Definition A:Set. (*error*)
+ Axiom A:Set.
+End SIG.
+
+Module M0.
+ Definition A:Set.
+ Exact nat.
+ Save.
+End M0.
+
+Module M1:SIG.
+ Definition A:=nat.
+End M1.
+
+Module M2<:SIG.
+ Definition A:=nat.
+End M2.
+
+Module M3:=M0.
+
+Module M4:SIG:=M0.
+
+Module M5<:SIG:=M0.
+
+
+Module F[X:SIG]:=X.
+
+
+Declare Module M6.
+
+
+Module Type T.
+
+ Declare Module M0.
+ Lemma A:Set (*error*).
+ Axiom A:Set.
+ End M0.
+
+ Declare Module M1:SIG.
+
+ Declare Module M2<:SIG.
+ Definition A:=nat.
+ End M2.
+
+ Declare Module M3:=M0.
+
+ Declare Module M4:SIG:=M0. (* error *)
+
+ Declare Module M5<:SIG:=M0.
+
+ Declare Module M6:=F M0. (* error *)
+
+ Module M7.
+End T. \ No newline at end of file
diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
new file mode 100644
index 00000000..73448dc7
--- /dev/null
+++ b/test-suite/modules/modeq.v
@@ -0,0 +1,22 @@
+Module M.
+ Definition T:=nat.
+ Definition x:T:=O.
+End M.
+
+Module Type SIG.
+ Declare Module M:=Top.M.
+ Module Type SIG.
+ Parameter T:Set.
+ End SIG.
+ Declare Module N:SIG.
+End SIG.
+
+Module Z.
+ Module M:=Top.M.
+ Module Type SIG.
+ Parameter T:Set.
+ End SIG.
+ Module N:=M.
+End Z.
+
+Module A:SIG:=Z.
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
new file mode 100644
index 00000000..5612ea75
--- /dev/null
+++ b/test-suite/modules/modul.v
@@ -0,0 +1,39 @@
+Module M.
+ Parameter rel:nat -> nat -> Prop.
+
+ Axiom w : (n:nat)(rel O (S n)).
+
+ Hints Resolve w.
+
+ Grammar constr constr8 :=
+ not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
+
+ Print Hint *.
+
+ Lemma w1 : (O#(S O)).
+ Auto.
+ Save.
+
+End M.
+
+(*Lemma w1 : (M.rel O (S O)).
+Auto.
+*)
+
+Import M.
+
+Print Hint *.
+Lemma w1 : (O#(S O)).
+Print Hint.
+Print Hint *.
+
+Auto.
+Save.
+
+Check (O#O).
+Locate rel.
+
+Locate M.
+
+Module N:=Top.M.
+
diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
new file mode 100644
index 00000000..2231e084
--- /dev/null
+++ b/test-suite/modules/obj.v
@@ -0,0 +1,26 @@
+Implicit Arguments On.
+
+Module M.
+ Definition a:=[s:Set]s.
+ Print a.
+End M.
+
+Print M.a.
+
+Module K.
+ Definition app:=[A,B:Set; f:(A->B); x:A](f x).
+ Module N.
+ Definition apap:=[A,B:Set](app (app 1!A 2!B)).
+ Print app.
+ Print apap.
+ End N.
+ Print N.apap.
+End K.
+
+Print K.app.
+Print K.N.apap.
+
+Module W:=K.N.
+
+Print W.apap.
+
diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v
new file mode 100644
index 00000000..418ece44
--- /dev/null
+++ b/test-suite/modules/objects.v
@@ -0,0 +1,33 @@
+Module Type SET.
+ Axiom T:Set.
+ Axiom x:T.
+End SET.
+
+Implicit Arguments On.
+
+Module M[X:SET].
+ Definition T := nat.
+ Definition x := O.
+ Definition f := [A:Set][x:A]X.x.
+End M.
+
+Module N:=M.
+
+Module Nat.
+ Definition T := nat.
+ Definition x := O.
+End Nat.
+
+Module Z:=(N Nat).
+
+Check (Z.f O).
+
+Module P[Y:SET] := N.
+
+Module Y:=P Z Nat.
+
+Check (Y.f O).
+
+
+
+
diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v
new file mode 100644
index 00000000..6061ace3
--- /dev/null
+++ b/test-suite/modules/pliczek.v
@@ -0,0 +1,3 @@
+Require Export plik.
+
+Definition tutu := [X:Set](toto X).
diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v
new file mode 100644
index 00000000..f1f59df0
--- /dev/null
+++ b/test-suite/modules/plik.v
@@ -0,0 +1,4 @@
+Definition toto:=[x:Set]x.
+
+Grammar constr constr8 :=
+ toto [ "#" constr7($b) ] -> [ (toto $b) ].
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
new file mode 100644
index 00000000..eb8736bb
--- /dev/null
+++ b/test-suite/modules/sig.v
@@ -0,0 +1,29 @@
+Module M.
+ Module Type SIG.
+ Parameter T:Set.
+ Parameter x:T.
+ End SIG.
+ Module N:SIG.
+ Definition T:=nat.
+ Definition x:=O.
+ End N.
+End M.
+
+Module N:=M.
+
+Module Type SPRYT.
+ Declare Module N.
+ Definition T:=M.N.T.
+ Parameter x:T.
+ End N.
+End SPRYT.
+
+Module K:SPRYT:=N.
+Module K':SPRYT:=M.
+
+Module Type SIG.
+ Definition T:Set:=M.N.T.
+ Parameter x:T.
+End SIG.
+
+Module J:SIG:=M.N.
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
new file mode 100644
index 00000000..1bd4faef
--- /dev/null
+++ b/test-suite/modules/sub_objects.v
@@ -0,0 +1,33 @@
+Set Implicit Arguments.
+
+
+Module M.
+ Definition id:=[A:Set][x:A]x.
+
+ Module Type SIG.
+ Parameter idid:(A:Set)A->A.
+ End SIG.
+
+ Module N.
+ Definition idid:=[A:Set][x:A](id x).
+ Grammar constr constr8 :=
+ not_eq [ "#" constr7($b) ] -> [ (idid $b) ].
+ Notation inc := (plus (S O)).
+ End N.
+
+ Definition zero:=(N.idid O).
+
+End M.
+
+Definition zero := (M.N.idid O).
+Definition jeden := (M.N.inc O).
+
+Module Goly:=M.N.
+
+Definition Gole_zero := (Goly.idid O).
+Definition Goly_jeden := (Goly.inc O).
+
+Module Ubrany : M.SIG := M.N.
+
+Definition Ubrane_zero := (Ubrany.idid O).
+
diff --git a/test-suite/output/Arith.out b/test-suite/output/Arith.out
new file mode 100644
index 00000000..210dd6ad
--- /dev/null
+++ b/test-suite/output/Arith.out
@@ -0,0 +1,4 @@
+[n:nat](S (S n))
+ : nat->nat
+[n:nat](S (plus n n))
+ : nat->nat
diff --git a/test-suite/output/Arith.v b/test-suite/output/Arith.v
new file mode 100644
index 00000000..39989dfc
--- /dev/null
+++ b/test-suite/output/Arith.v
@@ -0,0 +1,2 @@
+Check [n](S (S n)).
+Check [n](S (plus n n)).
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
new file mode 100644
index 00000000..5f13caaf
--- /dev/null
+++ b/test-suite/output/Cases.out
@@ -0,0 +1,4 @@
+t_rect =
+[P:(t->Type); f:([x:=t](x0:x)(P x0)->(P (k x0)))]
+ Fix F{F [t:t] : (P t) := <P>Cases t of (k x x0) => (f x0 (F x0)) end}
+ : (P:(t->Type))([x:=t](x0:x)(P x0)->(P (k x0)))->(t:t)(P t)
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
new file mode 100644
index 00000000..7483e8c4
--- /dev/null
+++ b/test-suite/output/Cases.v
@@ -0,0 +1,5 @@
+(* Cases with let-in in constructors types *)
+
+Inductive t : Set := k : [x:=t]x -> x.
+
+Print t_rect.
diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out
new file mode 100644
index 00000000..63e042d8
--- /dev/null
+++ b/test-suite/output/Coercions.out
@@ -0,0 +1,4 @@
+(P x)
+ : Prop
+(R x x)
+ : Prop
diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v
new file mode 100644
index 00000000..61b69038
--- /dev/null
+++ b/test-suite/output/Coercions.v
@@ -0,0 +1,9 @@
+(* Submitted by Randy Pollack *)
+
+Record pred [S:Set]: Type := { sp_pred :> S -> Prop }.
+Record rel [S:Set]: Type := { sr_rel :> S -> S -> Prop }.
+
+Section testSection.
+Variables S: Set; P: (pred S); R: (rel S); x:S.
+Check (P x).
+Check (R x x).
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
new file mode 100644
index 00000000..270fff4e
--- /dev/null
+++ b/test-suite/output/Fixpoint.v
@@ -0,0 +1,7 @@
+Require PolyList.
+
+Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) :=
+ [_,_,f,l]Cases l of
+ nil => (nil ?)
+ | (cons a l) => (cons (f a) (F ? ? f l))
+ end}.
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
new file mode 100644
index 00000000..f9cf9efc
--- /dev/null
+++ b/test-suite/output/Implicit.out
@@ -0,0 +1,5 @@
+d2 = [x:nat](d1 1!x)
+ : (x,x0:nat)x0=x ->x0=x
+
+Positions [1; 2] are implicit
+Argument scopes are [nat_scope nat_scope _]
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
new file mode 100644
index 00000000..2dea0d18
--- /dev/null
+++ b/test-suite/output/Implicit.v
@@ -0,0 +1,18 @@
+Set Implicit Arguments.
+
+(* Suggested by Pierre Casteran (bug #169) *)
+(* Argument 3 is needed to typecheck and should be printed *)
+Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)).
+Check (compose 3!nat S).
+
+(* Better to explicitly display the arguments inferable from a
+ position that could disappear after reduction *)
+Inductive ex [A:Set;P:A->Prop] : Prop
+ := ex_intro : (x:A)(P x)->(ex P).
+Check (ex_intro 2![_]True 3!O I).
+
+(* Test for V8 printing of implicit by names *)
+Definition d1 [y;x;h:x=y:>nat] := h.
+Definition d2 [x] := (!d1 x).
+
+Print d2.
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
new file mode 100644
index 00000000..d7120f89
--- /dev/null
+++ b/test-suite/output/InitSyntax.out
@@ -0,0 +1,6 @@
+Inductive sig2 [A : Set; P : A->Prop; Q : A->Prop] : Set :=
+ exist2 : (x:A)(P x)->(Q x)->(sig2 A P Q)
+(EX x:nat|x=x)
+ : Prop
+[b:bool](if b then b else b)
+ : bool->bool
diff --git a/test-suite/output/InitSyntax.v b/test-suite/output/InitSyntax.v
new file mode 100644
index 00000000..90fad371
--- /dev/null
+++ b/test-suite/output/InitSyntax.v
@@ -0,0 +1,4 @@
+(* Soumis par Pierre *)
+Print sig2.
+Check (EX x:nat|x=x).
+Check [b:bool]if b then b else b.
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
new file mode 100644
index 00000000..cadb35c6
--- /dev/null
+++ b/test-suite/output/Intuition.out
@@ -0,0 +1,7 @@
+1 subgoal
+
+ m : Z
+ n : Z
+ H : `m >= n`
+ ============================
+ `m >= m`
diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v
new file mode 100644
index 00000000..c0508c90
--- /dev/null
+++ b/test-suite/output/Intuition.v
@@ -0,0 +1,5 @@
+Require ZArith_base.
+Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`.
+Intros; Intuition.
+Show.
+Abort.
diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
new file mode 100644
index 00000000..505821d7
--- /dev/null
+++ b/test-suite/output/Nametab.out
@@ -0,0 +1,28 @@
+id is not a defined object
+K.id is not a defined object
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+K is not a defined object
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
+id is not a defined object
+Constant Top.Q.N.K.id
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+Module Top.Q.N.K
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v
new file mode 100644
index 00000000..61966c7c
--- /dev/null
+++ b/test-suite/output/Nametab.v
@@ -0,0 +1,48 @@
+Module Q.
+ Module N.
+ Module K.
+ Definition id:=Set.
+ End K.
+ End N.
+End Q.
+
+(* Bad *) Locate id.
+(* Bad *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK *) Locate Q.N.K.id.
+(* OK *) Locate Top.Q.N.K.id.
+
+(* Bad *) Locate K.
+(* Bad *) Locate N.K.
+(* OK *) Locate Q.N.K.
+(* OK *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK *) Locate Q.N.
+(* OK *) Locate Top.Q.N.
+
+(* OK *) Locate Q.
+(* OK *) Locate Top.Q.
+
+
+
+Import Q.N.
+
+
+(* Bad *) Locate id.
+(* OK *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK *) Locate Q.N.K.id.
+(* OK *) Locate Top.Q.N.K.id.
+
+(* OK *) Locate K.
+(* Bad *) Locate N.K.
+(* OK *) Locate Q.N.K.
+(* OK *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK *) Locate Q.N.
+(* OK *) Locate Top.Q.N.
+
+(* OK *) Locate Q.
+(* OK *) Locate Top.Q.
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
new file mode 100644
index 00000000..fa30656b
--- /dev/null
+++ b/test-suite/output/RealSyntax.out
@@ -0,0 +1,4 @@
+``32``
+ : R
+``-31``
+ : R
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
new file mode 100644
index 00000000..d976dcc1
--- /dev/null
+++ b/test-suite/output/RealSyntax.v
@@ -0,0 +1,3 @@
+Require Reals.
+Check ``32``.
+Check ``-31``.
diff --git a/test-suite/output/Remark2.out b/test-suite/output/Remark2.out
new file mode 100644
index 00000000..adabc2fe
--- /dev/null
+++ b/test-suite/output/Remark2.out
@@ -0,0 +1 @@
+B.C.t is not a defined object
diff --git a/test-suite/output/Remark2.v b/test-suite/output/Remark2.v
new file mode 100644
index 00000000..e1ef57a0
--- /dev/null
+++ b/test-suite/output/Remark2.v
@@ -0,0 +1,8 @@
+Section A.
+Section B.
+Section C.
+Remark t : True. Proof I.
+End C.
+End B.
+End A.
+Locate B.C.t.
diff --git a/test-suite/output/Sum.out b/test-suite/output/Sum.out
new file mode 100644
index 00000000..22422602
--- /dev/null
+++ b/test-suite/output/Sum.out
@@ -0,0 +1,6 @@
+nat+nat+{True}
+ : Set
+{True}+{True}+{True}
+ : Set
+nat+{True}+{True}
+ : Set
diff --git a/test-suite/output/Sum.v b/test-suite/output/Sum.v
new file mode 100644
index 00000000..aceadd12
--- /dev/null
+++ b/test-suite/output/Sum.v
@@ -0,0 +1,3 @@
+Check nat+nat+{True}.
+Check {True}+{True}+{True}.
+Check nat+{True}+{True}.
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
new file mode 100644
index 00000000..41e8648b
--- /dev/null
+++ b/test-suite/output/TranspModtype.out
@@ -0,0 +1,10 @@
+TrM.A = M.A
+ : Set
+
+OpM.A = M.A
+ : Set
+
+TrM.B = M.B
+ : Set
+
+*** [ OpM.B : Set ]
diff --git a/test-suite/output/TranspModtype.v b/test-suite/output/TranspModtype.v
new file mode 100644
index 00000000..27b1fb9f
--- /dev/null
+++ b/test-suite/output/TranspModtype.v
@@ -0,0 +1,22 @@
+Module Type SIG.
+ Axiom A:Set.
+ Axiom B:Set.
+End SIG.
+
+Module M:SIG.
+ Definition A:=nat.
+ Definition B:=nat.
+End M.
+
+Module N<:SIG:=M.
+
+Module TranspId[X:SIG] <: SIG with Definition A:=X.A := X.
+Module OpaqueId[X:SIG] : SIG with Definition A:=X.A := X.
+
+Module TrM := TranspId M.
+Module OpM := OpaqueId M.
+
+Print TrM.A.
+Print OpM.A.
+Print TrM.B.
+Print OpM.B.
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
new file mode 100644
index 00000000..0fdc5b7e
--- /dev/null
+++ b/test-suite/output/ZSyntax.out
@@ -0,0 +1,26 @@
+`32`
+ : Z
+[f:(nat->Z)]`(f O)+0`
+ : (nat->Z)->Z
+[x:positive](POS (xO x))
+ : positive->Z
+[x:positive]`(POS x)+1`
+ : positive->Z
+[x:positive](POS x)
+ : positive->Z
+[x:positive](NEG (xO x))
+ : positive->Z
+[x:positive]`(POS (xO x))+0`
+ : positive->Z
+[x:positive]`(Zopp (POS (xO x)))`
+ : positive->Z
+[x:positive]`(Zopp (POS (xO x)))+0`
+ : positive->Z
+`(inject_nat (0))+1`
+ : Z
+`0+(inject_nat (plus (0) (0)))`
+ : Z
+`(inject_nat (0)) = 0`
+ : Prop
+`0+(inject_nat (11))`
+ : Z
diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v
new file mode 100644
index 00000000..49442b75
--- /dev/null
+++ b/test-suite/output/ZSyntax.v
@@ -0,0 +1,17 @@
+Require ZArith.
+Check `32`.
+Check [f:nat->Z]`(f O) + 0`.
+Check [x:positive]`(POS (xO x))`.
+Check [x:positive]`(POS x)+1`.
+Check [x:positive]`(POS x)`.
+Check [x:positive]`(NEG (xO x))`.
+Check [x:positive]`(POS (xO x))+0`.
+Check [x:positive]`(Zopp (POS (xO x)))`.
+Check [x:positive]`(Zopp (POS (xO x)))+0`.
+Check `(inject_nat O)+1`.
+Check (Zplus `0` (inject_nat (plus O O))).
+Check `(inject_nat O)=0`.
+
+(* Submitted by Pierre Casteran *)
+Require Arith.
+Check (Zplus `0` (inject_nat (11))).
diff --git a/test-suite/output/implicits.out b/test-suite/output/implicits.out
new file mode 100644
index 00000000..e4837199
--- /dev/null
+++ b/test-suite/output/implicits.out
@@ -0,0 +1,4 @@
+(compose 3!nat S)
+ : (nat->nat)->nat->nat
+(ex_intro 2![_:nat]True 3!(0) I)
+ : (ex [_:nat]True)
diff --git a/test-suite/output/implicits.v b/test-suite/output/implicits.v
new file mode 100644
index 00000000..d7ea7227
--- /dev/null
+++ b/test-suite/output/implicits.v
@@ -0,0 +1,13 @@
+Set Implicit Arguments.
+
+(* Suggested by Pierre Casteran (bug #169) *)
+(* Argument 3 is needed to typecheck and should be printed *)
+Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)).
+Check (compose 3!nat S).
+
+(* Better to explicitly display the arguments inferable from a
+ position that could disappear after reduction *)
+Inductive ex [A:Set;P:A->Prop] : Prop
+ := ex_intro : (x:A)(P x)->(ex P).
+Check (ex_intro 2![_]True 3!O I).
+
diff --git a/test-suite/success/Abstract.v8 b/test-suite/success/Abstract.v8
new file mode 100644
index 00000000..21a985bc
--- /dev/null
+++ b/test-suite/success/Abstract.v8
@@ -0,0 +1,26 @@
+
+(* Cf coqbugs #546 *)
+
+Require Import Omega.
+
+Section S.
+
+Variables n m : nat.
+Variable H : n<m.
+
+Inductive Dummy : nat -> Set :=
+| Dummy0 : Dummy 0
+| Dummy2 : Dummy 2
+| DummyApp : forall i j, Dummy i -> Dummy j -> Dummy (i+j).
+
+Definition Bug : Dummy (2*n).
+Proof.
+induction n.
+ simpl ; apply Dummy0.
+ replace (2 * S n0) with (2*n0 + 2) ; auto with arith.
+ apply DummyApp.
+ 2:exact Dummy2.
+ apply IHn0 ; abstract omega.
+Defined.
+
+End S.
diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v
new file mode 100644
index 00000000..2d5a5134
--- /dev/null
+++ b/test-suite/success/Case1.v
@@ -0,0 +1,15 @@
+(* Testing eta-expansion of elimination predicate *)
+
+Section NATIND2.
+Variable P : nat -> Type.
+Variable H0 : (P O).
+Variable H1 : (P (S O)).
+Variable H2 : (n:nat)(P n)->(P (S (S n))).
+Fixpoint nat_ind2 [n:nat] : (P n) :=
+ <P>Cases n of
+ O => H0
+ | (S O) => H1
+ | (S (S n)) => (H2 n (nat_ind2 n))
+ end.
+End NATIND2.
+
diff --git a/test-suite/success/Case10.v b/test-suite/success/Case10.v
new file mode 100644
index 00000000..73413c47
--- /dev/null
+++ b/test-suite/success/Case10.v
@@ -0,0 +1,26 @@
+(* ============================================== *)
+(* To test compilation of dependent case *)
+(* Multiple Patterns *)
+(* ============================================== *)
+Inductive skel: Type :=
+ PROP: skel
+ | PROD: skel->skel->skel.
+
+Parameter Can : skel -> Type.
+Parameter default_can : (s:skel) (Can s).
+
+
+Type [s1,s2:skel]
+ <[s1,_:skel](Can s1)>Cases s1 s2 of
+ PROP PROP => (default_can PROP)
+ | s1 _ => (default_can s1)
+ end.
+
+
+Type [s1,s2:skel]
+<[s1:skel][_:skel](Can s1)>Cases s1 s2 of
+ PROP PROP => (default_can PROP)
+| (PROP as s) _ => (default_can s)
+| ((PROD s1 s2) as s) PROP => (default_can s)
+| ((PROD s1 s2) as s) _ => (default_can s)
+end.
diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v
new file mode 100644
index 00000000..580cd87d
--- /dev/null
+++ b/test-suite/success/Case11.v
@@ -0,0 +1,11 @@
+(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
+(* Problème rapporté par Solange Coupet *)
+
+Section A.
+
+Variables Alpha:Set; Beta:Set.
+
+Definition nodep_prod_of_dep: (sigS Alpha [a:Alpha]Beta)-> Alpha*Beta:=
+[c] Cases c of (existS a b)=>(a,b) end.
+
+End A.
diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
new file mode 100644
index 00000000..284695f4
--- /dev/null
+++ b/test-suite/success/Case12.v
@@ -0,0 +1,60 @@
+(* This example was proposed by Cuihtlauac ALVARADO *)
+
+Require PolyList.
+
+Fixpoint mult2 [n:nat] : nat :=
+Cases n of
+| O => O
+| (S n) => (S (S (mult2 n)))
+end.
+
+Inductive list : nat -> Set :=
+| nil : (list O)
+| cons : (n:nat)(list (mult2 n))->(list (S (S (mult2 n)))).
+
+Type
+[P:((n:nat)(list n)->Prop);
+ f:(P O nil);
+ f0:((n:nat; l:(list (mult2 n)))
+ (P (mult2 n) l)->(P (S (S (mult2 n))) (cons n l)))]
+ Fix F
+ {F [n:nat; l:(list n)] : (P n l) :=
+ <P>Cases l of
+ nil => f
+ | (cons n0 l0) => (f0 n0 l0 (F (mult2 n0) l0))
+ end}.
+
+Inductive list' : nat -> Set :=
+| nil' : (list' O)
+| cons' : (n:nat)[m:=(mult2 n)](list' m)->(list' (S (S m))).
+
+Fixpoint length [n; l:(list' n)] : nat :=
+ Cases l of
+ nil' => O
+ | (cons' _ m l0) => (S (length m l0))
+ end.
+
+Type
+[P:((n:nat)(list' n)->Prop);
+ f:(P O nil');
+ f0:((n:nat)
+ [m:=(mult2 n)](l:(list' m))(P m l)->(P (S (S m)) (cons' n l)))]
+ Fix F
+ {F [n:nat; l:(list' n)] : (P n l) :=
+ <P>
+ Cases l of
+ nil' => f
+ | (cons' n0 m l0) => (f0 n0 l0 (F m l0))
+ end}.
+
+(* Check on-the-fly insertion of let-in patterns for compatibility *)
+
+Inductive list'' : nat -> Set :=
+| nil'' : (list'' O)
+| cons'' : (n:nat)[m:=(mult2 n)](list'' m)->[p:=(S (S m))](list'' p).
+
+Check Fix length { length [n; l:(list'' n)] : nat :=
+ Cases l of
+ nil'' => O
+ | (cons'' n l0) => (S (length (mult2 n) l0))
+ end }.
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
new file mode 100644
index 00000000..71c9191d
--- /dev/null
+++ b/test-suite/success/Case13.v
@@ -0,0 +1,33 @@
+(* Check coercions in patterns *)
+
+Inductive I : Set :=
+ C1 : nat -> I
+| C2 : I -> I.
+
+Coercion C1 : nat >-> I.
+
+(* Coercion at the root of pattern *)
+Check [x]Cases x of (C2 n) => O | O => O | (S n) => n end.
+
+(* Coercion not at the root of pattern *)
+Check [x]Cases x of (C2 O) => O | _ => O end.
+
+(* Unification and coercions inside patterns *)
+Check [x:(option nat)]Cases x of None => O | (Some O) => O | _ => O end.
+
+(* Coercion up to delta-conversion, and unification *)
+Coercion somenat := (Some nat).
+Check [x]Cases x of None => O | O => O | (S n) => n end.
+
+(* Coercions with parameters *)
+Inductive listn : nat-> Set :=
+ niln : (listn O)
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive I' : nat -> Set :=
+ C1' : (n:nat) (listn n) -> (I' n)
+| C2' : (n:nat) (I' n) -> (I' n).
+
+Coercion C1' : listn >-> I'.
+Check [x:(I' O)]Cases x of (C2' _ _) => O | niln => O | _ => O end.
+Check [x:(I' O)]Cases x of (C2' _ niln) => O | _ => O end.
diff --git a/test-suite/success/Case14.v b/test-suite/success/Case14.v
new file mode 100644
index 00000000..edecee79
--- /dev/null
+++ b/test-suite/success/Case14.v
@@ -0,0 +1,16 @@
+(* Test of inference of elimination predicate for "if" *)
+(* submitted by Robert R Schneck *)
+
+Axiom bad : false = true.
+
+Definition try1 : False :=
+ <[b:bool][_:false=b](if b then False else True)>
+ Cases bad of refl_equal => I end.
+
+Definition try2 : False :=
+ <[b:bool][_:false=b]((if b then False else True)::Prop)>
+ Cases bad of refl_equal => I end.
+
+Definition try3 : False :=
+ <[b:bool][_:false=b](([b':bool] if b' then False else True) b)>
+ Cases bad of refl_equal => I end.
diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v
new file mode 100644
index 00000000..22944520
--- /dev/null
+++ b/test-suite/success/Case15.v
@@ -0,0 +1,48 @@
+(* Check compilation of multiple pattern-matching on terms non
+ apparently of inductive type *)
+
+(* Check that the non dependency in y is OK both in V7 and V8 *)
+Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of
+ | O y z' => (or_introl ? (z'=z') (refl_equal ? O))
+ | _ y O => (or_intror ?? (refl_equal ? O))
+ | x y _ => (or_introl ?? (refl_equal ? x))
+ end).
+
+(* Suggested by Pierre Letouzey (PR#207) *)
+Inductive Boite : Set :=
+ boite : (b:bool)(if b then nat else nat*nat)->Boite.
+
+Definition test := [B:Boite]<nat>Cases B of
+ (boite true n) => n
+| (boite false (n,m)) => (plus n m)
+end.
+
+(* Check lazyness of compilation ... future work
+Inductive I : Set := c : (b:bool)(if b then bool else nat)->I.
+
+Check [x]
+ Cases x of
+ (c (true as y) (true as x)) => (if x then y else true)
+ | (c false O) => true | _ => false
+ end.
+
+Check [x]
+ Cases x of
+ (c true true) => true
+ | (c false O) => true
+ | _ => false
+ end.
+
+(* Devrait produire ceci mais trouver le type intermediaire est coton ! *)
+Check
+ [x:I]
+ Cases x of
+ (c b y) =>
+ (<[b:bool](if b then bool else nat)->bool>if b
+ then [y](if y then true else false)
+ else [y]Cases y of
+ O => true
+ | (S _) => false
+ end y)
+ end.
+*)
diff --git a/test-suite/success/Case16.v b/test-suite/success/Case16.v
new file mode 100644
index 00000000..3f142fae
--- /dev/null
+++ b/test-suite/success/Case16.v
@@ -0,0 +1,9 @@
+(**********************************************************************)
+(* Test dependencies in constructors *)
+(**********************************************************************)
+
+Check [x : {b:bool|if b then True else False}]
+ <[x]let (b,_) = x in if b then True else False>Cases x of
+ | (exist true y) => y
+ | (exist false z) => z
+ end.
diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v
new file mode 100644
index 00000000..07d64958
--- /dev/null
+++ b/test-suite/success/Case17.v
@@ -0,0 +1,45 @@
+(* Check the synthesis of predicate from a cast in case of matching of
+ the first component (here [list bool]) of a dependent type (here [sigS])
+ (Simplification of an example from file parsing2.v of the Coq'Art
+ exercises) *)
+
+Require Import PolyList.
+
+Variable parse_rel : (list bool) -> (list bool) -> nat -> Prop.
+
+Variables l0:(list bool); rec:(l' : (list bool))
+ (le (length l') (S (length l0))) ->
+ {l'' : (list bool) &
+ {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} +
+ {(l'' : (list bool))(t : nat)~ (parse_rel l' l'' t)}.
+
+Axiom HHH : (A:Prop)A.
+
+Check (Cases (rec l0 (HHH ?)) of
+ | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?))
+ | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) =>
+ (inright ? ? (HHH ?))
+ | (inleft (existS _ _)) => (inright ? ? (HHH ?))
+ | (inright Hnp) => (inright ? ? (HHH ?))
+ end ::
+ {l'' : (list bool) &
+ {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} +
+ {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}).
+
+(* The same but with relative links to l0 and rec *)
+
+Check [l0:(list bool);rec:(l' : (list bool))
+ (le (length l') (S (length l0))) ->
+ {l'' : (list bool) &
+ {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} +
+ {(l'' : (list bool)) (t : nat) ~ (parse_rel l' l'' t)}]
+ (Cases (rec l0 (HHH ?)) of
+ | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?))
+ | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) =>
+ (inright ? ? (HHH ?))
+ | (inleft (existS _ _)) => (inright ? ? (HHH ?))
+ | (inright Hnp) => (inright ? ? (HHH ?))
+ end ::
+ {l'' : (list bool) &
+ {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} +
+ {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}).
diff --git a/test-suite/success/Case2.v b/test-suite/success/Case2.v
new file mode 100644
index 00000000..0aa7b5be
--- /dev/null
+++ b/test-suite/success/Case2.v
@@ -0,0 +1,11 @@
+(* ============================================== *)
+(* To test compilation of dependent case *)
+(* Nested patterns *)
+(* ============================================== *)
+
+Type <[n:nat]n=n>Cases O of
+ O => (refl_equal nat O)
+ | m => (refl_equal nat m)
+end.
+
+
diff --git a/test-suite/success/Case5.v b/test-suite/success/Case5.v
new file mode 100644
index 00000000..fe49cdf9
--- /dev/null
+++ b/test-suite/success/Case5.v
@@ -0,0 +1,14 @@
+
+Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
+Parameter discr_r : (n:nat) ~(O=(S n)).
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+
+Type
+[n:nat]
+ <[n:nat]n=O\/~n=O>Cases n of
+ O => (or_introl ? ~O=O (refl_equal ? O))
+ | (S O) => (or_intror (S O)=O ? (discr_l O))
+ | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x)))
+
+ end.
diff --git a/test-suite/success/Case6.v b/test-suite/success/Case6.v
new file mode 100644
index 00000000..a262251e
--- /dev/null
+++ b/test-suite/success/Case6.v
@@ -0,0 +1,19 @@
+Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
+Parameter discr_r : (n:nat) ~(O=(S n)).
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m :=
+[m:nat]
+ <[n,m:nat] n=m \/ ~n=m>Cases n m of
+ O O => (or_introl ? ~O=O (refl_equal ? O))
+
+ | O (S x) => (or_intror O=(S x) ? (discr_r x))
+
+ | (S x) O => (or_intror ? ~(S x)=O (discr_l x))
+
+ | ((S x) as N) ((S y) as M) =>
+ <N=M\/~N=M>Cases (eqdec x y) of
+ (or_introl h) => (or_introl ? ~N=M (f_equal nat nat S x y h))
+ | (or_intror h) => (or_intror N=M ? (ff x y h))
+ end
+ end.
diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v
new file mode 100644
index 00000000..6e2aea48
--- /dev/null
+++ b/test-suite/success/Case7.v
@@ -0,0 +1,16 @@
+Inductive List [A:Set] :Set :=
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Inductive Empty [A:Set] : (List A)-> Prop :=
+ intro_Empty: (Empty A (Nil A)).
+
+Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)).
+
+
+Type
+[A:Set]
+[l:(List A)]
+ <[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of
+ Nil => (or_introl ? ~(Empty A (Nil A)) (intro_Empty A))
+ | ((Cons a y) as b) => (or_intror (Empty A b) ? (inv_Empty A a y))
+ end.
diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v
new file mode 100644
index 00000000..a5d07405
--- /dev/null
+++ b/test-suite/success/Case9.v
@@ -0,0 +1,55 @@
+Inductive List [A:Set] :Set :=
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Inductive eqlong : (List nat)-> (List nat)-> Prop :=
+ eql_cons : (n,m:nat)(x,y:(List nat))
+ (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y))
+| eql_nil : (eqlong (Nil nat) (Nil nat)).
+
+
+Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)).
+Parameter V2 : (a:nat)(x:(List nat))
+ (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)).
+Parameter V3 : (a:nat)(x:(List nat))
+ (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)).
+Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat))
+ (eqlong (Cons nat a x)(Cons nat b y))
+ \/ ~(eqlong (Cons nat a x) (Cons nat b y)).
+
+Parameter nff : (n,m:nat)(x,y:(List nat))
+ ~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)).
+Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)).
+Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)).
+
+Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) :=
+[y:(List nat)]
+ <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of
+ Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil)
+
+ | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x))
+
+ | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x))
+
+ | ((Cons a x) as L1) ((Cons b y) as L2) =>
+ <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of
+ (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h))
+ | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h))
+ end
+ end.
+
+
+Type
+ <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of
+ Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil)
+
+ | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x))
+
+ | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x))
+
+ | ((Cons a x) as L1) ((Cons b y) as L2) =>
+ <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of
+ (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h))
+ | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h))
+ end
+ end.
+
diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v
new file mode 100644
index 00000000..b5f0e730
--- /dev/null
+++ b/test-suite/success/CaseAlias.v
@@ -0,0 +1,21 @@
+(* This has been a bug reported by Y. Bertot *)
+Inductive expr : Set :=
+ b: expr -> expr -> expr
+ | u: expr -> expr
+ | a: expr
+ | var: nat -> expr .
+
+Fixpoint f [t : expr] : expr :=
+ Cases t of
+ | (b t1 t2) => (b (f t1) (f t2))
+ | a => a
+ | x => (b t a)
+ end.
+
+Fixpoint f2 [t : expr] : expr :=
+ Cases t of
+ | (b t1 t2) => (b (f2 t1) (f2 t2))
+ | a => a
+ | x => (b x a)
+ end.
+
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
new file mode 100644
index 00000000..6ccd669a
--- /dev/null
+++ b/test-suite/success/Cases.v
@@ -0,0 +1,1597 @@
+(****************************************************************************)
+(* Pattern-matching when non inductive terms occur *)
+
+(* Dependent form of annotation *)
+Type <[n:nat]nat>Cases O eq of O x => O | (S x) y => x end.
+Type <[_,_:nat]nat>Cases O eq O of O x y => O | (S x) y z => x end.
+
+(* Non dependent form of annotation *)
+Type <nat>Cases O eq of O x => O | (S x) y => x end.
+
+(* Combining dependencies and non inductive arguments *)
+Type [A:Set][a:A][H:O=O]<[x][H]H==H>Cases H a of _ _ => (refl_eqT ? H) end.
+
+(* Interaction with coercions *)
+Parameter bool2nat : bool -> nat.
+Coercion bool2nat : bool >-> nat.
+Check [x](Cases x of O => true | (S _) => O end :: nat).
+
+(****************************************************************************)
+(* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *)
+
+Inductive IFExpr : Set :=
+ Var : nat -> IFExpr
+ | Tr : IFExpr
+ | Fa : IFExpr
+ | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr.
+
+Inductive List [A:Set] :Set :=
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Inductive listn : nat-> Set :=
+ niln : (listn O)
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive Listn [A:Set] : nat-> Set :=
+ Niln : (Listn A O)
+| Consn : (n:nat)nat->(Listn A n) -> (Listn A (S n)).
+
+Inductive Le : nat->nat->Set :=
+ LeO: (n:nat)(Le O n)
+| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+
+Inductive LE [n:nat] : nat->Set :=
+ LE_n : (LE n n) | LE_S : (m:nat)(LE n m)->(LE n (S m)).
+
+Require Bool.
+
+
+
+Inductive PropForm : Set :=
+ Fvar : nat -> PropForm
+ | Or : PropForm -> PropForm -> PropForm .
+
+Section testIFExpr.
+Definition Assign:= nat->bool.
+Parameter Prop_sem : Assign -> PropForm -> bool.
+
+Type [A:Assign][F:PropForm]
+ <bool>Cases F of
+ (Fvar n) => (A n)
+ | (Or F G) => (orb (Prop_sem A F) (Prop_sem A G))
+ end.
+
+Type [A:Assign][H:PropForm]
+ <bool>Cases H of
+ (Fvar n) => (A n)
+ | (Or F G) => (orb (Prop_sem A F) (Prop_sem A G))
+ end.
+End testIFExpr.
+
+
+
+Type [x:nat]<nat>Cases x of O => O | x => x end.
+
+Section testlist.
+Parameter A:Set.
+Inductive list : Set := nil : list | cons : A->list->list.
+Parameter inf: A->A->Prop.
+
+
+Definition list_Lowert2 :=
+ [a:A][l:list](<Prop>Cases l of nil => True
+ | (cons b l) =>(inf a b) end).
+
+Definition titi :=
+ [a:A][l:list](<list>Cases l of nil => l
+ | (cons b l) => l end).
+Reset list.
+End testlist.
+
+
+(* To test translation *)
+(* ------------------- *)
+
+
+Type <nat>Cases O of O => O | _ => O end.
+
+Type <nat>Cases O of
+ (O as b) => b
+ | (S O) => O
+ | (S (S x)) => x end.
+
+Type Cases O of
+ (O as b) => b
+ | (S O) => O
+ | (S (S x)) => x end.
+
+
+Type [x:nat]<nat>Cases x of
+ (O as b) => b
+ | (S x) => x end.
+
+Type [x:nat]Cases x of
+ (O as b) => b
+ | (S x) => x end.
+
+Type <nat>Cases O of
+ (O as b) => b
+ | (S x) => x end.
+
+Type <nat>Cases O of
+ x => x
+ end.
+
+Type Cases O of
+ x => x
+ end.
+
+Type <nat>Cases O of
+ O => O
+ | ((S x) as b) => b
+ end.
+
+Type [x:nat]<nat>Cases x of
+ O => O
+ | ((S x) as b) => b
+ end.
+
+Type [x:nat] Cases x of
+ O => O
+ | ((S x) as b) => b
+ end.
+
+
+Type <nat>Cases O of
+ O => O
+ | (S x) => O
+ end.
+
+
+Type <nat*nat>Cases O of
+ O => (O,O)
+ | (S x) => (x,O)
+ end.
+
+Type Cases O of
+ O => (O,O)
+ | (S x) => (x,O)
+ end.
+
+Type <nat->nat>Cases O of
+ O => [n:nat]O
+ | (S x) => [n:nat]O
+ end.
+
+Type Cases O of
+ O => [n:nat]O
+ | (S x) => [n:nat]O
+ end.
+
+
+Type <nat->nat>Cases O of
+ O => [n:nat]O
+ | (S x) => [n:nat](plus x n)
+ end.
+
+Type Cases O of
+ O => [n:nat]O
+ | (S x) => [n:nat](plus x n)
+ end.
+
+
+Type <nat>Cases O of
+ O => O
+ | ((S x) as b) => (plus b x)
+ end.
+
+Type <nat>Cases O of
+ O => O
+ | ((S (x as a)) as b) => (plus b a)
+ end.
+Type Cases O of
+ O => O
+ | ((S (x as a)) as b) => (plus b a)
+ end.
+
+
+Type Cases O of
+ O => O
+ | _ => O
+ end.
+
+Type <nat>Cases O of
+ O => O
+ | x => x
+ end.
+
+Type <nat>Cases O (S O) of
+ x y => (plus x y)
+ end.
+
+Type Cases O (S O) of
+ x y => (plus x y)
+ end.
+
+Type <nat>Cases O (S O) of
+ O y => y
+ | (S x) y => (plus x y)
+ end.
+
+Type Cases O (S O) of
+ O y => y
+ | (S x) y => (plus x y)
+ end.
+
+
+Type <nat>Cases O (S O) of
+ O x => x
+ | (S y) O => y
+ | x y => (plus x y)
+ end.
+
+
+
+
+Type Cases O (S O) of
+ O x => (plus x O)
+ | (S y) O => (plus y O)
+ | x y => (plus x y)
+ end.
+
+Type
+ <nat>Cases O (S O) of
+ O x => (plus x O)
+ | (S y) O => (plus y O)
+ | x y => (plus x y)
+ end.
+
+
+Type
+ <nat>Cases O (S O) of
+ O x => x
+ | ((S x) as b) (S y) => (plus (plus b x) y)
+ | x y => (plus x y)
+ end.
+
+
+Type Cases O (S O) of
+ O x => x
+ | ((S x) as b) (S y) => (plus (plus b x) y)
+ | x y => (plus x y)
+ end.
+
+
+Type [l:(List nat)]<(List nat)>Cases l of
+ Nil => (Nil nat)
+ | (Cons a l) => l
+ end.
+
+Type [l:(List nat)] Cases l of
+ Nil => (Nil nat)
+ | (Cons a l) => l
+ end.
+
+Type <nat>Cases (Nil nat) of
+ Nil =>O
+ | (Cons a l) => (S a)
+ end.
+Type Cases (Nil nat) of
+ Nil =>O
+ | (Cons a l) => (S a)
+ end.
+
+Type <(List nat)>Cases (Nil nat) of
+ (Cons a l) => l
+ | x => x
+ end.
+
+Type Cases (Nil nat) of
+ (Cons a l) => l
+ | x => x
+ end.
+
+Type <(List nat)>Cases (Nil nat) of
+ Nil => (Nil nat)
+ | (Cons a l) => l
+ end.
+
+Type Cases (Nil nat) of
+ Nil => (Nil nat)
+ | (Cons a l) => l
+ end.
+
+
+Type
+ <nat>Cases O of
+ O => O
+ | (S x) => <nat>Cases (Nil nat) of
+ Nil => x
+ | (Cons a l) => (plus x a)
+ end
+ end.
+
+Type
+ Cases O of
+ O => O
+ | (S x) => Cases (Nil nat) of
+ Nil => x
+ | (Cons a l) => (plus x a)
+ end
+ end.
+
+Type
+ [y:nat]Cases y of
+ O => O
+ | (S x) => Cases (Nil nat) of
+ Nil => x
+ | (Cons a l) => (plus x a)
+ end
+ end.
+
+
+Type
+ <nat>Cases O (Nil nat) of
+ O x => O
+ | (S x) Nil => x
+ | (S x) (Cons a l) => (plus x a)
+ end.
+
+
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of
+ niln => O
+ | x => O
+ end.
+
+Type [n:nat][l:(listn n)]
+ Cases l of
+ niln => O
+ | x => O
+ end.
+
+
+Type <[_:nat]nat>Cases niln of
+ niln => O
+ | x => O
+ end.
+
+Type Cases niln of
+ niln => O
+ | x => O
+ end.
+
+
+Type <[_:nat]nat>Cases niln of
+ niln => O
+ | (consn n a l) => a
+ end.
+Type Cases niln of niln => O
+ | (consn n a l) => a
+ end.
+
+
+Type <[n:nat][_:(listn n)]nat>Cases niln of
+ (consn m _ niln) => m
+ | _ => (S O) end.
+
+
+
+Type [n:nat][x:nat][l:(listn n)]<[_:nat]nat>Cases x l of
+ O niln => O
+ | y x => O
+ end.
+
+Type <[_:nat]nat>Cases O niln of
+ O niln => O
+ | y x => O
+ end.
+
+
+Type <[_:nat]nat>Cases niln O of
+ niln O => O
+ | y x => O
+ end.
+
+Type Cases niln O of
+ niln O => O
+ | y x => O
+ end.
+
+Type <[_:nat][_:nat]nat>Cases niln niln of
+ niln niln => O
+ | x y => O
+ end.
+
+Type Cases niln niln of
+ niln niln => O
+ | x y => O
+ end.
+
+Type <[_,_,_:nat]nat>Cases niln niln niln of
+ niln niln niln => O
+ | x y z => O
+ end.
+
+
+Type Cases niln niln niln of
+ niln niln niln => O
+ | x y z => O
+ end.
+
+
+
+Type <[_:nat]nat>Cases (niln) of
+ niln => O
+ | (consn n a l) => O
+ end.
+
+Type Cases (niln) of
+ niln => O
+ | (consn n a l) => O
+ end.
+
+
+Type <[_:nat][_:nat]nat>Cases niln niln of
+ niln niln => O
+ | niln (consn n a l) => n
+ | (consn n a l) x => a
+ end.
+
+
+Type Cases niln niln of
+ niln niln => O
+ | niln (consn n a l) => n
+ | (consn n a l) x => a
+ end.
+
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of
+ niln => O
+ | x => O
+ end.
+
+Type [c:nat;s:bool]
+ <[_:nat;_:bool]nat>Cases c s of
+ | O _ => O
+ | _ _ => c
+ end.
+
+Type [c:nat;s:bool]
+ <[_:nat;_:bool]nat>Cases c s of
+ | O _ => O
+ | (S _) _ => c
+ end.
+
+
+(* Rows of pattern variables: some tricky cases *)
+Axiom P:nat->Prop; f:(n:nat)(P n).
+
+Type [i:nat]
+ <[_:bool;n:nat](P n)>Cases true i of
+ | true k => (f k)
+ | _ k => (f k)
+ end.
+
+Type [i:nat]
+ <[n:nat;_:bool](P n)>Cases i true of
+ | k true => (f k)
+ | k _ => (f k)
+ end.
+
+(* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe
+ * it has to synthtize the predicate on O (which he can't)
+ *)
+Type <[n]Cases n of O => bool | (S _) => nat end>Cases O of
+ O => true
+ | (S _) => O
+ end.
+
+Type [n:nat][l:(listn n)]Cases l of
+ niln => O
+ | x => O
+ end.
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of
+ niln => O
+ | (consn n a niln) => O
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+
+Type [n:nat][l:(listn n)]Cases l of
+ niln => O
+ | (consn n a niln) => O
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of
+ niln => O
+ | (consn n a niln) => O
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+Type [n:nat][l:(listn n)]Cases l of
+ niln => O
+ | (consn n a niln) => O
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+
+Type [A:Set][n:nat][l:(Listn A n)]<[_:nat]nat>Cases l of
+ Niln => O
+ | (Consn n a Niln) => O
+ | (Consn n a (Consn m b l)) => (plus n m)
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]Cases l of
+ Niln => O
+ | (Consn n a Niln) => O
+ | (Consn n a (Consn m b l)) => (plus n m)
+ end.
+
+(*
+Type [A:Set][n:nat][l:(Listn A n)]
+ <[_:nat](Listn A O)>Cases l of
+ (Niln as b) => b
+ | (Consn n a (Niln as b))=> (Niln A)
+ | (Consn n a (Consn m b l)) => (Niln A)
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ Cases l of
+ (Niln as b) => b
+ | (Consn n a (Niln as b))=> (Niln A)
+ | (Consn n a (Consn m b l)) => (Niln A)
+ end.
+*)
+(******** This example rises an error unconstrained_variables!
+Type [A:Set][n:nat][l:(Listn A n)]
+ Cases l of
+ (Niln as b) => (Consn A O O b)
+ | ((Consn n a Niln) as L) => L
+ | (Consn n a _) => (Consn A O O (Niln A))
+ end.
+**********)
+
+(* To test tratement of as-patterns in depth *)
+Type [A:Set] [l:(List A)]
+ Cases l of
+ (Nil as b) => (Nil A)
+ | ((Cons a Nil) as L) => L
+ | ((Cons a (Cons b m)) as L) => L
+ end.
+
+
+Type [n:nat][l:(listn n)]
+ <[_:nat](listn n)>Cases l of
+ niln => l
+ | (consn n a c) => l
+ end.
+Type [n:nat][l:(listn n)]
+ Cases l of
+ niln => l
+ | (consn n a c) => l
+ end.
+
+
+Type [n:nat][l:(listn n)]
+ <[_:nat](listn n)>Cases l of
+ (niln as b) => l
+ | _ => l
+ end.
+
+
+Type [n:nat][l:(listn n)]
+ Cases l of
+ (niln as b) => l
+ | _ => l
+ end.
+
+Type [n:nat][l:(listn n)]
+ <[_:nat](listn n)>Cases l of
+ (niln as b) => l
+ | x => l
+ end.
+
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ Cases l of
+ (Niln as b) => l
+ | _ => l
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ <[_:nat](Listn A n)>Cases l of
+ Niln => l
+ | (Consn n a Niln) => l
+ | (Consn n a (Consn m b c)) => l
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ Cases l of
+ Niln => l
+ | (Consn n a Niln) => l
+ | (Consn n a (Consn m b c)) => l
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ <[_:nat](Listn A n)>Cases l of
+ (Niln as b) => l
+ | (Consn n a (Niln as b)) => l
+ | (Consn n a (Consn m b _)) => l
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ Cases l of
+ (Niln as b) => l
+ | (Consn n a (Niln as b)) => l
+ | (Consn n a (Consn m b _)) => l
+ end.
+
+
+Type <[_:nat]nat>Cases (niln) of
+ niln => O
+ | (consn n a niln) => O
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+
+Type Cases (niln) of
+ niln => O
+ | (consn n a niln) => O
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+Type <[_,_:nat]nat>Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m h) => (plus n m)
+ end.
+
+
+Type Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m h) => (plus n m)
+ end.
+
+Type [n:nat][l:(Listn nat n)]
+ <[_:nat]nat>Cases l of
+ Niln => O
+ | (Consn n a l) => O
+ end.
+
+
+Type [n:nat][l:(Listn nat n)]
+ Cases l of
+ Niln => O
+ | (Consn n a l) => O
+ end.
+
+
+Type Cases (Niln nat) of
+ Niln => O
+ | (Consn n a l) => O
+ end.
+
+Type <[_:nat]nat>Cases (LE_n O) of
+ LE_n => O
+ | (LE_S m h) => O
+ end.
+
+
+Type Cases (LE_n O) of
+ LE_n => O
+ | (LE_S m h) => O
+ end.
+
+
+
+Type Cases (LE_n O) of
+ LE_n => O
+ | (LE_S m h) => O
+ end.
+
+
+
+Type <[_:nat]nat>Cases (niln ) of
+ niln => O
+ | (consn n a niln) => n
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+Type Cases (niln ) of
+ niln => O
+ | (consn n a niln) => n
+ | (consn n a (consn m b l)) => (plus n m)
+ end.
+
+
+Type <[_:nat]nat>Cases (Niln nat) of
+ Niln => O
+ | (Consn n a Niln) => n
+ | (Consn n a (Consn m b l)) => (plus n m)
+ end.
+
+Type Cases (Niln nat) of
+ Niln => O
+ | (Consn n a Niln) => n
+ | (Consn n a (Consn m b l)) => (plus n m)
+ end.
+
+
+Type <[_,_:nat]nat>Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) => (plus n x)
+ end.
+
+
+Type Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) => (plus n x)
+ end.
+
+
+Type <[_,_:nat]nat>Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) => m
+ end.
+
+Type Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) => m
+ end.
+
+
+Type [n,m:nat][h:(Le n m)]
+ <[_,_:nat]nat>Cases h of
+ (LeO x) => x
+ | x => O
+ end.
+
+Type [n,m:nat][h:(Le n m)]
+ Cases h of
+ (LeO x) => x
+ | x => O
+ end.
+
+
+Type [n,m:nat][h:(Le n m)]
+ <[_,_:nat]nat>Cases h of
+ (LeS n m h) => n
+ | x => O
+ end.
+
+
+Type [n,m:nat][h:(Le n m)]
+ Cases h of
+ (LeS n m h) => n
+ | x => O
+ end.
+
+
+Type [n,m:nat][h:(Le n m)]
+ <[_,_:nat]nat*nat>Cases h of
+ (LeO n) => (O,n)
+ |(LeS n m _) => ((S n),(S m))
+ end.
+
+
+Type [n,m:nat][h:(Le n m)]
+ Cases h of
+ (LeO n) => (O,n)
+ |(LeS n m _) => ((S n),(S m))
+ end.
+
+
+Fixpoint F [n,m:nat; h:(Le n m)] : (Le n (S m)) :=
+ <[n,m:nat](Le n (S m))>Cases h of
+ (LeO m') => (LeO (S m'))
+ | (LeS n' m' h') => (LeS n' (S m') (F n' m' h'))
+ end.
+
+Reset F.
+
+Fixpoint F [n,m:nat; h:(Le n m)] :(Le n (S m)) :=
+ <[n,m:nat](Le n (S m))>Cases h of
+ (LeS n m h) => (LeS n (S m) (F n m h))
+ | (LeO m) => (LeO (S m))
+ end.
+
+(* Rend la longueur de la liste *)
+Definition length1:= [n:nat] [l:(listn n)]
+ <[_:nat]nat>Cases l of
+ (consn n _ (consn m _ _)) => (S (S m))
+ |(consn n _ _) => (S O)
+ | _ => O
+ end.
+
+Reset length1.
+Definition length1:= [n:nat] [l:(listn n)]
+ Cases l of
+ (consn n _ (consn m _ _)) => (S (S m))
+ |(consn n _ _) => (S O)
+ | _ => O
+ end.
+
+
+Definition length2:= [n:nat] [l:(listn n)]
+ <[_:nat]nat>Cases l of
+ (consn n _ (consn m _ _)) => (S (S m))
+ |(consn n _ _) => (S n)
+ | _ => O
+ end.
+
+Reset length2.
+
+Definition length2:= [n:nat] [l:(listn n)]
+ Cases l of
+ (consn n _ (consn m _ _)) => (S (S m))
+ |(consn n _ _) => (S n)
+ | _ => O
+ end.
+
+Definition length3 :=
+[n:nat][l:(listn n)]
+ <[_:nat]nat>Cases l of
+ (consn n _ (consn m _ l)) => (S n)
+ |(consn n _ _) => (S O)
+ | _ => O
+ end.
+
+
+Reset length3.
+
+Definition length3 :=
+[n:nat][l:(listn n)]
+ Cases l of
+ (consn n _ (consn m _ l)) => (S n)
+ |(consn n _ _) => (S O)
+ | _ => O
+ end.
+
+
+Type <[_,_:nat]nat>Cases (LeO O) of
+ (LeS n m h) =>(plus n m)
+ | x => O
+ end.
+Type Cases (LeO O) of
+ (LeS n m h) =>(plus n m)
+ | x => O
+ end.
+
+Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+ end.
+
+
+Type [n,m:nat][h:(Le n m)]Cases h of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+ end.
+
+Type <[_,_:nat]nat>Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+ end.
+
+Type Cases (LeO O) of
+ (LeO x) => x
+ | (LeS n m (LeO x)) => (plus x m)
+ | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+ end.
+
+
+Type <[_:nat]nat>Cases (LE_n O) of
+ LE_n => O
+ | (LE_S m LE_n) => (plus O m)
+ | (LE_S m (LE_S y h)) => (plus O m)
+ end.
+
+
+Type Cases (LE_n O) of
+ LE_n => O
+ | (LE_S m LE_n) => (plus O m)
+ | (LE_S m (LE_S y h)) => (plus O m)
+ end.
+
+
+Type [n,m:nat][h:(Le n m)] Cases h of
+ x => x
+ end.
+
+Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of
+ (LeO n) => n
+ | x => O
+ end.
+Type [n,m:nat][h:(Le n m)] Cases h of
+ (LeO n) => n
+ | x => O
+ end.
+
+
+Type [n:nat]<[_:nat]nat->nat>Cases niln of
+ niln => [_:nat]O
+ | (consn n a niln) => [_:nat]O
+ | (consn n a (consn m b l)) => [_:nat](plus n m)
+ end.
+
+
+Type [n:nat] Cases niln of
+ niln => [_:nat]O
+ | (consn n a niln) => [_:nat]O
+ | (consn n a (consn m b l)) => [_:nat](plus n m)
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ <[_:nat]nat->nat>Cases l of
+ Niln => [_:nat]O
+ | (Consn n a Niln) => [_:nat] n
+ | (Consn n a (Consn m b l)) => [_:nat](plus n m)
+ end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ Cases l of
+ Niln => [_:nat]O
+ | (Consn n a Niln) => [_:nat] n
+ | (Consn n a (Consn m b l)) => [_:nat](plus n m)
+ end.
+
+(* Alsos tests for multiple _ patterns *)
+Type [A:Set][n:nat][l:(Listn A n)]
+ <[n:nat](Listn A n)>Cases l of
+ (Niln as b) => b
+ | ((Consn _ _ _ ) as b)=> b
+ end.
+
+(** Horrible error message!
+
+Type [A:Set][n:nat][l:(Listn A n)]
+ Cases l of
+ (Niln as b) => b
+ | ((Consn _ _ _ ) as b)=> b
+ end.
+******)
+
+Type <[n:nat](listn n)>Cases niln of
+ (niln as b) => b
+ | ((consn _ _ _ ) as b)=> b
+ end.
+
+
+Type <[n:nat](listn n)>Cases niln of
+ (niln as b) => b
+ | x => x
+ end.
+
+Type [n,m:nat][h:(LE n m)]<[_:nat]nat->nat>Cases h of
+ LE_n => [_:nat]n
+ | (LE_S m LE_n) => [_:nat](plus n m)
+ | (LE_S m (LE_S y h)) => [_:nat](plus m y )
+ end.
+Type [n,m:nat][h:(LE n m)]Cases h of
+ LE_n => [_:nat]n
+ | (LE_S m LE_n) => [_:nat](plus n m)
+ | (LE_S m (LE_S y h)) => [_:nat](plus m y )
+ end.
+
+
+Type [n,m:nat][h:(LE n m)]
+ <[_:nat]nat>Cases h of
+ LE_n => n
+ | (LE_S m LE_n ) => (plus n m)
+ | (LE_S m (LE_S y LE_n )) => (plus (plus n m) y)
+ | (LE_S m (LE_S y (LE_S y' h))) => (plus (plus n m) (plus y y'))
+ end.
+
+
+
+Type [n,m:nat][h:(LE n m)]
+ Cases h of
+ LE_n => n
+ | (LE_S m LE_n ) => (plus n m)
+ | (LE_S m (LE_S y LE_n )) => (plus (plus n m) y)
+ | (LE_S m (LE_S y (LE_S y' h))) => (plus (plus n m) (plus y y'))
+ end.
+
+
+Type [n,m:nat][h:(LE n m)]<[_:nat]nat>Cases h of
+ LE_n => n
+ | (LE_S m LE_n) => (plus n m)
+ | (LE_S m (LE_S y h)) => (plus (plus n m) y)
+ end.
+
+
+Type [n,m:nat][h:(LE n m)]Cases h of
+ LE_n => n
+ | (LE_S m LE_n) => (plus n m)
+ | (LE_S m (LE_S y h)) => (plus (plus n m) y)
+ end.
+
+Type [n,m:nat]
+ <[_,_:nat]nat>Cases (LeO O) of
+ (LeS n m h) =>(plus n m)
+ | x => O
+ end.
+
+Type [n,m:nat]
+ Cases (LeO O) of
+ (LeS n m h) =>(plus n m)
+ | x => O
+ end.
+
+Parameter test : (n:nat){(le O n)}+{False}.
+Type [n:nat]<nat>Cases (test n) of
+ (left _) => O
+ | _ => O end.
+
+
+Type [n:nat] <nat> Cases (test n) of
+ (left _) => O
+ | _ => O end.
+
+Type [n:nat]Cases (test n) of
+ (left _) => O
+ | _ => O end.
+
+Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}.
+Type <nat>Cases (compare O O) of
+ (* k<i *) (inleft (left _)) => O
+ | (* k=i *) (inleft _) => O
+ | (* k>i *) (inright _) => O end.
+
+Type Cases (compare O O) of
+ (* k<i *) (inleft (left _)) => O
+ | (* k=i *) (inleft _) => O
+ | (* k>i *) (inright _) => O end.
+
+
+
+CoInductive SStream [A:Set] : (nat->A->Prop)->Type :=
+scons :
+ (P:nat->A->Prop)(a:A)(P O a)->(SStream A [n:nat](P (S n)))->(SStream A P).
+Parameter B : Set.
+
+Type
+ [P:nat->B->Prop][x:(SStream B P)]<[_:nat->B->Prop]B>Cases x of
+ (scons _ a _ _) => a end.
+
+
+Type
+ [P:nat->B->Prop][x:(SStream B P)] Cases x of
+ (scons _ a _ _) => a end.
+
+Type <nat*nat>Cases (O,O) of (x,y) => ((S x),(S y)) end.
+Type <nat*nat>Cases (O,O) of ((x as b), y) => ((S x),(S y)) end.
+Type <nat*nat>Cases (O,O) of (pair x y) => ((S x),(S y)) end.
+
+Type Cases (O,O) of (x,y) => ((S x),(S y)) end.
+Type Cases (O,O) of ((x as b), y) => ((S x),(S y)) end.
+Type Cases (O,O) of (pair x y) => ((S x),(S y)) end.
+
+
+
+Parameter concat : (A:Set)(List A) ->(List A) ->(List A).
+
+Type <(List nat)>Cases (Nil nat) (Nil nat) of
+ (Nil as b) x => (concat nat b x)
+ | ((Cons _ _) as d) (Nil as c) => (concat nat d c)
+ | _ _ => (Nil nat)
+ end.
+Type Cases (Nil nat) (Nil nat) of
+ (Nil as b) x => (concat nat b x)
+ | ((Cons _ _) as d) (Nil as c) => (concat nat d c)
+ | _ _ => (Nil nat)
+ end.
+
+
+Inductive redexes : Set :=
+ VAR : nat -> redexes
+ | Fun : redexes -> redexes
+ | Ap : bool -> redexes -> redexes -> redexes.
+
+Fixpoint regular [U:redexes] : Prop := <Prop>Cases U of
+ (VAR n) => True
+| (Fun V) => (regular V)
+| (Ap true ((Fun _) as V) W) => (regular V) /\ (regular W)
+| (Ap true _ W) => False
+| (Ap false V W) => (regular V) /\ (regular W)
+end.
+
+
+Type [n:nat]Cases n of O => O | (S ((S n) as V)) => V | _ => O end.
+
+Reset concat.
+Parameter concat :(n:nat) (listn n) -> (m:nat) (listn m)-> (listn (plus n m)).
+Type [n:nat][l:(listn n)][m:nat][l':(listn m)]
+ <[n,_:nat](listn (plus n m))>Cases l l' of
+ niln x => x
+ | (consn n a l'') x =>(consn (plus n m) a (concat n l'' m x))
+ end.
+
+Type [x,y,z:nat]
+ [H:x=y]
+ [H0:y=z]<[_:nat]x=z>Cases H of refl_equal =>
+ <[n:nat]x=n>Cases H0 of refl_equal => H
+ end
+ end.
+
+Type [h:False]<False>Cases h of end.
+
+Type [h:False]<True>Cases h of end.
+
+Definition is_zero := [n:nat]Cases n of O => True | _ => False end.
+
+Type [n:nat][h:O=(S n)]<[n:nat](is_zero n)>Cases h of refl_equal => I end.
+
+Definition disc : (n:nat)O=(S n)->False :=
+ [n:nat][h:O=(S n)]
+ <[n:nat](is_zero n)>Cases h of refl_equal => I end.
+
+Definition nlength3 := [n:nat] [l: (listn n)]
+ Cases l of
+ niln => O
+ | (consn O _ _) => (S O)
+ | (consn (S n) _ _) => (S (S n))
+ end.
+
+(* == Testing strategy elimintation predicate synthesis == *)
+Section titi.
+Variable h:False.
+Type Cases O of
+ O => O
+ | _ => (Except h)
+ end.
+End titi.
+
+Type Cases niln of
+ (consn _ a niln) => a
+ | (consn n _ x) => O
+ | niln => O
+ end.
+
+
+
+Inductive wsort : Set := ws : wsort | wt : wsort.
+Inductive TS : wsort->Set :=
+ id :(TS ws)
+| lift:(TS ws)->(TS ws).
+
+Type [b:wsort][M:(TS b)][N:(TS b)]
+ Cases M N of
+ (lift M1) id => False
+ | _ _ => True
+ end.
+
+
+
+(* ===================================================================== *)
+(* To test pattern matching over a non-dependent inductive type, but *)
+(* having constructors with some arguments that depend on others *)
+(* I.e. to test manipulation of elimination predicate *)
+(* ===================================================================== *)
+
+
+Parameter LTERM : nat -> Set.
+Mutual Inductive TERM : Type :=
+ var : TERM
+ | oper : (op:nat) (LTERM op) -> TERM.
+
+Parameter t1, t2:TERM.
+
+Type Cases t1 t2 of
+ var var => True
+
+ | (oper op1 l1) (oper op2 l2) => False
+ | _ _ => False
+ end.
+Reset LTERM.
+
+
+
+Require Peano_dec.
+Parameter n:nat.
+Definition eq_prf := (EXT m | n=m).
+Parameter p:eq_prf .
+
+Type Cases p of
+ (exT_intro c eqc) =>
+ Cases (eq_nat_dec c n) of
+ (right _) => (refl_equal ? n)
+ |(left y) (* c=n*) => (refl_equal ? n)
+ end
+ end.
+
+
+Parameter ordre_total : nat->nat->Prop.
+
+Parameter N_cla:(N:nat){N=O}+{N=(S O)}+{(ge N (S (S O)))}.
+
+Parameter exist_U2:(N:nat)(ge N (S (S O)))->
+ {n:nat|(m:nat)(lt O m)/\(le m N)
+ /\(ordre_total n m)
+ /\(lt O n)/\(lt n N)}.
+
+Type [N:nat](Cases (N_cla N) of
+ (inright H)=>(Cases (exist_U2 N H) of
+ (exist a b)=>a
+ end)
+ | _ => O
+ end).
+
+
+
+(* ============================================== *)
+(* To test compilation of dependent case *)
+(* Nested patterns *)
+(* ============================================== *)
+
+(* == To test that terms named with AS are correctly absolutized before
+ substitution in rhs == *)
+
+Type [n:nat]<[n:nat]nat>Cases (n) of
+ O => O
+ | (S O) => O
+ | ((S (S n1)) as N) => N
+ end.
+
+(* ========= *)
+
+Type <[n:nat][_:(listn n)]Prop>Cases niln of
+ niln => True
+ | (consn (S O) _ _) => False
+ | _ => True end.
+
+Type <[n:nat][_:(listn n)]Prop>Cases niln of
+ niln => True
+ | (consn (S (S O)) _ _) => False
+ | _ => True end.
+
+
+Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of
+ (LeO _) => O
+ | (LeS (S x) _ _) => x
+ | _ => (S O) end.
+
+Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of
+ (LeO _) => O
+ | (LeS (S x) (S y) _) => x
+ | _ => (S O) end.
+
+Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of
+ (LeO _) => O
+ | (LeS ((S x) as b) (S y) _) => b
+ | _ => (S O) end.
+
+
+
+Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
+Parameter discr_r : (n:nat) ~(O=(S n)).
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+Type
+[n:nat]
+ <[n:nat]n=O\/~n=O>Cases n of
+ O => (or_introl ? ~O=O (refl_equal ? O))
+ | (S x) => (or_intror (S x)=O ? (discr_l x))
+ end.
+
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m :=
+[m:nat]
+ <[n,m:nat] n=m \/ ~n=m>Cases n m of
+ O O => (or_introl ? ~O=O (refl_equal ? O))
+
+ | O (S x) => (or_intror O=(S x) ? (discr_r x))
+
+ | (S x) O => (or_intror ? ~(S x)=O (discr_l x))
+
+ | (S x) (S y) =>
+ <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+ (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal nat nat S x y h))
+ | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))
+ end
+ end.
+
+Reset eqdec.
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m :=
+<[n:nat] (m:nat)n=m \/ ~n=m>Cases n of
+ O => [m:nat] <[m:nat]O=m\/~O=m>Cases m of
+ O => (or_introl ? ~O=O (refl_equal nat O))
+ |(S x) => (or_intror O=(S x) ? (discr_r x))
+ end
+ | (S x) => [m:nat]
+ <[m:nat](S x)=m\/~(S x)=m>Cases m of
+ O => (or_intror (S x)=O ? (discr_l x))
+ | (S y) =>
+ <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+ (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h))
+ | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))
+ end
+ end
+ end.
+
+
+Inductive empty : (n:nat)(listn n)-> Prop :=
+ intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y))
+ end.
+
+Reset ff.
+Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
+Parameter discr_r : (n:nat) ~(O=(S n)).
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+Type
+[n:nat]
+ <[n:nat]n=O\/~n=O>Cases n of
+ O => (or_introl ? ~O=O (refl_equal ? O))
+ | (S x) => (or_intror (S x)=O ? (discr_l x))
+ end.
+
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m :=
+[m:nat]
+ <[n,m:nat] n=m \/ ~n=m>Cases n m of
+ O O => (or_introl ? ~O=O (refl_equal ? O))
+
+ | O (S x) => (or_intror O=(S x) ? (discr_r x))
+
+ | (S x) O => (or_intror ? ~(S x)=O (discr_l x))
+
+ | (S x) (S y) =>
+ <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+ (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal nat nat S x y h))
+ | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))
+ end
+ end.
+Reset eqdec.
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m :=
+<[n:nat] (m:nat)n=m \/ ~n=m>Cases n of
+ O => [m:nat] <[m:nat]O=m\/~O=m>Cases m of
+ O => (or_introl ? ~O=O (refl_equal nat O))
+ |(S x) => (or_intror O=(S x) ? (discr_r x))
+ end
+ | (S x) => [m:nat]
+ <[m:nat](S x)=m\/~(S x)=m>Cases m of
+ O => (or_intror (S x)=O ? (discr_l x))
+ | (S y) =>
+ <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+ (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h))
+ | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))
+ end
+ end
+ end.
+
+
+(* ================================================== *)
+(* Pour tester parametres *)
+(* ================================================== *)
+
+
+Inductive Empty [A:Set] : (List A)-> Prop :=
+ intro_Empty: (Empty A (Nil A)).
+
+Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)).
+
+
+Type
+ <[l:(List nat)](Empty nat l) \/ ~(Empty nat l)>Cases (Nil nat) of
+ Nil => (or_introl ? ~(Empty nat (Nil nat)) (intro_Empty nat))
+ | (Cons a y) => (or_intror (Empty nat (Cons nat a y)) ?
+ (inv_Empty nat a y))
+ end.
+
+
+(* ================================================== *)
+(* Sur les listes *)
+(* ================================================== *)
+
+
+Inductive empty : (n:nat)(listn n)-> Prop :=
+ intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type
+[n:nat] [l:(listn n)]
+ <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of
+ niln => (or_introl ? ~(empty O niln) intro_empty)
+ | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y))
+ end.
+
+(* ===================================== *)
+(* Test parametros: *)
+(* ===================================== *)
+
+Inductive eqlong : (List nat)-> (List nat)-> Prop :=
+ eql_cons : (n,m:nat)(x,y:(List nat))
+ (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y))
+| eql_nil : (eqlong (Nil nat) (Nil nat)).
+
+
+Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)).
+Parameter V2 : (a:nat)(x:(List nat))
+ (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)).
+Parameter V3 : (a:nat)(x:(List nat))
+ (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)).
+Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat))
+ (eqlong (Cons nat a x)(Cons nat b y))
+ \/ ~(eqlong (Cons nat a x) (Cons nat b y)).
+
+Type
+ <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of
+ Nil Nil => V1
+ | Nil (Cons a x) => (V2 a x)
+ | (Cons a x) Nil => (V3 a x)
+ | (Cons a x) (Cons b y) => (V4 a x b y)
+ end.
+
+
+Type
+[x,y:(List nat)]
+ <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of
+ Nil Nil => V1
+ | Nil (Cons a x) => (V2 a x)
+ | (Cons a x) Nil => (V3 a x)
+ | (Cons a x) (Cons b y) => (V4 a x b y)
+ end.
+
+
+(* ===================================== *)
+
+Inductive Eqlong : (n:nat) (listn n)-> (m:nat) (listn m)-> Prop :=
+ Eql_cons : (n,m:nat )(x:(listn n))(y:(listn m)) (a,b:nat)
+ (Eqlong n x m y)
+ ->(Eqlong (S n) (consn n a x) (S m) (consn m b y))
+| Eql_niln : (Eqlong O niln O niln).
+
+
+Parameter W1 : (Eqlong O niln O niln)\/ ~(Eqlong O niln O niln).
+Parameter W2 : (n,a:nat)(x:(listn n))
+ (Eqlong O niln (S n)(consn n a x)) \/ ~(Eqlong O niln (S n) (consn n a x)).
+Parameter W3 : (n,a:nat)(x:(listn n))
+ (Eqlong (S n) (consn n a x) O niln) \/ ~(Eqlong (S n) (consn n a x) O niln).
+Parameter W4 : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m))
+ (Eqlong (S n)(consn n a x) (S m) (consn m b y))
+ \/ ~(Eqlong (S n)(consn n a x) (S m) (consn m b y)).
+
+Type
+ <[n:nat][x:(listn n)][m:nat][y:(listn m)]
+ (Eqlong n x m y)\/~(Eqlong n x m y)>Cases niln niln of
+ niln niln => W1
+ | niln (consn n a x) => (W2 n a x)
+ | (consn n a x) niln => (W3 n a x)
+ | (consn n a x) (consn m b y) => (W4 n a x m b y)
+ end.
+
+
+Type
+[n,m:nat][x:(listn n)][y:(listn m)]
+ <[n:nat][x:(listn n)][m:nat][y:(listn m)]
+ (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of
+ niln niln => W1
+ | niln (consn n a x) => (W2 n a x)
+ | (consn n a x) niln => (W3 n a x)
+ | (consn n a x) (consn m b y) => (W4 n a x m b y)
+ end.
+
+
+Parameter Inv_r : (n,a:nat)(x:(listn n)) ~(Eqlong O niln (S n) (consn n a x)).
+Parameter Inv_l : (n,a:nat)(x:(listn n)) ~(Eqlong (S n) (consn n a x) O niln).
+Parameter Nff : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m))
+ ~(Eqlong n x m y)
+ -> ~(Eqlong (S n) (consn n a x) (S m) (consn m b y)).
+
+
+
+Fixpoint Eqlongdec [n:nat; x:(listn n)] : (m:nat)(y:(listn m))
+ (Eqlong n x m y)\/~(Eqlong n x m y)
+:= [m:nat][y:(listn m)]
+ <[n:nat][x:(listn n)][m:nat][y:(listn m)]
+ (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of
+ niln niln => (or_introl ? ~(Eqlong O niln O niln) Eql_niln)
+
+ | niln ((consn n a x) as L) =>
+ (or_intror (Eqlong O niln (S n) L) ? (Inv_r n a x))
+
+ | ((consn n a x) as L) niln =>
+ (or_intror (Eqlong (S n) L O niln) ? (Inv_l n a x))
+
+
+ | ((consn n a x) as L1) ((consn m b y) as L2) =>
+ <(Eqlong (S n) L1 (S m) L2) \/~(Eqlong (S n) L1 (S m) L2)>
+ Cases (Eqlongdec n x m y) of
+ (or_introl h) =>
+ (or_introl ? ~(Eqlong (S n) L1 (S m) L2)(Eql_cons n m x y a b h))
+ | (or_intror h) =>
+ (or_intror (Eqlong (S n) L1 (S m) L2) ? (Nff n a x m b y h))
+ end
+ end.
+
+(* ============================================== *)
+(* To test compilation of dependent case *)
+(* Multiple Patterns *)
+(* ============================================== *)
+Inductive skel: Type :=
+ PROP: skel
+ | PROD: skel->skel->skel.
+
+Parameter Can : skel -> Type.
+Parameter default_can : (s:skel) (Can s).
+
+Type [s1,s2:skel]
+[s1,s2:skel]<[s1:skel][_:skel](Can s1)>Cases s1 s2 of
+ PROP PROP => (default_can PROP)
+| (PROD x y) PROP => (default_can (PROD x y))
+| (PROD x y) _ => (default_can (PROD x y))
+| PROP _ => (default_can PROP)
+end.
+
+(* to test bindings in nested Cases *)
+(* ================================ *)
+Inductive Pair : Set :=
+ pnil : Pair |
+ pcons : Pair -> Pair -> Pair.
+
+Type [p,q:Pair]Cases p of
+ (pcons _ x) =>
+ Cases q of
+ (pcons _ (pcons _ x)) => True
+ | _ => False
+ end
+| _ => False
+end.
+
+
+Type [p,q:Pair]Cases p of
+ (pcons _ x) =>
+ Cases q of
+ (pcons _ (pcons _ x)) =>
+ Cases q of
+ (pcons _ (pcons _ (pcons _ x))) => x
+ | _ => pnil
+ end
+ | _ => pnil
+ end
+| _ => pnil
+end.
+
+Type
+ [n:nat]
+ [l:(listn (S n))]
+ <[z:nat](listn (pred z))>Cases l of
+ niln => niln
+ | (consn n _ l) =>
+ <[m:nat](listn m)>Cases l of
+ niln => niln
+ | b => b
+ end
+ end.
+
+
+
+(* Test de la syntaxe avec nombres *)
+Require Arith.
+Type [n]Cases n of (2) => true | _ => false end.
+
+Require ZArith.
+Type [n]Cases n of `0` => true | _ => false end.
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
new file mode 100644
index 00000000..0256280c
--- /dev/null
+++ b/test-suite/success/CasesDep.v
@@ -0,0 +1,405 @@
+(* Check forward dependencies *)
+
+Check [P:nat->Prop][Q][A:(P O)->Q][B:(n:nat)(P (S n))->Q][x]
+ <[_]Q>Cases x of
+ | (exist O H) => (A H)
+ | (exist (S n) H) => (B n H)
+ end.
+
+(* Check dependencies in anonymous arguments (from FTA/listn.v) *)
+
+Inductive listn [A:Set] : nat->Set :=
+ niln: (listn A O)
+| consn: (a:A)(n:nat)(listn A n)->(listn A (S n)).
+
+Section Folding.
+Variables B, C : Set.
+Variable g : B -> C -> C.
+Variable c : C.
+
+Fixpoint foldrn [n:nat; bs:(listn B n)] : C :=
+ Cases bs of niln => c
+ | (consn b _ tl) => (g b (foldrn ? tl))
+ end.
+End Folding.
+
+(* -------------------------------------------------------------------- *)
+(* Example to test patterns matching on dependent families *)
+(* This exemple extracted from the developement done by Nacira Chabane *)
+(* (equipe Paris 6) *)
+(* -------------------------------------------------------------------- *)
+
+
+Require Prelude.
+Require Logic_Type.
+
+Section Orderings.
+ Variable U: Type.
+
+ Definition Relation := U -> U -> Prop.
+
+ Variable R: Relation.
+
+ Definition Reflexive : Prop := (x: U) (R x x).
+
+ Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z).
+
+ Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x).
+
+ Definition Antisymmetric : Prop :=
+ (x,y: U) (R x y) -> (R y x) -> x==y.
+
+ Definition contains : Relation -> Relation -> Prop :=
+ [R,R': Relation] (x,y: U) (R' x y) -> (R x y).
+ Definition same_relation : Relation -> Relation -> Prop :=
+ [R,R': Relation] (contains R R') /\ (contains R' R).
+Inductive Equivalence : Prop :=
+ Build_Equivalence:
+ Reflexive -> Transitive -> Symmetric -> Equivalence.
+
+ Inductive PER : Prop :=
+ Build_PER: Symmetric -> Transitive -> PER.
+
+End Orderings.
+
+(***** Setoid *******)
+
+Inductive Setoid : Type
+ := Build_Setoid : (S:Type)(R:(Relation S))(Equivalence ? R) -> Setoid.
+
+Definition elem := [A:Setoid] let (S,R,e)=A in S.
+
+Grammar constr constr1 :=
+ elem [ "|" constr0($s) "|"] -> [ (elem $s) ].
+
+Definition equal := [A:Setoid]
+ <[s:Setoid](Relation |s|)>let (S,R,e)=A in R.
+
+Grammar constr constr1 :=
+ equal [ constr0($c) "=" "%" "S" constr0($c2) ] ->
+ [ (equal ? $c $c2) ].
+
+
+Axiom prf_equiv : (A:Setoid)(Equivalence |A| (equal A)).
+Axiom prf_refl : (A:Setoid)(Reflexive |A| (equal A)).
+Axiom prf_sym : (A:Setoid)(Symmetric |A| (equal A)).
+Axiom prf_trans : (A:Setoid)(Transitive |A| (equal A)).
+
+Section Maps.
+Variables A,B: Setoid.
+
+Definition Map_law := [f:|A| -> |B|]
+ (x,y:|A|) x =%S y -> (f x) =%S (f y).
+
+Inductive Map : Type :=
+ Build_Map : (f:|A| -> |B|)(p:(Map_law f))Map.
+
+Definition explicit_ap := [m:Map] <|A| -> |B|>Match m with
+ [f:?][p:?]f end.
+
+Axiom pres : (m:Map)(Map_law (explicit_ap m)).
+
+Definition ext := [f,g:Map]
+ (x:|A|) (explicit_ap f x) =%S (explicit_ap g x).
+
+Axiom Equiv_map_eq : (Equivalence Map ext).
+
+Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq).
+
+End Maps.
+
+Notation ap := (explicit_ap ? ?).
+
+Grammar constr constr8 :=
+ map_setoid [ constr7($c1) "=>" constr8($c2) ]
+ -> [ (Map_setoid $c1 $c2) ].
+
+
+Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)).
+
+
+(***** posint ******)
+
+Inductive posint : Type
+ := Z : posint | Suc : posint -> posint.
+
+Axiom f_equal : (A,B:Type)(f:A->B)(x,y:A) x==y -> (f x)==(f y).
+Axiom eq_Suc : (n,m:posint) n==m -> (Suc n)==(Suc m).
+
+(* The predecessor function *)
+
+Definition pred : posint->posint
+ := [n:posint](<posint>Case n of (* Z *) Z
+ (* Suc u *) [u:posint]u end).
+
+Axiom pred_Sucn : (m:posint) m==(pred (Suc m)).
+Axiom eq_add_Suc : (n,m:posint) (Suc n)==(Suc m) -> n==m.
+Axiom not_eq_Suc : (n,m:posint) ~(n==m) -> ~((Suc n)==(Suc m)).
+
+
+Definition IsSuc : posint->Prop
+ := [n:posint](<Prop>Case n of (* Z *) False
+ (* Suc p *) [p:posint]True end).
+Definition IsZero :posint->Prop :=
+ [n:posint]<Prop>Match n with
+ True
+ [p:posint][H:Prop]False end.
+
+Axiom Z_Suc : (n:posint) ~(Z==(Suc n)).
+Axiom Suc_Z: (n:posint) ~(Suc n)==Z.
+Axiom n_Sucn : (n:posint) ~(n==(Suc n)).
+Axiom Sucn_n : (n:posint) ~(Suc n)==n.
+Axiom eqT_symt : (a,b:posint) ~(a==b)->~(b==a).
+
+
+(******* Dsetoid *****)
+
+Definition Decidable :=[A:Type][R:(Relation A)]
+ (x,y:A)(R x y) \/ ~(R x y).
+
+
+Record DSetoid : Type :=
+{Set_of : Setoid;
+ prf_decid : (Decidable |Set_of| (equal Set_of))}.
+
+(* example de Dsetoide d'entiers *)
+
+
+Axiom eqT_equiv : (Equivalence posint (eqT posint)).
+Axiom Eq_posint_deci : (Decidable posint (eqT posint)).
+
+(* Dsetoide des posint*)
+
+Definition Set_of_posint := (Build_Setoid posint (eqT posint) eqT_equiv).
+
+Definition Dposint := (Build_DSetoid Set_of_posint Eq_posint_deci).
+
+
+
+(**************************************)
+
+
+(* Definition des signatures *)
+(* une signature est un ensemble d'operateurs muni
+ de l'arite de chaque operateur *)
+
+
+Section Sig.
+
+Record Signature :Type :=
+{Sigma : DSetoid;
+ Arity : (Map (Set_of Sigma) (Set_of Dposint))}.
+
+Variable S:Signature.
+
+
+
+Variable Var : DSetoid.
+
+Mutual Inductive TERM : Type :=
+ var : |(Set_of Var)| -> TERM
+ | oper : (op: |(Set_of (Sigma S))| ) (LTERM (ap (Arity S) op)) -> TERM
+with
+ LTERM : posint -> Type :=
+ nil : (LTERM Z)
+ | cons : TERM -> (n:posint)(LTERM n) -> (LTERM (Suc n)).
+
+
+
+(* -------------------------------------------------------------------- *)
+(* Examples *)
+(* -------------------------------------------------------------------- *)
+
+
+Parameter t1,t2: TERM.
+
+Type
+ Cases t1 t2 of
+ | (var v1) (var v2) => True
+ | (oper op1 l1) (oper op2 l2) => False
+ | _ _ => False
+ end.
+
+
+
+Parameter n2:posint.
+Parameter l1, l2:(LTERM n2).
+
+Type
+ Cases l1 l2 of
+ nil nil => True
+ | (cons v m y) nil => False
+ | _ _ => False
+end.
+
+
+Type Cases l1 l2 of
+ nil nil => True
+ | (cons u n x) (cons v m y) =>False
+ | _ _ => False
+end.
+
+
+
+Definition equalT [t1:TERM]:TERM->Prop :=
+[t2:TERM]
+ Cases t1 t2 of
+ (var v1) (var v2) => True
+ | (oper op1 l1) (oper op2 l2) => False
+ | _ _ => False
+ end.
+
+Definition EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+[n2:posint][l2:(LTERM n2)]
+ Cases l1 l2 of
+ nil nil => True
+ | (cons t1 n1' l1') (cons t2 n2' l2') => False
+ | _ _ => False
+end.
+
+
+Reset equalT.
+(* ------------------------------------------------------------------*)
+(* Initial exemple (without patterns) *)
+(*-------------------------------------------------------------------*)
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+<TERM->Prop>Case t1 of
+ (*var*) [v1:|(Set_of Var)|][t2:TERM]
+ <Prop>Case t2 of
+ (*var*)[v2:|(Set_of Var)|] (v1 =%S v2)
+ (*oper*)[op2:|(Set_of (Sigma S))|][_:(LTERM (ap (Arity S) op2))]False
+ end
+ (*oper*)[op1:|(Set_of (Sigma S))|]
+ [l1:(LTERM (ap (Arity S) op1))][t2:TERM]
+ <Prop>Case t2 of
+ (*var*)[v2:|(Set_of Var)|]False
+ (*oper*)[op2:|(Set_of (Sigma S))|]
+ [l2:(LTERM (ap (Arity S) op2))]
+ ((op1=%S op2)/\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2))
+ end
+end
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+<[_:posint](n2:posint)(LTERM n2)->Prop>Case l1 of
+ (*nil*) [n2:posint][l2:(LTERM n2)]
+ <[_:posint]Prop>Case l2 of
+ (*nil*)True
+ (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]False
+ end
+ (*cons*)[t1:TERM][n1':posint][l1':(LTERM n1')]
+ [n2:posint][l2:(LTERM n2)]
+ <[_:posint]Prop>Case l2 of
+ (*nil*) False
+ (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]
+ ((equalT t1 t2) /\ (EqListT n1' l1' n2' l2'))
+ end
+end.
+
+
+(* ---------------------------------------------------------------- *)
+(* Version with simple patterns *)
+(* ---------------------------------------------------------------- *)
+Reset equalT.
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+Cases t1 of
+ (var v1) => [t2:TERM]
+ Cases t2 of
+ (var v2) => (v1 =%S v2)
+ | (oper op2 _) =>False
+ end
+| (oper op1 l1) => [t2:TERM]
+ Cases t2 of
+ (var _) => False
+ | (oper op2 l2) => (op1=%S op2)
+ /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)
+ end
+end
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+<[_:posint](n2:posint)(LTERM n2)->Prop>Cases l1 of
+ nil => [n2:posint][l2:(LTERM n2)]
+ Cases l2 of
+ nil => True
+ | _ => False
+ end
+| (cons t1 n1' l1') => [n2:posint][l2:(LTERM n2)]
+ Cases l2 of
+ nil =>False
+ | (cons t2 n2' l2') => (equalT t1 t2)
+ /\ (EqListT n1' l1' n2' l2')
+ end
+end.
+
+
+Reset equalT.
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+Cases t1 of
+ (var v1) => [t2:TERM]
+ Cases t2 of
+ (var v2) => (v1 =%S v2)
+ | (oper op2 _) =>False
+ end
+| (oper op1 l1) => [t2:TERM]
+ Cases t2 of
+ (var _) => False
+ | (oper op2 l2) => (op1=%S op2)
+ /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)
+ end
+end
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+[n2:posint][l2:(LTERM n2)]
+Cases l1 of
+ nil =>
+ Cases l2 of
+ nil => True
+ | _ => False
+ end
+| (cons t1 n1' l1') => Cases l2 of
+ nil =>False
+ | (cons t2 n2' l2') => (equalT t1 t2)
+ /\ (EqListT n1' l1' n2' l2')
+ end
+end.
+
+(* ---------------------------------------------------------------- *)
+(* Version with multiple patterns *)
+(* ---------------------------------------------------------------- *)
+Reset equalT.
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+[t2:TERM]
+ Cases t1 t2 of
+ (var v1) (var v2) => (v1 =%S v2)
+
+ | (oper op1 l1) (oper op2 l2) =>
+ (op1=%S op2) /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)
+
+ | _ _ => False
+ end
+
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+[n2:posint][l2:(LTERM n2)]
+ Cases l1 l2 of
+ nil nil => True
+ | (cons t1 n1' l1') (cons t2 n2' l2') => (equalT t1 t2)
+ /\ (EqListT n1' l1' n2' l2')
+ | _ _ => False
+end.
+
+
+(* ------------------------------------------------------------------ *)
+
+End Sig.
+
+(* Exemple soumis par Bruno *)
+
+Definition bProp [b:bool] : Prop :=
+ if b then True else False.
+
+Definition f0 [F:False;ty:bool]: (bProp ty) :=
+ <[_:bool][ty:bool](bProp ty)>Cases ty ty of
+ true true => I
+ | _ false => F
+ | _ true => I
+ end.
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
new file mode 100644
index 00000000..5d183528
--- /dev/null
+++ b/test-suite/success/Check.v
@@ -0,0 +1,14 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(* Compiling the theories allows to test parsing and typing but not printing *)
+(* This file tests that pretty-printing does not fail *)
+(* Test of exact output is not specified *)
+
+Check O.
+Check S.
+Check nat.
diff --git a/test-suite/success/Conjecture.v b/test-suite/success/Conjecture.v
new file mode 100644
index 00000000..6db5859b
--- /dev/null
+++ b/test-suite/success/Conjecture.v
@@ -0,0 +1,13 @@
+(* Check keywords Conjecture and Admitted are recognized *)
+
+Conjecture c : (n:nat)n=O.
+
+Check c.
+
+Theorem d : (n:nat)n=O.
+Proof.
+ NewInduction n.
+ Reflexivity.
+ Assert H:False.
+ 2:NewDestruct H.
+Admitted.
diff --git a/test-suite/success/DHyp.v b/test-suite/success/DHyp.v
new file mode 100644
index 00000000..73907bc4
--- /dev/null
+++ b/test-suite/success/DHyp.v
@@ -0,0 +1,14 @@
+V7only [
+HintDestruct Hypothesis h1 (le ? O) 3 [Fun I -> Inversion I ].
+
+Lemma lem1 : ~(le (S O) O).
+Intro H.
+DHyp H.
+Qed.
+
+HintDestruct Conclusion h2 (le O ?) 3 [Constructor].
+
+Lemma lem2 : (le O O).
+DConcl.
+Qed.
+].
diff --git a/test-suite/success/Decompose.v b/test-suite/success/Decompose.v
new file mode 100644
index 00000000..21a3ab5d
--- /dev/null
+++ b/test-suite/success/Decompose.v
@@ -0,0 +1,7 @@
+(* This was a Decompose bug reported by Randy Pollack (29 Mar 2000) *)
+
+Goal (O=O/\((x:nat)(x=x)->(x=x)/\((y:nat)y=y->y=y)))-> True.
+Intro H.
+Decompose [and] H. (* Was failing *)
+
+Abort.
diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v
new file mode 100644
index 00000000..fdd929bb
--- /dev/null
+++ b/test-suite/success/Destruct.v
@@ -0,0 +1,13 @@
+(* Submitted by Robert Schneck *)
+
+Parameter A,B,C,D : Prop.
+Axiom X : A->B->C/\D.
+
+Lemma foo : A->B->C.
+Proof.
+Intros.
+NewDestruct X. (* Should find axiom X and should handle arguments of X *)
+Assumption.
+Assumption.
+Assumption.
+Qed.
diff --git a/test-suite/success/DiscrR.v b/test-suite/success/DiscrR.v
new file mode 100644
index 00000000..5d12098f
--- /dev/null
+++ b/test-suite/success/DiscrR.v
@@ -0,0 +1,41 @@
+Require Reals.
+Require DiscrR.
+
+Lemma ex0: ``1<>0``.
+Proof.
+ DiscrR.
+Save.
+
+Lemma ex1: ``0<>2``.
+Proof.
+ DiscrR.
+Save.
+Lemma ex2: ``4<>3``.
+Proof.
+ DiscrR.
+Save.
+
+Lemma ex3: ``3<>5``.
+Proof.
+ DiscrR.
+Save.
+
+Lemma ex4: ``-1<>0``.
+Proof.
+ DiscrR.
+Save.
+
+Lemma ex5: ``-2<>-3``.
+Proof.
+ DiscrR.
+Save.
+
+Lemma ex6: ``8<>-3``.
+Proof.
+ DiscrR.
+Save.
+
+Lemma ex7: ``-8<>3``.
+Proof.
+ DiscrR.
+Save.
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
new file mode 100644
index 00000000..39d2f4bb
--- /dev/null
+++ b/test-suite/success/Discriminate.v
@@ -0,0 +1,11 @@
+(* Check the behaviour of Discriminate *)
+
+(* Check that Discriminate tries Intro until *)
+
+Lemma l1 : O=(S O)->False.
+Discriminate 1.
+Qed.
+
+Lemma l2 : (H:O=(S O))H==H.
+Discriminate H.
+Qed.
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
new file mode 100644
index 00000000..c203b739
--- /dev/null
+++ b/test-suite/success/Field.v
@@ -0,0 +1,71 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* $Id: Field.v,v 1.1.16.1 2004/07/16 19:30:58 herbelin Exp $ *)
+
+(**** Tests of Field with real numbers ****)
+
+Require Reals.
+
+(* Example 1 *)
+Goal (eps:R)``eps*1/(2+2)+eps*1/(2+2) == eps*1/2``.
+Proof.
+ Intros.
+ Field.
+Abort.
+
+(* Example 2 *)
+Goal (f,g:(R->R); x0,x1:R)
+ ``((f x1)-(f x0))*1/(x1-x0)+((g x1)-(g x0))*1/(x1-x0) == ((f x1)+
+ (g x1)-((f x0)+(g x0)))*1/(x1-x0)``.
+Proof.
+ Intros.
+ Field.
+Abort.
+
+(* Example 3 *)
+Goal (a,b:R)``1/(a*b)*1/1/b == 1/a``.
+Proof.
+ Intros.
+ Field.
+Abort.
+
+(* Example 4 *)
+Goal (a,b:R)``a <> 0``->``b <> 0``->``1/(a*b)/1/b == 1/a``.
+Proof.
+ Intros.
+ Field.
+Abort.
+
+(* Example 5 *)
+Goal (a:R)``1 == 1*1/a*a``.
+Proof.
+ Intros.
+ Field.
+Abort.
+
+(* Example 6 *)
+Goal (a,b:R)``b == b*/a*a``.
+Proof.
+ Intros.
+ Field.
+Abort.
+
+(* Example 7 *)
+Goal (a,b:R)``b == b*1/a*a``.
+Proof.
+ Intros.
+ Field.
+Abort.
+
+(* Example 8 *)
+Goal (x,y:R)``x*((1/x)+x/(x+y)) == -(1/y)*y*(-(x*x/(x+y))-1)``.
+Proof.
+ Intros.
+ Field.
+Abort.
diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v
new file mode 100644
index 00000000..f1f7ae08
--- /dev/null
+++ b/test-suite/success/Fourier.v
@@ -0,0 +1,16 @@
+Require Rfunctions.
+Require Fourier.
+
+Lemma l1:
+ (x, y, z : R)
+ ``(Rabsolu x-z) <= (Rabsolu x-y)+(Rabsolu y-z)``.
+Intros; SplitAbsolu; Fourier.
+Qed.
+
+Lemma l2:
+ (x, y : R)
+ ``x < (Rabsolu y)`` ->
+ ``y < 1`` -> ``x >= 0`` -> ``-y <= 1`` -> ``(Rabsolu x) <= 1``.
+Intros.
+SplitAbsolu; Fourier.
+Qed.
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
new file mode 100644
index 00000000..819da259
--- /dev/null
+++ b/test-suite/success/Funind.v
@@ -0,0 +1,440 @@
+
+Definition iszero [n:nat] : bool := Cases n of
+ | O => true
+ | _ => false
+ end.
+
+Functional Scheme iszer_ind := Induction for iszero.
+
+Lemma toto : (n:nat) n = 0 -> (iszero n) = true.
+Intros x eg.
+Functional Induction iszero x; Simpl.
+Trivial.
+Subst x.
+Inversion H_eq_.
+Qed.
+
+(* We can even reuse the proof as a scheme: *)
+
+Functional Scheme toto_ind := Induction for iszero.
+
+
+
+
+
+Definition ftest [n, m:nat] : nat :=
+ Cases n of
+ | O => Cases m of
+ | O => 0
+ | _ => 1
+ end
+ | (S p) => 0
+ end.
+
+Functional Scheme ftest_ind := Induction for ftest.
+
+Lemma test1 : (n,m:nat) (le (ftest n m) 2).
+Intros n m.
+Functional Induction ftest n m;Auto.
+Save.
+
+
+Lemma test11 : (m:nat) (le (ftest 0 m) 2).
+Intros m.
+Functional Induction ftest 0 m.
+Auto.
+Auto.
+Qed.
+
+
+Definition lamfix :=
+[m:nat ]
+(Fix trivfun {trivfun [n:nat] : nat := Cases n of
+ | O => m
+ | (S p) => (trivfun p)
+ end}).
+
+(* Parameter v1 v2 : nat. *)
+
+Lemma lamfix_lem : (v1,v2:nat) (lamfix v1 v2) = v1.
+Intros v1 v2.
+Functional Induction lamfix v1 v2.
+Trivial.
+Assumption.
+Defined.
+
+
+
+(* polymorphic function *)
+Require PolyList.
+
+Functional Scheme app_ind := Induction for app.
+
+Lemma appnil : (A:Set)(l,l':(list A)) l'=(nil A) -> l = (app l l').
+Intros A l l'.
+Functional Induction app A l l';Intuition.
+Rewrite <- H1;Trivial.
+Save.
+
+
+
+
+
+Require Export Arith.
+
+
+Fixpoint trivfun [n:nat] : nat :=
+ Cases n of
+ | O => 0
+ | (S m) => (trivfun m)
+ end.
+
+
+(* essaie de parametre variables non locaux:*)
+
+Parameter varessai : nat.
+
+Lemma first_try : (trivfun varessai) = 0.
+Functional Induction trivfun varessai.
+Trivial.
+Simpl.
+Assumption.
+Defined.
+
+
+Functional Scheme triv_ind := Induction for trivfun.
+
+Lemma bisrepetita : (n':nat) (trivfun n') = 0.
+Intros n'.
+Functional Induction trivfun n'.
+Trivial.
+Simpl .
+Assumption.
+Qed.
+
+
+
+
+
+
+
+Fixpoint iseven [n:nat] : bool :=
+ Cases n of
+ | O => true
+ | (S (S m)) => (iseven m)
+ | _ => false
+ end.
+
+Fixpoint funex [n:nat] : nat :=
+ Cases (iseven n) of
+ | true => n
+ | false => Cases n of
+ | O => 0
+ | (S r) => (funex r)
+ end
+ end.
+
+Fixpoint nat_equal_bool [n:nat] : nat -> bool :=
+[m:nat]
+ Cases n of
+ | O => Cases m of
+ | O => true
+ | _ => false
+ end
+ | (S p) => Cases m of
+ | O => false
+ | (S q) => (nat_equal_bool p q)
+ end
+ end.
+
+
+Require Export Div2.
+
+Lemma div2_inf : (n:nat) (le (div2 n) n).
+Intros n.
+Functional Induction div2 n.
+Auto.
+Auto.
+
+Apply le_S.
+Apply le_n_S.
+Exact H.
+Qed.
+
+(* reuse this lemma as a scheme:*)
+
+Functional Scheme div2_ind := Induction for div2_inf.
+
+Fixpoint nested_lam [n:nat] : nat -> nat :=
+ Cases n of
+ | O => [m:nat ] 0
+ | (S n') => [m:nat ] (plus m (nested_lam n' m))
+ end.
+
+Functional Scheme nested_lam_ind := Induction for nested_lam.
+
+Lemma nest : (n, m:nat) (nested_lam n m) = (mult n m).
+Intros n m.
+Functional Induction nested_lam n m; Auto.
+Qed.
+
+Lemma nest2 : (n, m:nat) (nested_lam n m) = (mult n m).
+Intros n m. Pattern n m .
+Apply nested_lam_ind; Simpl ; Intros; Auto.
+Qed.
+
+
+Fixpoint essai [x : nat] : nat * nat -> nat :=
+ [p : nat * nat] ( Case p of [n, m : ?] Cases n of
+ O => O
+ | (S q) =>
+ Cases x of
+ O => (S O)
+ | (S r) => (S (essai r (q, m)))
+ end
+ end end ).
+
+Lemma essai_essai:
+ (x : nat)
+ (p : nat * nat) ( Case p of [n, m : ?] (lt O n) -> (lt O (essai x p)) end ).
+Intros x p.
+(Functional Induction essai x p); Intros.
+Inversion H.
+Simpl; Try Abstract ( Auto with arith ).
+Simpl; Try Abstract ( Auto with arith ).
+Qed.
+
+
+Fixpoint plus_x_not_five'' [n : nat] : nat -> nat :=
+ [m : nat] let x = (nat_equal_bool m (S (S (S (S (S O)))))) in
+ let y = O in
+ Cases n of
+ O => y
+ | (S q) =>
+ let recapp = (plus_x_not_five'' q m) in
+ Cases x of true => (S recapp) | false => (S recapp) end
+ end.
+
+Lemma notplusfive'':
+ (x, y : nat) y = (S (S (S (S (S O))))) -> (plus_x_not_five'' x y) = x.
+Intros a b.
+Unfold plus_x_not_five''.
+(Functional Induction plus_x_not_five'' a b); Intros hyp; Simpl; Auto.
+Qed.
+
+Lemma iseq_eq: (n, m : nat) n = m -> (nat_equal_bool n m) = true.
+Intros n m.
+Unfold nat_equal_bool.
+(Functional Induction nat_equal_bool n m); Simpl; Intros hyp; Auto.
+Inversion hyp.
+Inversion hyp.
+Qed.
+
+Lemma iseq_eq': (n, m : nat) (nat_equal_bool n m) = true -> n = m.
+Intros n m.
+Unfold nat_equal_bool.
+(Functional Induction nat_equal_bool n m); Simpl; Intros eg; Auto.
+Inversion eg.
+Inversion eg.
+Qed.
+
+
+Inductive istrue : bool -> Prop :=
+ istrue0: (istrue true) .
+
+Lemma inf_x_plusxy': (x, y : nat) (le x (plus x y)).
+Intros n m.
+(Functional Induction plus n m); Intros.
+Auto with arith.
+Auto with arith.
+Qed.
+
+
+Lemma inf_x_plusxy'': (x : nat) (le x (plus x O)).
+Intros n.
+Unfold plus.
+(Functional Induction plus n O); Intros.
+Auto with arith.
+Apply le_n_S.
+Assumption.
+Qed.
+
+Lemma inf_x_plusxy''': (x : nat) (le x (plus O x)).
+Intros n.
+(Functional Induction plus O n); Intros;Auto with arith.
+Qed.
+
+Fixpoint mod2 [n : nat] : nat :=
+ Cases n of O => O
+ | (S (S m)) => (S (mod2 m))
+ | _ => O end.
+
+Lemma princ_mod2: (n : nat) (le (mod2 n) n).
+Intros n.
+(Functional Induction mod2 n); Simpl; Auto with arith.
+Qed.
+
+Definition isfour : nat -> bool :=
+ [n : nat] Cases n of (S (S (S (S O)))) => true | _ => false end.
+
+Definition isononeorfour : nat -> bool :=
+ [n : nat] Cases n of (S O) => true
+ | (S (S (S (S O)))) => true
+ | _ => false end.
+
+Lemma toto'': (n : nat) (istrue (isfour n)) -> (istrue (isononeorfour n)).
+Intros n.
+(Functional Induction isononeorfour n); Intros istr; Simpl; Inversion istr.
+Apply istrue0.
+Qed.
+
+Lemma toto': (n, m : nat) n = (S (S (S (S O)))) -> (istrue (isononeorfour n)).
+Intros n.
+(Functional Induction isononeorfour n); Intros m istr; Inversion istr.
+Apply istrue0.
+Qed.
+
+Definition ftest4 : nat -> nat -> nat :=
+ [n, m : nat] Cases n of
+ O =>
+ Cases m of O => O | (S q) => (S O) end
+ | (S p) =>
+ Cases m of O => O | (S r) => (S O) end
+ end.
+
+Lemma test4: (n, m : nat) (le (ftest n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest n m); Auto with arith.
+Qed.
+
+Lemma test4': (n, m : nat) (le (ftest4 (S n) m) (S (S O))).
+Intros n m.
+(Functional Induction ftest4 (S n) m).
+Auto with arith.
+Auto with arith.
+Qed.
+
+Definition ftest44 : nat * nat -> nat -> nat -> nat :=
+ [x : nat * nat]
+ [n, m : nat]
+ ( Case x of [p, q : ?] Cases n of
+ O =>
+ Cases m of O => O | (S q) => (S O) end
+ | (S p) =>
+ Cases m of O => O | (S r) => (S O) end
+ end end ).
+
+Lemma test44:
+ (pq : nat * nat) (n, m, o, r, s : nat) (le (ftest44 pq n (S m)) (S (S O))).
+Intros pq n m o r s.
+(Functional Induction ftest44 pq n (S m)).
+Auto with arith.
+Auto with arith.
+Auto with arith.
+Auto with arith.
+Qed.
+
+Fixpoint ftest2 [n : nat] : nat -> nat :=
+ [m : nat] Cases n of
+ O =>
+ Cases m of O => O | (S q) => O end
+ | (S p) => (ftest2 p m)
+ end.
+
+Lemma test2: (n, m : nat) (le (ftest2 n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest2 n m) ; Simpl; Intros; Auto.
+Qed.
+
+Fixpoint ftest3 [n : nat] : nat -> nat :=
+ [m : nat] Cases n of
+ O => O
+ | (S p) =>
+ Cases m of O => (ftest3 p O) | (S r) => O end
+ end.
+
+Lemma test3: (n, m : nat) (le (ftest3 n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest3 n m).
+Intros.
+Auto.
+Intros.
+Auto.
+Intros.
+Simpl.
+Auto.
+Qed.
+
+Fixpoint ftest5 [n : nat] : nat -> nat :=
+ [m : nat] Cases n of
+ O => O
+ | (S p) =>
+ Cases m of O => (ftest5 p O) | (S r) => (ftest5 p r) end
+ end.
+
+Lemma test5: (n, m : nat) (le (ftest5 n m) (S (S O))).
+Intros n m.
+(Functional Induction ftest5 n m).
+Intros.
+Auto.
+Intros.
+Auto.
+Intros.
+Simpl.
+Auto.
+Qed.
+
+Definition ftest7 : (n : nat) nat :=
+ [n : nat] Cases (ftest5 n O) of O => O | (S r) => O end.
+
+Lemma essai7:
+ (Hrec : (n : nat) (ftest5 n O) = O -> (le (ftest7 n) (S (S O))))
+ (Hrec0 : (n, r : nat) (ftest5 n O) = (S r) -> (le (ftest7 n) (S (S O))))
+ (n : nat) (le (ftest7 n) (S (S O))).
+Intros hyp1 hyp2 n.
+Unfold ftest7.
+(Functional Induction ftest7 n); Auto.
+Qed.
+
+Fixpoint ftest6 [n : nat] : nat -> nat :=
+ [m : nat]
+ Cases n of
+ O => O
+ | (S p) =>
+ Cases (ftest5 p O) of O => (ftest6 p O) | (S r) => (ftest6 p r) end
+ end.
+
+
+Lemma princ6:
+ ((n, m : nat) n = O -> (le (ftest6 O m) (S (S O)))) ->
+ ((n, m, p : nat)
+ (le (ftest6 p O) (S (S O))) ->
+ (ftest5 p O) = O -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) ->
+ ((n, m, p, r : nat)
+ (le (ftest6 p r) (S (S O))) ->
+ (ftest5 p O) = (S r) -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) ->
+ (x, y : nat) (le (ftest6 x y) (S (S O))).
+Intros hyp1 hyp2 hyp3 n m.
+Generalize hyp1 hyp2 hyp3.
+Clear hyp1 hyp2 hyp3.
+(Functional Induction ftest6 n m);Auto.
+Qed.
+
+Lemma essai6: (n, m : nat) (le (ftest6 n m) (S (S O))).
+Intros n m.
+Unfold ftest6.
+(Functional Induction ftest6 n m); Simpl; Auto.
+Qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test-suite/success/Generalize.v b/test-suite/success/Generalize.v
new file mode 100644
index 00000000..0dc73991
--- /dev/null
+++ b/test-suite/success/Generalize.v
@@ -0,0 +1,7 @@
+(* Check Generalize Dependent *)
+
+Lemma l1 : [a:=O;b:=a](c:b=b;d:(True->b=b))d=d.
+Intros.
+Generalize Dependent a.
+Intros a b c d.
+Abort.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
new file mode 100644
index 00000000..f32753e0
--- /dev/null
+++ b/test-suite/success/Hints.v
@@ -0,0 +1,48 @@
+(* Checks syntax of Hints commands *)
+(* Checks that qualified names are accepted *)
+
+(* New-style syntax *)
+Hint h1 : core arith := Resolve Logic.refl_equal.
+Hint h2 := Immediate Logic.trans_equal.
+Hint h3 : core := Unfold Logic.sym_equal.
+Hint h4 : foo bar := Constructors Logic.eq.
+Hint h5 : foo bar := Extern 3 (eq ? ? ?) Apply Logic.refl_equal.
+
+(* Old-style syntax *)
+Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal.
+Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo.
+Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal.
+Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo.
+Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal.
+Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal : foo.
+
+(* What's this stranged syntax ? *)
+HintDestruct Conclusion h6 (le ? ?) 4 [ Fun H -> Apply H ].
+HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ Fun H -> Apply H ].
+HintDestruct Hypothesis h8 (le ? ?) 4 [ Fun H -> Apply H ].
+
+(* Checks that local names are accepted *)
+Section A.
+ Remark Refl : (A:Set)(x:A)x=x.
+ Proof refl_equal.
+ Definition Sym := sym_equal.
+ Local Trans := trans_equal.
+
+ Hint h1 : foo := Resolve Refl.
+ Hint h2 : bar := Resolve Sym.
+ Hint h3 : foo2 := Resolve Trans.
+
+ Hint h2 := Immediate Refl.
+ Hint h2 := Immediate Sym.
+ Hint h2 := Immediate Trans.
+
+ Hint h3 := Unfold Refl.
+ Hint h3 := Unfold Sym.
+ Hint h3 := Unfold Trans.
+
+ Hints Resolve Sym Trans Refl.
+ Hints Immediate Sym Trans Refl.
+ Hints Unfold Sym Trans Refl.
+
+End A.
+
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
new file mode 100644
index 00000000..87431a75
--- /dev/null
+++ b/test-suite/success/Inductive.v
@@ -0,0 +1,34 @@
+(* Check local definitions in context of inductive types *)
+Inductive A [C,D:Prop; E:=C; F:=D; x,y:E->F] : E -> Set :=
+ I : (z:E)(A C D x y z).
+
+Check
+ [C,D:Prop; E:=C; F:=D; x,y:(E ->F);
+ P:((c:C)(A C D x y c) ->Type);
+ f:((z:C)(P z (I C D x y z)));
+ y0:C; a:(A C D x y y0)]
+ <[y1:C; a0:(A C D x y y1)](P y1 a0)>Cases a of (I x0) => (f x0) end.
+
+Record B [C,D:Set; E:=C; F:=D; x,y:E->F] : Set := { p : C; q : E }.
+
+Check
+ [C,D:Set; E:=C; F:=D; x,y:(E ->F);
+ P:((B C D x y) ->Type);
+ f:((p0,q0:C)(P (Build_B C D x y p0 q0)));
+ b:(B C D x y)]
+ <[b0:(B C D x y)](P b0)>Cases b of (Build_B x0 x1) => (f x0 x1) end.
+
+(* Check implicit parameters of inductive types (submitted by Pierre
+ Casteran and also implicit in #338) *)
+
+Set Implicit Arguments.
+
+CoInductive LList [A:Set] : Set :=
+ | LNil : (LList A)
+ | LCons : A -> (LList A) -> (LList A).
+
+Implicits LNil [1].
+
+Inductive Finite [A:Set] : (LList A) -> Prop :=
+ | Finite_LNil : (Finite LNil)
+ | Finite_LCons : (a:A) (l:(LList A)) (Finite l) -> (Finite (LCons a l)).
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
new file mode 100644
index 00000000..fd80cec6
--- /dev/null
+++ b/test-suite/success/Injection.v
@@ -0,0 +1,34 @@
+(* Check the behaviour of Injection *)
+
+(* Check that Injection tries Intro until *)
+
+Lemma l1 : (x:nat)(S x)=(S (S x))->False.
+Injection 1.
+Apply n_Sn.
+Qed.
+
+Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False.
+Injection H.
+Intros.
+Apply (n_Sn x H0).
+Qed.
+
+(* Check that no tuple needs to be built *)
+Lemma l3 : (x,y:nat)
+ (existS ? [n:nat]({n=n}+{n=n}) x (left ? ? (refl_equal nat x)))=
+ (existS ? [n:nat]({n=n}+{n=n}) y (left ? ? (refl_equal nat y)))
+ -> x=y.
+Intros x y H.
+Injection H.
+Exact [H]H.
+Qed.
+
+(* Check that a tuple is built (actually the same as the initial one) *)
+Lemma l4 : (p1,p2:{O=O}+{O=O})
+ (existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2)
+ ->(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2).
+Intros.
+Injection H.
+Exact [H]H.
+Qed.
+
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
new file mode 100644
index 00000000..a9e4a843
--- /dev/null
+++ b/test-suite/success/Inversion.v
@@ -0,0 +1,85 @@
+Axiom magic:False.
+
+(* Submitted by Dachuan Yu (bug #220) *)
+Fixpoint T[n:nat] : Type :=
+ Cases n of
+ | O => (nat -> Prop)
+ | (S n') => (T n')
+ end.
+Inductive R : (n:nat)(T n) -> nat -> Prop :=
+ | RO : (Psi:(T O); l:nat)
+ (Psi l) -> (R O Psi l)
+ | RS : (n:nat; Psi:(T (S n)); l:nat)
+ (R n Psi l) -> (R (S n) Psi l).
+Definition Psi00 : (nat -> Prop) := [n:nat] False.
+Definition Psi0 : (T O) := Psi00.
+Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l).
+Inversion 1.
+Abort.
+
+(* Submitted by Pierre Casteran (bug #540) *)
+
+Set Implicit Arguments.
+Parameter rule: Set -> Type.
+
+Inductive extension [I:Set]:Type :=
+ NL : (extension I)
+|add_rule : (rule I) -> (extension I) -> (extension I).
+
+
+Inductive in_extension [I :Set;r: (rule I)] : (extension I) -> Type :=
+ in_first : (e:?)(in_extension r (add_rule r e))
+|in_rest : (e,r':?)(in_extension r e) -> (in_extension r (add_rule r' e)).
+
+Implicits NL [1].
+
+Inductive super_extension [I:Set;e :(extension I)] : (extension I) -> Type :=
+ super_NL : (super_extension e NL)
+| super_add : (r:?)(e': (extension I))
+ (in_extension r e) ->
+ (super_extension e e') ->
+ (super_extension e (add_rule r e')).
+
+
+
+Lemma super_def : (I :Set)(e1, e2: (extension I))
+ (super_extension e2 e1) ->
+ (ru:?)
+ (in_extension ru e1) ->
+ (in_extension ru e2).
+Proof.
+ Induction 1.
+ Inversion 1; Auto.
+ Elim magic.
+Qed.
+
+(* Example from Norbert Schirmer on Coq-Club, Sep 2000 *)
+
+Unset Implicit Arguments.
+Definition Q[n,m:nat;prf:(le n m)]:=True.
+Goal (n,m:nat;H:(le (S n) m))(Q (S n) m H)==True.
+Intros.
+Dependent Inversion_clear H.
+Elim magic.
+Elim magic.
+Qed.
+
+(* Submitted by Boris Yakobowski (bug #529) *)
+(* Check that Inversion does not fail due to unnormalized evars *)
+
+Set Implicit Arguments.
+Require Import Bvector.
+
+Inductive I : nat -> Set :=
+| C1 : (I (S O))
+| C2 : (k,i:nat)(vector (I i) k) -> (I i).
+
+Inductive SI : (k:nat)(I k) -> (vector nat k) -> nat -> Prop :=
+| SC2 : (k,i,vf:nat) (v:(vector (I i) k))(xi:(vector nat i))(SI (C2 v) xi vf).
+
+Theorem SUnique : (k:nat)(f:(I k))(c:(vector nat k))
+(v,v':?) (SI f c v) -> (SI f c v') -> v=v'.
+Proof.
+NewInduction 1.
+Intros H ; Inversion H.
+Admitted.
diff --git a/test-suite/success/LetIn.v b/test-suite/success/LetIn.v
new file mode 100644
index 00000000..0e0b4435
--- /dev/null
+++ b/test-suite/success/LetIn.v
@@ -0,0 +1,11 @@
+(* Simple let-in's *)
+Definition l1 := [P := O]P.
+Definition l2 := [P := nat]P.
+Definition l3 := [P := True]P.
+Definition l4 := [P := Prop]P.
+Definition l5 := [P := Type]P.
+
+(* Check casting of let-in *)
+Definition l6 := [P := O : nat]P.
+Definition l7 := [P := True : Prop]P.
+Definition l8 := [P := True : Type]P.
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
new file mode 100644
index 00000000..d89ee3be
--- /dev/null
+++ b/test-suite/success/MatchFail.v
@@ -0,0 +1,28 @@
+Require Export ZArith.
+Require Export ZArithRing.
+
+(* Cette tactique a pour objectif de remplacer toute instance
+ de (POS (xI e)) ou de (POS (xO e)) par
+ 2*(POS e)+1 ou 2*(POS e), pour rendre les expressions plus
+ à même d'être utilisées par Ring, lorsque ces expressions contiennent
+ des variables de type positive. *)
+Tactic Definition compute_POS :=
+ (Match Context With
+ | [|- [(POS (xI ?1))]] -> Let v = ?1 In
+ (Match v With
+ | [xH] ->
+ (Fail 1)
+ |_->
+ Rewrite (POS_xI v))
+ | [ |- [(POS (xO ?1))]] -> Let v = ?1 In
+ Match v With
+ |[xH]->
+ (Fail 1)
+ |[?]->
+ Rewrite (POS_xO v)).
+
+Goal (x:positive)(POS (xI (xI x)))=`4*(POS x)+3`.
+Intros.
+Repeat compute_POS.
+Ring.
+Qed.
diff --git a/test-suite/success/Mod_ltac.v b/test-suite/success/Mod_ltac.v
new file mode 100644
index 00000000..1a9f6fc5
--- /dev/null
+++ b/test-suite/success/Mod_ltac.v
@@ -0,0 +1,20 @@
+(* Submitted by Houda Anoun *)
+
+Module toto.
+Tactic Definition titi:=Auto.
+End toto.
+
+Module ti.
+Import toto.
+Tactic Definition equal:=
+Match Context With
+[ |- ?1=?1]-> titi
+| [ |- ?]-> Idtac.
+
+End ti.
+
+Import ti.
+Definition simple:(a:nat) a=a.
+Intro.
+equal.
+Qed.
diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v
new file mode 100644
index 00000000..098de3cf
--- /dev/null
+++ b/test-suite/success/Mod_params.v
@@ -0,0 +1,78 @@
+(* Syntax test - all possible kinds of module parameters *)
+
+Module Type SIG.
+End SIG.
+
+Module Type FSIG[X:SIG].
+End FSIG.
+
+Module F[X:SIG].
+End F.
+
+Module Q.
+End Q.
+
+(*
+#trace Nametab.push;;
+#trace Nametab.push_short_name;;
+#trace Nametab.freeze;;
+#trace Nametab.unfreeze;;
+#trace Nametab.exists_cci;;
+*)
+
+Module M.
+Reset M.
+Module M[X:SIG].
+Reset M.
+Module M[X,Y:SIG].
+Reset M.
+Module M[X:SIG;Y:SIG].
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG].
+Reset M.
+Module M[X:SIG][Y:SIG].
+Reset M.
+Module M[X,Y:SIG][Z1,Z:SIG].
+Reset M.
+Module M:SIG.
+Reset M.
+Module M[X:SIG]:SIG.
+Reset M.
+Module M[X,Y:SIG]:SIG.
+Reset M.
+Module M[X:SIG;Y:SIG]:SIG.
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG]:SIG.
+Reset M.
+Module M[X:SIG][Y:SIG]:SIG.
+Reset M.
+Module M[X,Y:SIG][Z1,Z:SIG]:SIG.
+Reset M.
+Module M:=(F Q).
+Reset M.
+Module M[X:FSIG]:=(X Q).
+Reset M.
+Module M[X,Y:FSIG]:=(X Q).
+Reset M.
+Module M[X:FSIG;Y:SIG]:=(X Y).
+Reset M.
+Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z).
+Reset M.
+Module M[X:FSIG][Y:SIG]:=(X Y).
+Reset M.
+Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z).
+Reset M.
+Module M:SIG:=(F Q).
+Reset M.
+Module M[X:FSIG]:SIG:=(X Q).
+Reset M.
+Module M[X,Y:FSIG]:SIG:=(X Q).
+Reset M.
+Module M[X:FSIG;Y:SIG]:SIG:=(X Y).
+Reset M.
+Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z).
+Reset M.
+Module M[X:FSIG][Y:SIG]:SIG:=(X Y).
+Reset M.
+Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z).
+Reset M.
diff --git a/test-suite/success/Mod_strengthen.v b/test-suite/success/Mod_strengthen.v
new file mode 100644
index 00000000..a472e698
--- /dev/null
+++ b/test-suite/success/Mod_strengthen.v
@@ -0,0 +1,64 @@
+Module Type Sub.
+ Axiom Refl1 : (x:nat)(x=x).
+ Axiom Refl2 : (x:nat)(x=x).
+ Axiom Refl3 : (x:nat)(x=x).
+ Inductive T : Set := A : T.
+End Sub.
+
+Module Type Main.
+ Declare Module M:Sub.
+End Main.
+
+
+Module A <: Main.
+ Module M <: Sub.
+ Lemma Refl1 : (x:nat) x=x.
+ Intros;Reflexivity.
+ Qed.
+ Axiom Refl2 : (x:nat) x=x.
+ Lemma Refl3 : (x:nat) x=x.
+ Intros;Reflexivity.
+ Defined.
+ Inductive T : Set := A : T.
+ End M.
+End A.
+
+
+
+(* first test *)
+
+Module F[S:Sub].
+ Module M:=S.
+End F.
+
+Module B <: Main with Module M:=A.M := F A.M.
+
+
+
+(* second test *)
+
+Lemma r1 : (A.M.Refl1 == B.M.Refl1).
+Proof.
+ Reflexivity.
+Qed.
+
+Lemma r2 : (A.M.Refl2 == B.M.Refl2).
+Proof.
+ Reflexivity.
+Qed.
+
+Lemma r3 : (A.M.Refl3 == B.M.Refl3).
+Proof.
+ Reflexivity.
+Qed.
+
+Lemma t : (A.M.T == B.M.T).
+Proof.
+ Reflexivity.
+Qed.
+
+Lemma a : (A.M.A == B.M.A).
+Proof.
+ Reflexivity.
+Qed.
+
diff --git a/test-suite/success/NatRing.v b/test-suite/success/NatRing.v
new file mode 100644
index 00000000..6a1eeccc
--- /dev/null
+++ b/test-suite/success/NatRing.v
@@ -0,0 +1,10 @@
+Require ArithRing.
+
+Lemma l1 : (S (S O))=(plus (S O) (S O)).
+NatRing.
+Qed.
+
+Lemma l2 : (x:nat)(S (S x))=(plus (S O) (S x)).
+Intro.
+NatRing.
+Qed. \ No newline at end of file
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
new file mode 100644
index 00000000..c324919f
--- /dev/null
+++ b/test-suite/success/Omega.v
@@ -0,0 +1,89 @@
+
+Require Omega.
+
+(* Submitted by Xavier Urbain 18 Jan 2002 *)
+
+Lemma lem1 : (x,y:Z)
+ `-5 < x < 5` ->
+ `-5 < y` ->
+ `-5 < x+y+5`.
+Proof.
+Intros x y.
+Omega.
+Qed.
+
+(* Proposed by Pierre Crégut *)
+
+Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`.
+Intro.
+Omega.
+Qed.
+
+(* Proposed by Jean-Christophe Filliâtre *)
+
+Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`.
+Proof.
+Intros.
+Omega.
+Qed.
+
+(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
+(* internal variable and a section variable (June 2001) *)
+
+Section A.
+Variable x,y : Z.
+Hypothesis H : `x > y`.
+Lemma lem4 : `x > y`.
+Omega.
+Qed.
+End A.
+
+(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
+(* May 2002 *)
+
+Section B.
+Variables R1,R2,S1,S2,H,S:Z.
+Hypothesis I:`R1 < 0`->`R2 = R1+(2*S1-1)`.
+Hypothesis J:`R1 < 0`->`S2 = S1-1`.
+Hypothesis K:`R1 >= 0`->`R2 = R1`.
+Hypothesis L:`R1 >= 0`->`S2 = S1`.
+Hypothesis M:`H <= 2*S`.
+Hypothesis N:`S < H`.
+Lemma lem5 : `H > 0`.
+Omega.
+Qed.
+End B.
+
+(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+Lemma lem6: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`.
+Intros.
+Omega.
+Qed.
+
+(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
+Require Omega.
+Section C.
+Parameter g:(m:nat)~m=O->Prop.
+Parameter f:(m:nat)(H:~m=O)(g m H).
+Variable n:nat.
+Variable ap_n:~n=O.
+Local delta:=(f n ap_n).
+Lemma lem7 : n=n.
+Omega.
+Qed.
+End C.
+
+(* Problem of dependencies *)
+Require Omega.
+Lemma lem8 : (H:O=O->O=O) H=H -> O=O.
+Intros; Omega.
+Qed.
+
+(* Bug that what caused by the use of intro_using in Omega *)
+Require Omega.
+Lemma lem9 : (p,q:nat)
+ ~((le p q)/\(lt p q)\/(le q p)/\(lt p q))
+ -> (lt p p)\/(le p p).
+Intros; Omega.
+Qed.
+
diff --git a/test-suite/success/PPFix.v8 b/test-suite/success/PPFix.v8
new file mode 100644
index 00000000..1ecbae3a
--- /dev/null
+++ b/test-suite/success/PPFix.v8
@@ -0,0 +1,8 @@
+
+(* To test PP of fixpoints *)
+Require Import Arith.
+Check fix a(n: nat): n<5 -> nat :=
+ match n return n<5 -> nat with
+ | 0 => fun _ => 0
+ | S n => fun h => S (a n (lt_S_n _ _ (lt_S _ _ h)))
+ end.
diff --git a/test-suite/success/Print.v b/test-suite/success/Print.v
new file mode 100644
index 00000000..4554a843
--- /dev/null
+++ b/test-suite/success/Print.v
@@ -0,0 +1,20 @@
+Print Tables.
+Print ML Path.
+Print ML Modules.
+Print LoadPath.
+Print Graph.
+Print Coercions.
+Print Classes.
+Print nat.
+Print Proof O.
+Print All.
+Print Grammar constr constr.
+Inspect 10.
+
+Section A.
+Coercion f := [x]True : nat -> Prop.
+Print Coercion Paths nat SORTCLASS.
+
+Print Section A.
+Print.
+
diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v
new file mode 100644
index 00000000..7f5cd800
--- /dev/null
+++ b/test-suite/success/Projection.v
@@ -0,0 +1,45 @@
+Structure S : Type :=
+ {Dom : Type;
+ Op : Dom -> Dom -> Dom}.
+
+Check [s:S](Dom s).
+Check [s:S](Op s).
+Check [s:S;a,b:(Dom s)](Op s a b).
+
+(* v8
+Check fun s:S => s.(Dom).
+Check fun s:S => s.(Op).
+Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b.
+*)
+
+Set Implicit Arguments.
+Unset Strict Implicits.
+
+Structure S' [A:Set] : Type :=
+ {Dom' : Type;
+ Op' : A -> Dom' -> Dom'}.
+
+Check [s:(S' nat)](Dom' s).
+Check [s:(S' nat)](Op' 2!s).
+Check [s:(S' nat)](!Op' nat s).
+Check [s:(S' nat);a:nat;b:(Dom' s)](Op' a b).
+Check [s:(S' nat);a:nat;b:(Dom' s)](!Op' nat s a b).
+
+(* v8
+Check fun s:S' => s.(Dom').
+Check fun s:S' => s.(Op').
+Check fun (s:S') (a b:s.(Dom')) => _.(Op') a b.
+Check fun (s:S') (a b:s.(Dom')) => s.(Op') a b.
+
+Set Implicit Arguments.
+Unset Strict Implicits.
+
+Structure S' (A:Set) : Type :=
+ {Dom' : Type;
+ Op' : A -> Dom' -> Dom'}.
+
+Check fun s:S' nat => s.(Dom').
+Check fun s:S' nat => s.(Op').
+Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => _.(@Op' nat) a b.
+Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => s.(Op') a b.
+*)
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
new file mode 100644
index 00000000..f3a13634
--- /dev/null
+++ b/test-suite/success/Record.v
@@ -0,0 +1,3 @@
+(* Nijmegen expects redefinition of sorts *)
+Definition CProp := Prop.
+Record test : CProp := { n:nat }.
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v
new file mode 100644
index 00000000..eaa0690c
--- /dev/null
+++ b/test-suite/success/Reg.v
@@ -0,0 +1,136 @@
+Require Reals.
+
+Axiom y : R->R.
+Axiom d_y : (derivable y).
+Axiom n_y : (x:R)``(y x)<>0``.
+Axiom dy_0 : (derive_pt y R0 (d_y R0)) == R1.
+
+Lemma essai0 : (continuity_pt [x:R]``(x+2)/(y x)+x/(y x)`` R0).
+Assert H := d_y.
+Assert H0 := n_y.
+Reg.
+Qed.
+
+Lemma essai1 : (derivable_pt [x:R]``/2*(sin x)`` ``1``).
+Reg.
+Qed.
+
+Lemma essai2 : (continuity [x:R]``(Rsqr x)*(cos (x*x))+x``).
+Reg.
+Qed.
+
+Lemma essai3 : (derivable_pt [x:R]``x*((Rsqr x)+3)`` R0).
+Reg.
+Qed.
+
+Lemma essai4 : (derivable [x:R]``(x+x)*(sin x)``).
+Reg.
+Qed.
+
+Lemma essai5 : (derivable [x:R]``1+(sin (2*x+3))*(cos (cos x))``).
+Reg.
+Qed.
+
+Lemma essai6 : (derivable [x:R]``(cos (x+3))``).
+Reg.
+Qed.
+
+Lemma essai7 : (derivable_pt [x:R]``(cos (/(sqrt x)))*(Rsqr ((sin x)+1))`` R1).
+Reg.
+Apply Rlt_R0_R1.
+Red; Intro; Rewrite sqrt_1 in H; Assert H0 := R1_neq_R0; Elim H0; Assumption.
+Qed.
+
+Lemma essai8 : (derivable_pt [x:R]``(sqrt ((Rsqr x)+(sin x)+1))`` R0).
+Reg.
+Rewrite sin_0.
+Rewrite Rsqr_O.
+Replace ``0+0+1`` with ``1``; [Apply Rlt_R0_R1 | Ring].
+Qed.
+
+Lemma essai9 : (derivable_pt (plus_fct id sin) R1).
+Reg.
+Qed.
+
+Lemma essai10 : (derivable_pt [x:R]``x+2`` R0).
+Reg.
+Qed.
+
+Lemma essai11 : (derive_pt [x:R]``x+2`` R0 essai10)==R1.
+Reg.
+Qed.
+
+Lemma essai12 : (derivable [x:R]``x+(Rsqr (x+2))``).
+Reg.
+Qed.
+
+Lemma essai13 : (derive_pt [x:R]``x+(Rsqr (x+2))`` R0 (essai12 R0)) == ``5``.
+Reg.
+Qed.
+
+Lemma essai14 : (derivable_pt [x:R]``2*x+x`` ``2``).
+Reg.
+Qed.
+
+Lemma essai15 : (derive_pt [x:R]``2*x+x`` ``2`` essai14) == ``3``.
+Reg.
+Qed.
+
+Lemma essai16 : (derivable_pt [x:R]``x+(sin x)`` R0).
+Reg.
+Qed.
+
+Lemma essai17 : (derive_pt [x:R]``x+(sin x)`` R0 essai16)==``2``.
+Reg.
+Rewrite cos_0.
+Reflexivity.
+Qed.
+
+Lemma essai18 : (derivable_pt [x:R]``x+(y x)`` ``0``).
+Assert H := d_y.
+Reg.
+Qed.
+
+Lemma essai19 : (derive_pt [x:R]``x+(y x)`` ``0`` essai18) == ``2``.
+Assert H := dy_0.
+Assert H0 := d_y.
+Reg.
+Qed.
+
+Axiom z:R->R.
+Axiom d_z: (derivable z).
+
+Lemma essai20 : (derivable_pt [x:R]``(z (y x))`` R0).
+Reg.
+Apply d_y.
+Apply d_z.
+Qed.
+
+Lemma essai21 : (derive_pt [x:R]``(z (y x))`` R0 essai20) == R1.
+Assert H := dy_0.
+Reg.
+Abort.
+
+Lemma essai22 : (derivable [x:R]``(sin (z x))+(Rsqr (z x))/(y x)``).
+Assert H := d_y.
+Reg.
+Apply n_y.
+Apply d_z.
+Qed.
+
+(* Pour tester la continuite de sqrt en 0 *)
+Lemma essai23 : (continuity_pt [x:R]``(sin (sqrt (x-1)))+(exp (Rsqr ((sqrt x)+3)))`` R1).
+Reg.
+Left; Apply Rlt_R0_R1.
+Right; Unfold Rminus; Rewrite Rplus_Ropp_r; Reflexivity.
+Qed.
+
+Lemma essai24 : (derivable [x:R]``(sqrt (x*x+2*x+2))+(Rabsolu (x*x+1))``).
+Reg.
+Replace ``x*x+2*x+2`` with ``(Rsqr (x+1))+1``.
+Apply ge0_plus_gt0_is_gt0; [Apply pos_Rsqr | Apply Rlt_R0_R1].
+Unfold Rsqr; Ring.
+Red; Intro; Cut ``0<x*x+1``.
+Intro; Rewrite H in H0; Elim (Rlt_antirefl ? H0).
+Apply ge0_plus_gt0_is_gt0; [Replace ``x*x`` with (Rsqr x); [Apply pos_Rsqr | Reflexivity] | Apply Rlt_R0_R1].
+Qed.
diff --git a/test-suite/success/Remark.v b/test-suite/success/Remark.v
new file mode 100644
index 00000000..2dd6a211
--- /dev/null
+++ b/test-suite/success/Remark.v
@@ -0,0 +1,12 @@
+(* Test obsolete, Remark est maintenant global
+Section A.
+Section B.
+Section C.
+Remark t : True. Proof I.
+End C.
+Locate C.t.
+End B.
+Locate B.C.t.
+End A.
+Locate A.B.C.t.
+*)
diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v
new file mode 100644
index 00000000..edb20a81
--- /dev/null
+++ b/test-suite/success/Rename.v
@@ -0,0 +1,5 @@
+Goal (n:nat)(n=O)->(n=O).
+Intros.
+Rename n into p.
+NewInduction p; Auto.
+Qed.
diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v
new file mode 100644
index 00000000..654808fc
--- /dev/null
+++ b/test-suite/success/Require.v
@@ -0,0 +1,3 @@
+Require Coq.Arith.Plus.
+Read Module Coq.Arith.Minus.
+Locate Library Coq.Arith.Minus.
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
new file mode 100644
index 00000000..55d8343e
--- /dev/null
+++ b/test-suite/success/Scopes.v
@@ -0,0 +1,8 @@
+(* Check exportation of Argument Scopes even without import of modules *)
+
+Require Import ZArith.
+
+Module A.
+Definition opp := Zopp.
+End A.
+Check (A.opp 3).
diff --git a/test-suite/success/Simplify_eq.v b/test-suite/success/Simplify_eq.v
new file mode 100644
index 00000000..41aa77ef
--- /dev/null
+++ b/test-suite/success/Simplify_eq.v
@@ -0,0 +1,13 @@
+(* Check the behaviour of Simplify_eq *)
+
+(* Check that Simplify_eq tries Intro until *)
+
+Lemma l1 : O=(S O)->False.
+Simplify_eq 1.
+Qed.
+
+Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False.
+Simplify_eq H.
+Intros.
+Apply (n_Sn x H0).
+Qed.
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
new file mode 100644
index 00000000..883a82ab
--- /dev/null
+++ b/test-suite/success/Tauto.v
@@ -0,0 +1,240 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* $Id: Tauto.v,v 1.10.8.1 2004/07/16 19:30:59 herbelin Exp $ *)
+
+(**** Tactics Tauto and Intuition ****)
+
+(**** Tauto:
+ Tactic for automating proof in Intuionnistic Propositional Calculus, based on
+ the contraction-free LJT* of Dickhoff ****)
+
+(**** Intuition:
+ Simplifications of goals, based on LJT* calcul ****)
+
+(**** Examples of intuitionistic tautologies ****)
+Parameter A,B,C,D,E,F:Prop.
+Parameter even:nat -> Prop.
+Parameter P:nat -> Prop.
+
+Lemma Ex_Wallen:(A->(B/\C)) -> ((A->B)\/(A->C)).
+Proof.
+ Tauto.
+Save.
+
+Lemma Ex_Klenne:~(~(A \/ ~A)).
+Proof.
+ Tauto.
+Save.
+
+Lemma Ex_Klenne':(n:nat)(~(~((even n) \/ ~(even n)))).
+Proof.
+ Tauto.
+Save.
+
+Lemma Ex_Klenne'':~(~(((n:nat)(even n)) \/ ~((m:nat)(even m)))).
+Proof.
+ Tauto.
+Save.
+
+Lemma tauto:((x:nat)(P x)) -> ((y:nat)(P y)).
+Proof.
+ Tauto.
+Save.
+
+Lemma tauto1:(A -> A).
+Proof.
+ Tauto.
+Save.
+
+Lemma tauto2:(A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+ Tauto.
+Save.
+
+Lemma a:(x0: (A \/ B))(x1:(B /\ C))(A -> B).
+Proof.
+ Tauto.
+Save.
+
+Lemma a2:((A -> (B /\ C)) -> ((A -> B) \/ (A -> C))).
+Proof.
+ Tauto.
+Save.
+
+Lemma a4:(~A -> ~A).
+Proof.
+ Tauto.
+Save.
+
+Lemma e2:~(~(A \/ ~A)).
+Proof.
+ Tauto.
+Save.
+
+Lemma e4:~(~((A \/ B) -> (A \/ B))).
+Proof.
+ Tauto.
+Save.
+
+Lemma y0:(x0:A)(x1: ~A)(x2:(A -> B))(x3:(A \/ B))(x4:(A /\ B))(A -> False).
+Proof.
+ Tauto.
+Save.
+
+Lemma y1:(x0:((A /\ B) /\ C))B.
+Proof.
+ Tauto.
+Save.
+
+Lemma y2:(x0:A)(x1:B)(C \/ B).
+Proof.
+ Tauto.
+Save.
+
+Lemma y3:(x0:(A /\ B))(B /\ A).
+Proof.
+ Tauto.
+Save.
+
+Lemma y5:(x0:(A \/ B))(B \/ A).
+Proof.
+ Tauto.
+Save.
+
+Lemma y6:(x0:(A -> B))(x1:A) B.
+Proof.
+ Tauto.
+Save.
+
+Lemma y7:(x0 : ((A /\ B) -> C))(x1 : B)(x2 : A) C.
+Proof.
+ Tauto.
+Save.
+
+Lemma y8:(x0 : ((A \/ B) -> C))(x1 : A) C.
+Proof.
+ Tauto.
+Save.
+
+Lemma y9:(x0 : ((A \/ B) -> C))(x1 : B) C.
+Proof.
+ Tauto.
+Save.
+
+Lemma y10:(x0 : ((A -> B) -> C))(x1 : B) C.
+Proof.
+ Tauto.
+Save.
+
+(* This example took much time with the old version of Tauto *)
+Lemma critical_example0:(~~B->B)->(A->B)->~~A->B.
+Proof.
+ Tauto.
+Save.
+
+(* Same remark as previously *)
+Lemma critical_example1:(~~B->B)->(~B->~A)->~~A->B.
+Proof.
+ Tauto.
+Save.
+
+(* This example took very much time (about 3mn on a PIII 450MHz in bytecode)
+ with the old Tauto. Now, it's immediate (less than 1s). *)
+Lemma critical_example2:(~A<->B)->(~B<->A)->(~~A<->A).
+Proof.
+ Tauto.
+Save.
+
+(* This example was a bug *)
+Lemma old_bug0:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F.
+Proof.
+ Tauto.
+Save.
+
+(* Another bug *)
+Lemma old_bug1:((A->B->False)->False) -> (B->False) -> False.
+Proof.
+ Tauto.
+Save.
+
+(* A bug again *)
+Lemma old_bug2:
+ ((((C->False)->A)->((B->False)->A)->False)->False) ->
+ (((C->B->False)->False)->False) ->
+ ~A->A.
+Proof.
+ Tauto.
+Save.
+
+(* A bug from CNF form *)
+Lemma old_bug3:
+ ((~A\/B)/\(~B\/B)/\(~A\/~B)/\(~B\/~B)->False)->~((A->B)->B)->False.
+Proof.
+ Tauto.
+Save.
+
+(* sometimes, the behaviour of Tauto depends on the order of the hyps *)
+Lemma old_bug3bis:
+ ~((A->B)->B)->((~B\/~B)/\(~B\/~A)/\(B\/~B)/\(B\/~A)->False)->False.
+Proof.
+ Tauto.
+Save.
+
+(* A bug found by Freek Wiedijk <freek@cs.kun.nl> *)
+Lemma new_bug:
+ ((A<->B)->(B<->C)) ->
+ ((B<->C)->(C<->A)) ->
+ ((C<->A)->(A<->B)) ->
+ (A<->B).
+Proof.
+ Tauto.
+Save.
+
+
+(* A private club has the following rules :
+ *
+ * . rule 1 : Every non-scottish member wears red socks
+ * . rule 2 : Every member wears a kilt or doesn't wear red socks
+ * . rule 3 : The married members don't go out on sunday
+ * . rule 4 : A member goes out on sunday if and only if he is scottish
+ * . rule 5 : Every member who wears a kilt is scottish and married
+ * . rule 6 : Every scottish member wears a kilt
+ *
+ * Actually, no one can be accepted !
+ *)
+
+Section club.
+
+Variable Scottish, RedSocks, WearKilt, Married, GoOutSunday : Prop.
+
+Hypothesis rule1 : ~Scottish -> RedSocks.
+Hypothesis rule2 : WearKilt \/ ~RedSocks.
+Hypothesis rule3 : Married -> ~GoOutSunday.
+Hypothesis rule4 : GoOutSunday <-> Scottish.
+Hypothesis rule5 : WearKilt -> (Scottish /\ Married).
+Hypothesis rule6 : Scottish -> WearKilt.
+
+Lemma NoMember : False.
+Tauto.
+Save.
+
+End club.
+
+(**** Use of Intuition ****)
+Lemma intu0:(((x:nat)(P x)) /\ B) ->
+ (((y:nat)(P y)) /\ (P O)) \/ (B /\ (P O)).
+Proof.
+ Intuition.
+Save.
+
+Lemma intu1:((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y).
+Proof.
+ Intuition.
+Save.
+
diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v
new file mode 100644
index 00000000..05cab1e6
--- /dev/null
+++ b/test-suite/success/Try.v
@@ -0,0 +1,8 @@
+(* To shorten interactive scripts, it is better that Try catches
+ non-existent names in Unfold [cf bug #263] *)
+
+Lemma lem1 : True.
+Try (Unfold i_dont_exist).
+Trivial.
+Qed.
+
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
new file mode 100644
index 00000000..4d898da9
--- /dev/null
+++ b/test-suite/success/cc.v
@@ -0,0 +1,83 @@
+
+Theorem t1: (A:Set)(a:A)(f:A->A)
+ (f a)=a->(f (f a))=a.
+Intros.
+Congruence.
+Save.
+
+Theorem t2: (A:Set)(a,b:A)(f:A->A)(g:A->A->A)
+ a=(f a)->(g b (f a))=(f (f a))->(g a b)=(f (g b a))->
+ (g a b)=a.
+Intros.
+Congruence.
+Save.
+
+(* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *)
+
+Theorem t3: (N:Set)(o:N)(s:N->N)(d:N->N)
+ (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s o)))))))))))))))=o->
+ (s (s (s (s (s (s (s (s (s (s o))))))))))=o->
+ (s (s (s (s (s (s o))))))=o->
+ o=(s o).
+Intros.
+Congruence.
+Save.
+
+(* Examples that fail due to dependencies *)
+
+(* yields transitivity problem *)
+
+Theorem dep:(A:Set)(P:A->Set)(f,g:(x:A)(P x))(x,y:A)
+ (e:x=y)(e0:(f y)=(g y))(f x)=(g x).
+Intros;Dependent Rewrite -> e;Exact e0.
+Save.
+
+(* yields congruence problem *)
+
+Theorem dep2:(A,B:Set)(f:(A:Set)(b:bool)if b then unit else A->unit)(e:A==B)
+ (f A true)=(f B true).
+Intros;Rewrite e;Reflexivity.
+Save.
+
+
+(* example that Congruence. can solve
+ (dependent function applied to the same argument)*)
+
+Theorem dep3:(A:Set)(P:(A->Set))(f,g:(x:A)(P x))f=g->(x:A)(f x)=(g x). Intros.
+Congruence.
+Save.
+
+(* Examples with injection rule *)
+
+Theorem inj1 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d.
+Intros.
+Split;Congruence.
+Save.
+
+Theorem inj2 : (A:Set;a,c,d:A;f:A->A*A) (f=(pair A A a))->
+ (Some ? (f c))=(Some ? (f d))->c=d.
+Intros.
+Congruence.
+Save.
+
+(* Examples with discrimination rule *)
+
+Theorem discr1 : true=false->False.
+Intros.
+Congruence.
+Save.
+
+Theorem discr2 : (Some ? true)=(Some ? false)->False.
+Intros.
+Congruence.
+Save.
+
+(* example with Congruence.Solve (requires CCSolve.v)*)
+
+Require CCSolve.
+
+Theorem t4 : (A:Set; P:(A->Prop); a,b,c,d:A)a=b->c=d->
+ (P a)->((P b)->(P c))->(P d).
+Intros.
+CCsolve.
+Save.
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
new file mode 100644
index 00000000..98b613ba
--- /dev/null
+++ b/test-suite/success/coercions.v
@@ -0,0 +1,11 @@
+(* Interaction between coercions and casts *)
+(* Example provided by Eduardo Gimenez *)
+
+Parameter Z,S:Set.
+
+Parameter f: S -> Z.
+Coercion f: S >-> Z.
+
+Parameter g : Z -> Z.
+
+Check [s](g (s::S)).
diff --git a/test-suite/success/coqbugs0181.v b/test-suite/success/coqbugs0181.v
new file mode 100644
index 00000000..21f906a6
--- /dev/null
+++ b/test-suite/success/coqbugs0181.v
@@ -0,0 +1,7 @@
+
+(* test the strength of pretyping unification *)
+
+Require PolyList.
+Definition listn := [A,n] {l:(list A)|(length l)=n}.
+Definition make_ln [A,n;l:(list A); h:([l](length l)=n l)] :=
+ (exist ?? l h).
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
new file mode 100644
index 00000000..97f7ccf0
--- /dev/null
+++ b/test-suite/success/eauto.v
@@ -0,0 +1,49 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+Require PolyList.
+
+Parameter in_list : (list nat*nat)->nat->Prop.
+Definition not_in_list : (list nat*nat)->nat->Prop
+ := [l,n]~(in_list l n).
+
+(* Hints Unfold not_in_list. *)
+
+Axiom lem1 : (l1,l2:(list nat*nat))(n:nat)
+ (not_in_list (app l1 l2) n)->(not_in_list l1 n).
+
+Axiom lem2 : (l1,l2:(list nat*nat))(n:nat)
+ (not_in_list (app l1 l2) n)->(not_in_list l2 n).
+
+Axiom lem3 : (l:(list nat*nat))(n,p,q:nat)
+ (not_in_list (cons (p,q) l) n)->(not_in_list l n).
+
+Axiom lem4 : (l1,l2:(list nat*nat))(n:nat)
+ (not_in_list l1 n)->(not_in_list l2 n)->(not_in_list (app l1 l2) n).
+
+Hints Resolve lem1 lem2 lem3 lem4: essai.
+
+Goal (l:(list nat*nat))(n,p,q:nat)
+ (not_in_list (cons (p,q) l) n)->(not_in_list l n).
+Intros.
+EAuto with essai.
+Save.
+
+(* Example from Nicolas Magaud on coq-club - Jul 2000 *)
+
+Definition Nat: Set := nat.
+Parameter S':Nat ->Nat.
+Parameter plus':Nat -> Nat ->Nat.
+
+Lemma simpl_plus_l_rr1:
+ ((n0:Nat) ((m, p:Nat) (plus' n0 m)=(plus' n0 p) ->m=p) ->
+ (m, p:Nat) (S' (plus' n0 m))=(S' (plus' n0 p)) ->m=p) ->
+ (n:Nat) ((m, p:Nat) (plus' n m)=(plus' n p) ->m=p) ->
+ (m, p:Nat) (S' (plus' n m))=(S' (plus' n p)) ->m=p.
+Intros.
+EAuto. (* does EApply H *)
+Qed.
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
new file mode 100644
index 00000000..f826df9a
--- /dev/null
+++ b/test-suite/success/eqdecide.v
@@ -0,0 +1,29 @@
+(************************************************************************)
+(* 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 T : Set := A: T | B :T->T.
+
+Lemma lem1 : (x,y:T){x=y}+{~x=y}.
+Decide Equality.
+Qed.
+
+Lemma lem2 : (x,y:T){x=y}+{~x=y}.
+Intros x y.
+Decide Equality x y.
+Qed.
+
+Lemma lem3 : (x,y:T){x=y}+{~x=y}.
+Intros x y.
+Decide Equality y x.
+Qed.
+
+Lemma lem4 : (x,y:T){x=y}+{~x=y}.
+Intros x y.
+Compare x y; Auto.
+Qed.
+
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
new file mode 100644
index 00000000..a7b6d6d8
--- /dev/null
+++ b/test-suite/success/evars.v
@@ -0,0 +1,23 @@
+(* The "?" of cons and eq should be inferred *)
+Variable list:Set -> Set.
+Variable cons:(T:Set) T -> (list T) -> (list T).
+Check (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))).
+
+(* Examples provided by Eduardo Gimenez *)
+
+Definition c [A;Q:(nat*A->Prop)->Prop;P] :=
+ (Q [p:nat*A]let (i,v) = p in (P i v)).
+
+(* What does this test ? *)
+Require PolyList.
+Definition list_forall_bool [A:Set][p:A->bool][l:(list A)] : bool :=
+ (fold_right ([a][r]if (p a) then r else false) true l).
+
+(* Checks that solvable ? in the lambda prefix of the definition are harmless*)
+Parameter A1,A2,F,B,C : Set.
+Parameter f : F -> A1 -> B.
+Definition f1 [frm0,a1]: B := (f frm0 a1).
+
+(* Checks that solvable ? in the type part of the definition are harmless *)
+Definition f2 : (frm0:?;a1:?)B := [frm0,a1](f frm0 a1).
+
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
new file mode 100644
index 00000000..374029bb
--- /dev/null
+++ b/test-suite/success/fix.v
@@ -0,0 +1,51 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(* Ancien bug signale par Laurent Thery sur la condition de garde *)
+
+Require Import Bool.
+Require Import ZArith.
+
+Definition rNat := positive.
+
+Inductive rBoolOp: Set :=
+ rAnd: rBoolOp
+ | rEq: rBoolOp .
+
+Definition rlt: rNat -> rNat ->Prop := [a, b:rNat](compare a b EGAL)=INFERIEUR.
+
+Definition rltDec: (m, n:rNat){(rlt m n)}+{(rlt n m) \/ m=n}.
+Intros n m; Generalize (compare_convert_INFERIEUR n m);
+ Generalize (compare_convert_SUPERIEUR n m);
+ Generalize (compare_convert_EGAL n m); Case (compare n m EGAL).
+Intros H' H'0 H'1; Right; Right; Auto.
+Intros H' H'0 H'1; Left; Unfold rlt.
+Apply convert_compare_INFERIEUR; Auto.
+Intros H' H'0 H'1; Right; Left; Unfold rlt.
+Apply convert_compare_INFERIEUR; Auto.
+Apply H'0; Auto.
+Defined.
+
+
+Definition rmax: rNat -> rNat ->rNat.
+Intros n m; Case (rltDec n m); Intros Rlt0.
+Exact m.
+Exact n.
+Defined.
+
+Inductive rExpr: Set :=
+ rV: rNat ->rExpr
+ | rN: rExpr ->rExpr
+ | rNode: rBoolOp -> rExpr -> rExpr ->rExpr .
+
+Fixpoint maxVar[e:rExpr]: rNat :=
+ Cases e of
+ (rV n) => n
+ | (rN p) => (maxVar p)
+ | (rNode n p q) => (rmax (maxVar p) (maxVar q))
+ end.
+
diff --git a/test-suite/success/if.v b/test-suite/success/if.v
new file mode 100644
index 00000000..85cd1f11
--- /dev/null
+++ b/test-suite/success/if.v
@@ -0,0 +1,5 @@
+(* The synthesis of the elimination predicate may fail if algebric *)
+(* universes are not cautiously treated *)
+
+Check [b:bool]if b then Type else nat.
+
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
new file mode 100644
index 00000000..c597f9bf
--- /dev/null
+++ b/test-suite/success/implicit.v
@@ -0,0 +1,31 @@
+(* Implicit on section variables *)
+
+Set Implicit Arguments.
+
+(* Example submitted by David Nowak *)
+
+Section Spec.
+Variable A:Set.
+Variable op : (A:Set)A->A->Set.
+Infix 6 "#" op V8only (at level 70).
+Check (x:A)(x # x).
+
+(* Example submitted by Christine *)
+Record stack : Type := {type : Set; elt : type;
+ empty : type -> bool; proof : (empty elt)=true }.
+
+Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack.
+
+End Spec.
+
+(* Example submitted by Frédéric (interesting in v8 syntax) *)
+
+Parameter f : nat -> nat * nat.
+Notation lhs := fst.
+Check [x](lhs ? ? (f x)).
+Check [x](!lhs ? ? (f x)).
+Notation "'rhs'" := snd.
+Check [x](rhs ? ? (f x)).
+(* V8 seulement
+Check (fun x => @ rhs ? ? (f x)).
+*)
diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v
new file mode 100644
index 00000000..d031691d
--- /dev/null
+++ b/test-suite/success/import_lib.v
@@ -0,0 +1,202 @@
+Definition le_trans:=O.
+
+
+Module Test_Read.
+ Module M.
+ Read Module Le. (* Reading without importing *)
+
+ Check Le.le_trans.
+
+ Lemma th0 : le_trans = O.
+ Reflexivity.
+ Qed.
+ End M.
+
+ Check Le.le_trans.
+
+ Lemma th0 : le_trans = O.
+ Reflexivity.
+ Qed.
+
+ Import M.
+
+ Lemma th1 : le_trans = O.
+ Reflexivity.
+ Qed.
+End Test_Read.
+
+
+(****************************************************************)
+
+Definition le_decide := (S O). (* from Arith/Compare *)
+Definition min := O. (* from Arith/Min *)
+
+Module Test_Require.
+
+ Module M.
+ Require Compare. (* Imports Min as well *)
+
+ Lemma th1 : le_decide = Compare.le_decide.
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : min = Min.min.
+ Reflexivity.
+ Qed.
+
+ End M.
+
+ (* Checks that Compare and List are loaded *)
+ Check Compare.le_decide.
+ Check Min.min.
+
+
+ (* Checks that Compare and List are _not_ imported *)
+ Lemma th1 : le_decide = (S O).
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : min = O.
+ Reflexivity.
+ Qed.
+
+ (* It should still be the case after Import M *)
+ Import M.
+
+ Lemma th3 : le_decide = (S O).
+ Reflexivity.
+ Qed.
+
+ Lemma th4 : min = O.
+ Reflexivity.
+ Qed.
+
+End Test_Require.
+
+(****************************************************************)
+
+Module Test_Import.
+ Module M.
+ Import Compare. (* Imports Min as well *)
+
+ Lemma th1 : le_decide = Compare.le_decide.
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : min = Min.min.
+ Reflexivity.
+ Qed.
+
+ End M.
+
+ (* Checks that Compare and List are loaded *)
+ Check Compare.le_decide.
+ Check Min.min.
+
+
+ (* Checks that Compare and List are _not_ imported *)
+ Lemma th1 : le_decide = (S O).
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : min = O.
+ Reflexivity.
+ Qed.
+
+ (* It should still be the case after Import M *)
+ Import M.
+
+ Lemma th3 : le_decide = (S O).
+ Reflexivity.
+ Qed.
+
+ Lemma th4 : min = O.
+ Reflexivity.
+ Qed.
+End Test_Import.
+
+(************************************************************************)
+
+Module Test_Export.
+ Module M.
+ Export Compare. (* Exports Min as well *)
+
+ Lemma th1 : le_decide = Compare.le_decide.
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : min = Min.min.
+ Reflexivity.
+ Qed.
+
+ End M.
+
+
+ (* Checks that Compare and List are _not_ imported *)
+ Lemma th1 : le_decide = (S O).
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : min = O.
+ Reflexivity.
+ Qed.
+
+
+ (* After Import M they should be imported as well *)
+
+ Import M.
+
+ Lemma th3 : le_decide = Compare.le_decide.
+ Reflexivity.
+ Qed.
+
+ Lemma th4 : min = Min.min.
+ Reflexivity.
+ Qed.
+End Test_Export.
+
+
+(************************************************************************)
+
+Module Test_Require_Export.
+
+ Definition mult_sym:=(S O). (* from Arith/Mult *)
+ Definition plus_sym:=O. (* from Arith/Plus *)
+
+ Module M.
+ Require Export Mult. (* Exports Plus as well *)
+
+ Lemma th1 : mult_sym = Mult.mult_sym.
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : plus_sym = Plus.plus_sym.
+ Reflexivity.
+ Qed.
+
+ End M.
+
+
+ (* Checks that Mult and Plus are _not_ imported *)
+ Lemma th1 : mult_sym = (S O).
+ Reflexivity.
+ Qed.
+
+ Lemma th2 : plus_sym = O.
+ Reflexivity.
+ Qed.
+
+
+ (* After Import M they should be imported as well *)
+
+ Import M.
+
+ Lemma th3 : mult_sym = Mult.mult_sym.
+ Reflexivity.
+ Qed.
+
+ Lemma th4 : plus_sym = Plus.plus_sym.
+ Reflexivity.
+ Qed.
+
+End Test_Require_Export.
diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v
new file mode 100644
index 00000000..b4a8af46
--- /dev/null
+++ b/test-suite/success/import_mod.v
@@ -0,0 +1,75 @@
+
+Definition p:=O.
+Definition m:=O.
+
+Module Test_Import.
+ Module P.
+ Definition p:=(S O).
+ End P.
+
+ Module M.
+ Import P.
+ Definition m:=p.
+ End M.
+
+ Module N.
+ Import M.
+
+ Lemma th0 : p=O.
+ Reflexivity.
+ Qed.
+
+ End N.
+
+
+ (* M and P should be closed *)
+ Lemma th1 : m=O /\ p=O.
+ Split; Reflexivity.
+ Qed.
+
+
+ Import N.
+
+ (* M and P should still be closed *)
+ Lemma th2 : m=O /\ p=O.
+ Split; Reflexivity.
+ Qed.
+End Test_Import.
+
+
+(********************************************************************)
+
+
+Module Test_Export.
+ Module P.
+ Definition p:=(S O).
+ End P.
+
+ Module M.
+ Export P.
+ Definition m:=p.
+ End M.
+
+ Module N.
+ Export M.
+
+ Lemma th0 : p=(S O).
+ Reflexivity.
+ Qed.
+
+ End N.
+
+
+ (* M and P should be closed *)
+ Lemma th1 : m=O /\ p=O.
+ Split; Reflexivity.
+ Qed.
+
+
+ Import N.
+
+ (* M and P should now be opened *)
+ Lemma th2 : m=(S O) /\ p=(S O).
+ Split; Reflexivity.
+ Qed.
+End Test_Export.
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
new file mode 100644
index 00000000..a391b804
--- /dev/null
+++ b/test-suite/success/inds_type_sec.v
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+Section S.
+Inductive T [U:Type] : Type := c : U -> (T U).
+End S.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
new file mode 100644
index 00000000..9ae498d2
--- /dev/null
+++ b/test-suite/success/induct.v
@@ -0,0 +1,17 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(* Teste des definitions inductives imbriquees *)
+
+Require PolyList.
+
+Inductive X : Set :=
+ cons1 : (list X)->X.
+
+Inductive Y : Set :=
+ cons2 : (list Y*Y)->Y.
+
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
new file mode 100644
index 00000000..55aa110d
--- /dev/null
+++ b/test-suite/success/ltac.v
@@ -0,0 +1,70 @@
+(* The tactic language *)
+
+(* Submitted by Pierre Crégut *)
+(* Checks substitution of x *)
+Tactic Definition f x := Unfold x; Idtac.
+
+Lemma lem1 : (plus O O) = O.
+f plus.
+Reflexivity.
+Qed.
+
+(* Submitted by Pierre Crégut *)
+(* Check syntactic correctness *)
+Recursive Tactic Definition F x := Idtac; (G x)
+And G y := Idtac; (F y).
+
+(* Check that Match Context keeps a closure *)
+Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a.
+
+Lemma lem2 : True.
+U.
+Qed.
+
+(* Check that Match giving non-tactic arguments are evaluated at Let-time *)
+
+Tactic Definition B :=
+ Let y = (Match Context With [ z:? |- ? ] -> z) In
+ Intro H1; Exact y.
+
+Lemma lem3 : True -> False -> True -> False.
+Intros H H0.
+B. (* y is H0 if at let-time, H1 otherwise *)
+Qed.
+
+(* Checks the matching order of hypotheses *)
+Tactic Definition Y := Match Context With [ x:?; y:? |- ? ] -> Apply x.
+Tactic Definition Z := Match Context With [ y:?; x:? |- ? ] -> Apply x.
+
+Lemma lem4 : (True->False) -> (False->False) -> False.
+Intros H H0.
+Z. (* Apply H0 *)
+Y. (* Apply H *)
+Exact I.
+Qed.
+
+(* Check backtracking *)
+Lemma back1 : (0)=(1)->(0)=(0)->(1)=(1)->(0)=(0).
+Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1).
+Qed.
+
+Lemma back2 : (0)=(0)->(0)=(1)->(1)=(1)->(0)=(0).
+Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1).
+Qed.
+
+Lemma back3 : (0)=(0)->(1)=(1)->(0)=(1)->(0)=(0).
+Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1).
+Qed.
+
+(* Check context binding *)
+Tactic Definition sym t := Match t With [C[?1=?2]] -> Inst C[?1=?2].
+
+Lemma sym : ~(0)=(1)->~(1)=(0).
+Intro H.
+Let t = (sym (Check H)) In Assert t.
+Exact H.
+Intro H1.
+Apply H.
+Symmetry.
+Assumption.
+Qed.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
new file mode 100644
index 00000000..e932f50c
--- /dev/null
+++ b/test-suite/success/mutual_ind.v
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(* Definition mutuellement inductive et dependante *)
+
+Require Export PolyList.
+
+ Record signature : Type := {
+ sort : Set;
+ sort_beq : sort->sort->bool;
+ sort_beq_refl : (f:sort)true=(sort_beq f f);
+ sort_beq_eq : (f1,f2:sort)true=(sort_beq f1 f2)->f1=f2;
+ fsym :> Set;
+ fsym_type : fsym->(list sort)*sort;
+ fsym_beq : fsym->fsym->bool;
+ fsym_beq_refl : (f:fsym)true=(fsym_beq f f);
+ fsym_beq_eq : (f1,f2:fsym)true=(fsym_beq f1 f2)->f1=f2
+ }.
+
+
+ Variable F : signature.
+
+ Definition vsym := (sort F)*nat.
+
+ Definition vsym_sort := (fst (sort F) nat).
+ Definition vsym_nat := (snd (sort F) nat).
+
+
+ Mutual Inductive term : (sort F)->Set :=
+ | term_var : (v:vsym)(term (vsym_sort v))
+ | term_app : (f:F)(list_term (Fst (fsym_type F f)))
+ ->(term (Snd (fsym_type F f)))
+ with list_term : (list (sort F)) -> Set :=
+ | term_nil : (list_term (nil (sort F)))
+ | term_cons : (s:(sort F);l:(list (sort F)))
+ (term s)->(list_term l)->(list_term (cons s l)).
+
diff --git a/test-suite/success/options.v b/test-suite/success/options.v
new file mode 100644
index 00000000..9e9af4fa
--- /dev/null
+++ b/test-suite/success/options.v
@@ -0,0 +1,34 @@
+(* Check that the syntax for options works *)
+Set Implicit Arguments.
+Unset Implicit Arguments.
+Test Implicit Arguments.
+
+Set Printing Coercions.
+Unset Printing Coercions.
+Test Printing Coercions.
+
+Set Silent.
+Unset Silent.
+Test Silent.
+
+Set Printing Depth 100.
+Print Table Printing Depth.
+
+Parameter i : bool -> nat.
+Coercion i : bool >-> nat.
+Set Printing Coercion i.
+Unset Printing Coercion i.
+Test Printing Coercion i.
+
+Print Table Printing Let.
+Print Table Printing If.
+Remove Printing Let sig.
+Remove Printing If bool.
+
+Unset Printing Synth.
+Set Printing Synth.
+Test Printing Synth.
+
+Unset Printing Wildcard.
+Set Printing Wildcard.
+Test Printing Wildcard.
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
new file mode 100644
index 00000000..ad4eed5a
--- /dev/null
+++ b/test-suite/success/refine.v
@@ -0,0 +1,30 @@
+
+(* Refine and let-in's *)
+
+Goal (EX x:nat | x=O).
+Refine let y = (plus O O) in ?.
+Exists y; Auto.
+Save test1.
+
+Goal (EX x:nat | x=O).
+Refine let y = (plus O O) in (ex_intro ? ? (plus y y) ?).
+Auto.
+Save test2.
+
+Goal nat.
+Refine let y = O in (plus O ?).
+Exact (S O).
+Save test3.
+
+(* Example submitted by Yves on coqdev *)
+
+Require PolyList.
+
+Goal (l:(list nat))l=l.
+Proof.
+Refine [l]<[l]l=l>
+ Cases l of
+ | nil => ?
+ | (cons O l0) => ?
+ | (cons (S _) l0) => ?
+ end.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
new file mode 100644
index 00000000..2d2b2af8
--- /dev/null
+++ b/test-suite/success/setoid_test.v
@@ -0,0 +1,104 @@
+Require Setoid.
+
+Parameter A : Set.
+
+Axiom eq_dec : (a,b :A) {a=b}+{~a=b}.
+
+Inductive set : Set :=
+|Empty : set
+|Add : A -> set -> set.
+
+Fixpoint In [a:A; s:set] : Prop :=
+Cases s of
+|Empty => False
+|(Add b s') => a=b \/ (In a s')
+end.
+
+Definition same [s,t:set] : Prop :=
+(a:A) (In a s) <-> (In a t).
+
+Lemma setoid_set : (Setoid_Theory set same).
+
+Unfold same; Split.
+Red; Auto.
+
+Red.
+Intros.
+Elim (H a); Auto.
+
+Intros.
+Elim (H a); Elim (H0 a).
+Split; Auto.
+Save.
+
+Add Setoid set same setoid_set.
+
+Add Morphism In : In_ext.
+Unfold same; Intros a s t H; Elim (H a); Auto.
+Save.
+
+Lemma add_aux : (s,t:set) (same s t) ->
+ (a,b:A)(In a (Add b s)) -> (In a (Add b t)).
+Unfold same; Induction 2; Intros.
+Rewrite H1.
+Simpl; Left; Reflexivity.
+
+Elim (H a).
+Intros.
+Simpl; Right.
+Apply (H2 H1).
+Save.
+
+Add Morphism Add : Add_ext.
+Split; Apply add_aux.
+Assumption.
+
+Rewrite H.
+Apply Seq_refl.
+Exact setoid_set.
+Save.
+
+Fixpoint remove [a:A; s:set] : set :=
+Cases s of
+|Empty => Empty
+|(Add b t) => Cases (eq_dec a b) of
+ |(left _) => (remove a t)
+ |(right _) => (Add b (remove a t))
+ end
+end.
+
+Lemma in_rem_not : (a:A)(s:set) ~(In a (remove a (Add a Empty))).
+
+Intros.
+Setoid_replace (remove a (Add a Empty)) with Empty.
+Unfold same.
+Split.
+Simpl.
+Intro H; Elim H.
+
+Simpl.
+Case (eq_dec a a).
+Intros e ff; Elim ff.
+
+Intros; Absurd a=a; Trivial.
+
+Auto.
+Save.
+
+Parameter P :set -> Prop.
+Parameter P_ext : (s,t:set) (same s t) -> (P s) -> (P t).
+
+Add Morphism P : P_extt.
+Exact P_ext.
+Save.
+
+Lemma test_rewrite : (a:A)(s,t:set)(same s t) -> (P (Add a s)) -> (P (Add a t)).
+Intros.
+Rewrite <- H.
+Rewrite H.
+Setoid_rewrite <- H.
+Setoid_rewrite H.
+Setoid_rewrite <- H.
+Trivial.
+Save.
+
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
new file mode 100644
index 00000000..de75dfce
--- /dev/null
+++ b/test-suite/success/unfold.v
@@ -0,0 +1,15 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(* Test le Hint Unfold sur des var locales *)
+
+Section toto.
+Local EQ:=eq.
+Goal (EQ nat O O).
+Hints Unfold EQ.
+Auto.
+Save.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
new file mode 100644
index 00000000..0a4b284f
--- /dev/null
+++ b/test-suite/success/univers.v
@@ -0,0 +1,19 @@
+(* This requires cumulativity *)
+
+Definition Type2 := Type.
+Definition Type1 := Type : Type2.
+
+Lemma lem1 : (True->Type1)->Type2.
+Intro H.
+Apply H.
+Exact I.
+Qed.
+
+Lemma lem2 : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x).
+Auto.
+Qed.
+
+Lemma lem3 : (P:Prop)P.
+Intro P ; Pattern P.
+Apply lem2.
+Abort.
diff --git a/test-suite/tactics/TestRefine.v b/test-suite/tactics/TestRefine.v
new file mode 100644
index 00000000..f752c5bc
--- /dev/null
+++ b/test-suite/tactics/TestRefine.v
@@ -0,0 +1,203 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* Petit bench vite fait, mal fait *)
+
+Require Refine.
+
+
+(************************************************************************)
+
+Lemma essai : (x:nat)x=x.
+
+Refine (([x0:nat]Cases x0 of
+ O => ?
+ | (S p) => ?
+ end) :: (x:nat)x=x). (* x0=x0 et x0=x0 *)
+
+Restart.
+
+Refine [x0:nat]<[n:nat]n=n>Case x0 of ? [p:nat]? end. (* OK *)
+
+Restart.
+
+Refine [x0:nat]<[n:nat]n=n>Cases x0 of O => ? | (S p) => ? end. (* OK *)
+
+Restart.
+
+(**
+Refine [x0:nat]Cases x0 of O => ? | (S p) => ? end. (* cannot be executed *)
+**)
+
+Abort.
+
+
+(************************************************************************)
+
+Lemma T : nat.
+
+Refine (S ?).
+
+Abort.
+
+
+(************************************************************************)
+
+Lemma essai2 : (x:nat)x=x.
+
+Refine Fix f{f/1 : (x:nat)x=x := [x:nat]? }.
+
+Restart.
+
+Refine Fix f{f/1 : (x:nat)x=x :=
+ [x:nat]<[n:nat](eq nat n n)>Case x of ? [p:nat]? end}.
+
+Restart.
+
+Refine Fix f{f/1 : (x:nat)x=x :=
+ [x:nat]<[n:nat]n=n>Cases x of O => ? | (S p) => ? end}.
+
+Restart.
+
+Refine Fix f{f/1 : (x:nat)x=x :=
+ [x:nat]<[n:nat](eq nat n n)>Case x of
+ ?
+ [p:nat](f_equal nat nat S p p ?) end}.
+
+Restart.
+
+Refine Fix f{f/1 : (x:nat)x=x :=
+ [x:nat]<[n:nat](eq nat n n)>Cases x of
+ O => ?
+ | (S p) =>(f_equal nat nat S p p ?) end}.
+
+Abort.
+
+
+(************************************************************************)
+
+Lemma essai : nat.
+
+Parameter f : nat*nat -> nat -> nat.
+
+Refine (f ? ([x:nat](? :: nat) O)).
+
+Restart.
+
+Refine (f ? O).
+
+Abort.
+
+
+(************************************************************************)
+
+Parameter P : nat -> Prop.
+
+Lemma essai : { x:nat | x=(S O) }.
+
+Refine (exist nat ? (S O) ?). (* ECHEC *)
+
+Restart.
+
+(* mais si on contraint par le but alors ca marche : *)
+(* Remarque : on peut toujours faire ça *)
+Refine ((exist nat ? (S O) ?) :: { x:nat | x=(S O) }).
+
+Restart.
+
+Refine (exist nat [x:nat](x=(S O)) (S O) ?).
+
+Abort.
+
+
+(************************************************************************)
+
+Lemma essai : (n:nat){ x:nat | x=(S n) }.
+
+Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end.
+
+Restart.
+
+Refine (([n:nat]Case n of ? [p:nat]? end) :: (n:nat){ x:nat | x=(S n) }).
+
+Restart.
+
+Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end.
+
+Restart.
+
+Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} :=
+ [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end}.
+
+Restart.
+
+Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} :=
+ [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end}.
+
+Exists (S O). Trivial.
+Elim (f0 p).
+Refine [x:nat][h:x=(S p)](exist nat [x:nat]x=(S (S p)) (S x) ?).
+Rewrite h. Auto.
+Save.
+
+
+
+(* Quelques essais de recurrence bien fondée *)
+
+Require Wf.
+Require Wf_nat.
+
+Lemma essai_wf : nat->nat.
+
+Refine [x:nat](well_founded_induction
+ nat
+ lt ?
+ [_:nat]nat->nat
+ [phi0:nat][w:(phi:nat)(lt phi phi0)->nat->nat](w x ?)
+ x x).
+Exact lt_wf.
+
+Abort.
+
+
+Require Compare_dec.
+Require Lt.
+
+Lemma fibo : nat -> nat.
+Refine (well_founded_induction
+ nat
+ lt ?
+ [_:nat]nat
+ [x0:nat][fib:(x:nat)(lt x x0)->nat]
+ Cases (zerop x0) of
+ (left _) => (S O)
+ | (right h1) => Cases (zerop (pred x0)) of
+ (left _) => (S O)
+ | (right h2) => (plus (fib (pred x0) ?)
+ (fib (pred (pred x0)) ?))
+ end
+ end).
+(*********
+Refine (well_founded_induction
+ nat
+ lt ?
+ [_:nat]nat
+ [x0:nat][fib:(x:nat)(lt x x0)->nat]
+ Cases x0 of
+ O => (S O)
+ | (S O) => (S O)
+ | (S (S p)) => (plus (fib (pred x0) ?)
+ (fib (pred (pred x0)) ?))
+ end).
+***********)
+Exact lt_wf.
+Auto.
+Apply lt_trans with m:=(pred x0); Auto.
+Save.
+
+