From 6b2d99445d35ea71cd24becb7f936e0cc9779d46 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 8 Feb 2001 08:29:12 +0000 Subject: simplification du make depend; fonctions de stat. util. memoire dans certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Zarith/fast_integer.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v index c933ebedc8..d301a7d409 100644 --- a/theories/Zarith/fast_integer.v +++ b/theories/Zarith/fast_integer.v @@ -1476,4 +1476,4 @@ Intros x y;Case x;Case y; [ | Unfold Zcompare; Intros q p; Rewrite <- ZC4; Intros H; Exists (true_sub q p); Simpl; Rewrite (ZC1 q p H); Trivial with arith]. Save. -End fast_integers. \ No newline at end of file +End fast_integers. -- cgit v1.2.3