aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornotin2006-03-17 10:09:02 +0000
committernotin2006-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 21f977f1c0..21f977f1c0 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 3bc5a32e3c..3bc5a32e3c 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 69e57ca42e..69e57ca42e 100755..100644
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
diff --git a/library/nametab.ml b/library/nametab.ml
index e4a8ee9956..e4a8ee9956 100755..100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 62c721b8b8..62c721b8b8 100755..100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b3180b06b2..b3180b06b2 100755..100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index b076de2aff..b076de2aff 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 03f6bbf66e..03f6bbf66e 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 222367b74c..222367b74c 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 8e18665382..8e18665382 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 0da475767b..0da475767b 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 cc6b75d508..cc6b75d508 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 f693298e94..f693298e94 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 1f265b8f52..1f265b8f52 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 02d6b46103..02d6b46103 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 992bc345ac..992bc345ac 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 3e64980cb7..3e64980cb7 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 42dde688a2..42dde688a2 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 3e7d8454b4..3e7d8454b4 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 3fa4226d70..3fa4226d70 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 ef5b448d86..ef5b448d86 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 aaaea9ae41..aaaea9ae41 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 0c0e2f9efe..0c0e2f9efe 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 7fa518d661..7fa518d661 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 c2b5ed7932..c2b5ed7932 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 eac13569af..eac13569af 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 369fd2cbd7..369fd2cbd7 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 4907c93a40..4907c93a40 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 464c8071df..464c8071df 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 9a236b7eef..9a236b7eef 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 6022da116c..6022da116c 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 f427492939..f427492939 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 17f3e5107d..17f3e5107d 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 57d01eefc5..57d01eefc5 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 5aaf0b2090..5aaf0b2090 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 366172381e..366172381e 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 26eae1a055..26eae1a055 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 1c2b97ce76..1c2b97ce76 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 0b0c329bec..0b0c329bec 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 ce94bec14f..ce94bec14f 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 d714b3bf7b..d714b3bf7b 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 3b91afd02f..3b91afd02f 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 3c3b7bbfae..3c3b7bbfae 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 9c53a28be5..9c53a28be5 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 317a5ed078..317a5ed078 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 e0f13b46e2..e0f13b46e2 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 b538620d19..b538620d19 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 6578f6c85f..6578f6c85f 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 eda581e8d5..eda581e8d5 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 a21534bd55..a21534bd55 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 09a941bcde..09a941bcde 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 efd83c1060..efd83c1060 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 9c85d67d03..9c85d67d03 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 53981ea8d1..53981ea8d1 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 94ea964c2e..94ea964c2e 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 469b41783d..469b41783d 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 c3492ba78f..c3492ba78f 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 970d6dab1d..970d6dab1d 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 aad294e938..aad294e938 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 07244e66f7..07244e66f7 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 0068319092..0068319092 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 c323ca3569..c323ca3569 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 1ac59056bc..1ac59056bc 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 cae796861c..cae796861c 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 f15bf19e64..f15bf19e64 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 fd83b0e0df..fd83b0e0df 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 11ac85e845..11ac85e845 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 a7da7db9a4..a7da7db9a4 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 ec8fb7e6d2..ec8fb7e6d2 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 d8bf7dc3c7..d8bf7dc3c7 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 2b5d192db6..2b5d192db6 100755..100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml