aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Wf_Z.v
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-24 10:27:08 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-24 10:27:08 +0000
commit38734c5e122e9a38cf5b8afc586f47abced11361 (patch)
tree2227afa958bf809d9152b526e29f183b552e5e61 /theories/ZArith/Wf_Z.v
parentc69ae2a1f05db124c19b7f326ca23e980f643198 (diff)
changement de pose en set (pose n'etait pas utilise avec la semantique
documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Wf_Z.v')
-rw-r--r--theories/ZArith/Wf_Z.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 1b1cf27d2..afe21b8d4 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -201,4 +201,4 @@ Proof.
exact Z_lt_rec.
Qed.
-End Efficient_Rec. \ No newline at end of file
+End Efficient_Rec.