aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-17 10:09:02 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-17 10:09:02 +0000
commitceb78dca0e2172577d0e2d4a15aa80da7d6bc5ae (patch)
tree0e2631760eae9dd51c1cfb944a5313654338ffbc
parentf78ee253bfced259d29b2e25ae6f8890be750ce3 (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
-rw-r--r--[-rwxr-xr-x]contrib/interface/blast.ml0
-rw-r--r--[-rwxr-xr-x]contrib/omega/Omega.v0
-rw-r--r--[-rwxr-xr-x]contrib/omega/omega.ml0
-rw-r--r--[-rwxr-xr-x]library/nametab.ml0
-rw-r--r--[-rwxr-xr-x]pretyping/classops.ml0
-rw-r--r--[-rwxr-xr-x]pretyping/recordops.ml0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Arith.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Between.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Compare.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Compare_dec.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Div.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/EqNat.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Gt.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Le.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Lt.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Max.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Min.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Minus.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Mult.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Peano_dec.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Plus.v0
-rw-r--r--[-rwxr-xr-x]theories/Arith/Wf_nat.v0
-rw-r--r--[-rwxr-xr-x]theories/Bool/Bool.v0
-rw-r--r--[-rwxr-xr-x]theories/Bool/DecBool.v0
-rw-r--r--[-rwxr-xr-x]theories/Bool/IfProp.v0
-rw-r--r--[-rwxr-xr-x]theories/Bool/Zerob.v0
-rw-r--r--[-rwxr-xr-x]theories/Init/Datatypes.v0
-rw-r--r--[-rwxr-xr-x]theories/Init/Logic.v0
-rw-r--r--[-rwxr-xr-x]theories/Init/Logic_Type.v0
-rw-r--r--[-rwxr-xr-x]theories/Init/Peano.v0
-rw-r--r--[-rwxr-xr-x]theories/Init/Prelude.v0
-rw-r--r--[-rwxr-xr-x]theories/Init/Specif.v0
-rw-r--r--[-rwxr-xr-x]theories/Init/Wf.v0
-rw-r--r--[-rwxr-xr-x]theories/Lists/List.v0
-rw-r--r--[-rwxr-xr-x]theories/Lists/MonoList.v0
-rw-r--r--[-rwxr-xr-x]theories/Lists/Streams.v0
-rw-r--r--[-rwxr-xr-x]theories/Lists/TheoryList.v0
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical.v0
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Pred_Set.v0
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Pred_Type.v0
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Prop.v0
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Type.v0
-rw-r--r--[-rwxr-xr-x]theories/Logic/Eqdep.v0
-rw-r--r--[-rwxr-xr-x]theories/Relations/Newman.v0
-rw-r--r--[-rwxr-xr-x]theories/Relations/Operators_Properties.v0
-rw-r--r--[-rwxr-xr-x]theories/Relations/Relation_Definitions.v0
-rw-r--r--[-rwxr-xr-x]theories/Relations/Relation_Operators.v0
-rw-r--r--[-rwxr-xr-x]theories/Relations/Relations.v0
-rw-r--r--[-rwxr-xr-x]theories/Relations/Rstar.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Classical_sets.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Constructive_sets.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Cpo.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Ensembles.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Finite_sets.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Finite_sets_facts.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Image.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Infinite_sets.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Integers.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Multiset.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Partial_Order.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Permut.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Powerset.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Powerset_Classical_facts.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Powerset_facts.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Relations_1.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Relations_1_facts.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Relations_2.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Relations_2_facts.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Relations_3.v0
-rw-r--r--[-rwxr-xr-x]theories/Sets/Relations_3_facts.v0
-rw-r--r--[-rwxr-xr-x]tools/coqdep.ml0
71 files changed, 0 insertions, 0 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 21f977f1c..21f977f1c 100755..100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 3bc5a32e3..3bc5a32e3 100755..100644
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index 69e57ca42..69e57ca42 100755..100644
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
diff --git a/library/nametab.ml b/library/nametab.ml
index e4a8ee995..e4a8ee995 100755..100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 62c721b8b..62c721b8b 100755..100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b3180b06b..b3180b06b 100755..100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
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
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2b5d192db..2b5d192db 100755..100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml