diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-17 10:09:02 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-17 10:09:02 +0000 |
commit | ceb78dca0e2172577d0e2d4a15aa80da7d6bc5ae (patch) | |
tree | 0e2631760eae9dd51c1cfb944a5313654338ffbc /theories | |
parent | f78ee253bfced259d29b2e25ae6f8890be750ce3 (diff) |
Modification des propriétés (svn:executable)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
64 files changed, 0 insertions, 0 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index b076de2af..b076de2af 100755..100644 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 03f6bbf66..03f6bbf66 100755..100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 222367b74..222367b74 100755..100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 8e1866538..8e1866538 100755..100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v index 0da475767..0da475767 100755..100644 --- a/theories/Arith/Div.v +++ b/theories/Arith/Div.v diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index cc6b75d50..cc6b75d50 100755..100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index f693298e9..f693298e9 100755..100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 1f265b8f5..1f265b8f5 100755..100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 02d6b4610..02d6b4610 100755..100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 992bc345a..992bc345a 100755..100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 3e64980cb..3e64980cb 100755..100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 42dde688a..42dde688a 100755..100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 3e7d8454b..3e7d8454b 100755..100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 3fa4226d7..3fa4226d7 100755..100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index ef5b448d8..ef5b448d8 100755..100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index aaaea9ae4..aaaea9ae4 100755..100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0c0e2f9ef..0c0e2f9ef 100755..100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 7fa518d66..7fa518d66 100755..100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index c2b5ed793..c2b5ed793 100755..100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index eac13569a..eac13569a 100755..100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 369fd2cbd..369fd2cbd 100755..100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4907c93a4..4907c93a4 100755..100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 464c8071d..464c8071d 100755..100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 9a236b7ee..9a236b7ee 100755..100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 6022da116..6022da116 100755..100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index f42749293..f42749293 100755..100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 17f3e5107..17f3e5107 100755..100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 57d01eefc..57d01eefc 100755..100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v index 5aaf0b209..5aaf0b209 100755..100644 --- a/theories/Lists/MonoList.v +++ b/theories/Lists/MonoList.v diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 366172381..366172381 100755..100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index 26eae1a05..26eae1a05 100755..100644 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 1c2b97ce7..1c2b97ce7 100755..100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index 0b0c329be..0b0c329be 100755..100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index ce94bec14..ce94bec14 100755..100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index d714b3bf7..d714b3bf7 100755..100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 3b91afd02..3b91afd02 100755..100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 3c3b7bbfa..3c3b7bbfa 100755..100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index 9c53a28be..9c53a28be 100755..100644 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 317a5ed07..317a5ed07 100755..100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index e0f13b46e..e0f13b46e 100755..100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index b538620d1..b538620d1 100755..100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 6578f6c85..6578f6c85 100755..100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index eda581e8d..eda581e8d 100755..100644 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index a21534bd5..a21534bd5 100755..100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 09a941bcd..09a941bcd 100755..100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index efd83c106..efd83c106 100755..100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 9c85d67d0..9c85d67d0 100755..100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 53981ea8d..53981ea8d 100755..100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 94ea964c2..94ea964c2 100755..100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 469b41783..469b41783 100755..100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index c3492ba78..c3492ba78 100755..100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 970d6dab1..970d6dab1 100755..100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index aad294e93..aad294e93 100755..100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 07244e66f..07244e66f 100755..100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 006831909..006831909 100755..100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index c323ca356..c323ca356 100755..100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 1ac59056b..1ac59056b 100755..100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index cae796861..cae796861 100755..100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index f15bf19e6..f15bf19e6 100755..100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index fd83b0e0d..fd83b0e0d 100755..100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index 11ac85e84..11ac85e84 100755..100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index a7da7db9a..a7da7db9a 100755..100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index ec8fb7e6d..ec8fb7e6d 100755..100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index d8bf7dc3c..d8bf7dc3c 100755..100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v |